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.