Versions Compared

Key

  • This line was added.
  • This line was removed.
  • Formatting was changed.

...

  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.

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 rholangRho 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

...

  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 (Closest English Pronunciation: Duh Brown) 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.

...