In The original rho calculus paper, Structural equivalence is defined as a mutual recursion between the following 3 equivalences:
- Parallel composition is a commutative monoid with 0/Nil as the identity.
- Quote(Drop(x)) is equivalent to x. Otherwise name equivalence.
- Alpha Equivalence.
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:
- Maps and sets are unordered collections.
- for(x ← a; y ← b) is equivalent to for(y ← b; x ← a) as long as a and b differ or the patterns x and y differ. (I have to think about this one, it may be tricky)
- Because Rholang uses variables for bound names rather than other names, Drop(Quote(P)) is also equivalent to P
Let's start with the 3 equivalences above:
- A standard way to write down a unique representation of a commutative monoid is to impose a sorting.
- We can enforce as we normalize and evaluate processes that Drop/Quote pairs are zeroed out.
- A standard way to handle alpha equivalence is to use a naming discipline. In our case we have chosen DeBruijn levels.
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 \} \}
- Any commutativity of arithmetic expressions.
- Binding order of free variables in process patterns is not commutative.
The only open question is join binding order.