In The original rho calculus paper, Structural equivalence is defined as a mutual recursion between the following 3 equivalences:
An important distinction between Rholang and the Rho calculus is that Rholang does not use names as variables. It uses variables as variables. Whenever a name appears in binding position, that name is not to be substituted, like in rholang, but to be matched.
We want to write down processes in such a form that for any member of the equivalence classes above, we pick a unique representative, this process of picking a unique representation is called Normalization
When we write the processes down in this way, structural equivalences becomes a byte compare, rather than a complex algorithm.
We also plan to support the following additional equivalences:
Let's start with the 3 equivalences above:
I'm working on producing a "semi-normalized" form that is straightforward to sort. Kent has been working on a total sort order for all of the terms.
Some equivalences we are not enforcing:
new x in { new y in { P } } is not the same as new y in { new x in { P } }
The only open question is join binding order.