In The original rho calculus paper, Structural equivalence is defined as a mutual recursion between the following 3 equivalences:
There is a straightforward algorithm using substitution and exhaustive search for comparing to see if 2 processes are structurally equivalent. This is insufficient if what we want are keys in maps.
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 (new or the result of a for), that name is not to be substituted, like in Rho Calculus, but to be pattern matched. (e.g. in for (@Nil ← y)
P
@Nil
is a pattern, not a variable name, and P is only executed when the quoted empty process is sent on Y. In Rho calculus, P is executed when any name is sent on Y, and that new name is substituted for @Nil
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.
We also plan to support the following additional equivalences:
Here's an example showing that for some terms, we just can't normalize them, or we would solve a hard problem:
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) } |
It should be clear that if we could normalize terms like this, we could solve the graph isomorphism problem in polynomial time.
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 ever enforcing:
Some equivalences that we will not currently enforce:
We 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.