Page Comparison

...

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. Nearly all terms in practice can be written this way.

When we write the processes down in this way, structural equivalences becomes a byte compare, rather than a complex algorithm.

...

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 .
   1. If the sources (a, b) are different, or the patterns (x
   and y differ. (I have to think about this one, it may be tricky)
   1. , y) are different, then there is an obvious ordering.
   2. If there is a bind of the same pattern as a read from the same channel, then the body is sorted, with those variables having the same sort value.
      1. If there are no parallel terms in the body with the same sort value, the binds can be numbered according to their use in the body.
      2. If there are terms with the same sort value, this is a term that can't be normalized. I have to work out in more detail, but we should be able to mark the parts of a term that lead it to be non-normalizable, and use the exhaustive algorithm just for those parts.

      3. Here's an example showing that for some terms, we just can't normalize them, or we would solve a hard problem:

         Code Block
         for (x0 ← a; x1 ←a; x2 ← a) { x0!(x1) | x1!(x2) | x2!(x0) } vs for (x0 ← a; x1 ←a; x2 ← a) { x0!(x2) | x1!(x0) | x2!(x1) }

         
         

      4. 
         

          It should be clear that if we could normalize terms like this, we could solve the graph isomorphism problem in polynomial time.

3. Because Rholang uses variables for bound names rather than other names, Drop(Quote(P)) is also equivalent to P (I need to think about this. We may do evaluation on quote)

Let's start with the 3 equivalences above:

...

Some equivalences we are not enforcingnot ever enforcing:

1. Any commutativity of arithmetic expressions.

Some equivalences that we will not currently enforce:

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 orderWe would need to use an approach similar to the one outlined above for join binding order. Identify if the term is one with a normalized form, and which sub-terms prevent it from being normalized.