Term Normalization and Structural Equivalence.

In The original rho calculus paper, Structural equivalence is defined as a mutual recursion between the following 3 equivalences:

1. Parallel composition is a commutative monoid with 0/Nil as the identity.
2. Quote(Drop(x)) is equivalent to x. Otherwise name equivalence.
3. 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:

1. Maps and sets are unordered collections.
2. 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)
3. 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:

1. A standard way to write down a unique representation of a commutative monoid is to impose a sorting.
2. We can enforce as we normalize and evaluate processes that Drop/Quote pairs are zeroed out.
3. 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:

1. new x in \{ new y in \{ P \} \} is not the same as new y in \{ new x in \{ P \} \}

2. Any commutativity of arithmetic expressions.
3. Binding order of free variables in process patterns is not commutative.

The only open question is join binding order.