Overview

In the previous post “Intro to Design of Computational Calculi 2”, we covered names, compilable programs, and equivalence of processes.

 

Now, we will explain program equivalence and operational semantics. We will also discuss the concepts of monoids and monads and their connection to computational calculi.

 

Domain-specific languages

Designing a computational calculus for use in a specific setting is synonymous with creating a domain-specific language. Domain-specific languages are one approach to problem-solving from a language perspective (e.g. HTML for web pages or Scheme). They are the product of language-oriented programming, and among the most powerful problem-solving methodologies. In the blockchain space, we need a domain-specific language which captures the range of behaviors of users within the application.

 

Another look at alpha equivalence

The following “Java” programs execute in exactly the same way despite referencing variables with different names.

 

Program 1                        Program 2

    Class C {                          Class C{

       T m( A a ){                     T m( A b ){

           if pred(a){                     if pred(b){

                  }                                          }

               else{                                  else{

                 }                                          }

              }                                         }

           }                                        }

 

Looking at Program 1, inside the class, C, there is a method, m, that takes in an argument, a, of type A, and returns something of type T. Inside the body, we test a predicate of the argument a. If true, we do something, and if false, we do something else. Looking at Program 2, inside the class C, there is a method, m, that takes in an argument, b, of type A, and returns something of type T. Inside the body, we test a predicate of the argument b. If true, we do something, and if false, we do something else.

 

We disregard the textual differences and treat these programs as the same because they execute in the same way (that’s what’s really important anyhow). The exact variable name does not matter as long as we are consistent with its usage. This is one way to think about α-equivalence.

 

Another way to think about the equivalence of programs is in terms of contexts. We say two programs are equivalent if they behave the same in all contexts, i.e. we can freely substitute one for the other in all contexts.

 

Universal algebra: monoids & monads

From the viewpoint of universal algebra, in π-calculus and ρcalculus, the collection of processes form a special structure. Together with the par operator |, the stopped process 0, and the equations from structural equivalence, the processes form an algebraic structure known as a monoid.

 

We define a monoid as a set M equipped with a binary relation : M × M M (i.e. for all a, b M, a b M) and a distinguished element e M (called the identity) which satisfies the following properties:

 

  1. For all a,b,c M, we have (a b) ∗ c = a ∗ (b c). (associativity)
  2. For all a M, we have a e = a = e a. (left and right identity)

 

We will denote all of this by displaying it as (M, , e).

 

The monoid (P, |, 0) formed by the processes has the set of processes P as the underlying set, the par operator | as the binary relation, the stopped process 0 as the identity, and the laws for structural equivalence make | associative and 0 the identity. We actually have additional structure in this case since the order in which we par processes together is irrelevant. So (P, |, 0) is, in fact, a commutative monoid.

 

Bill Lawvere identified a relationship between the grammar-style presentation and the monadic presentation in the 1960’s. He showed that the grammar-style presentation can be captured in what is called a Lawvere theory and that Lawvere theories have a correspondence (isomorphism) to a monad, i.e. you can either start with the monad and get the theory or vice versa. Structural equivalences correspond to the algebras of the monad.

 

In the 2000’s, Jamie Gabbay and Andy Pitts showed that the grammar of a computational calculus, in most cases, is representable by a monad, and used the monadic machinery to abstract out the variable machinery.

 

When we generate type systems using LADL(Logic as a Distributive Law), the monad will represent a key ingredient. Structural equivalence is the other ingredient; a wide range of monads give us freely-generated structures, a lot like the language generated from a grammar with no notion of equivalence of terms.

 

Example

One can freely generate the set of all strings over an alphabet A = {a,b}. This collection, L(A), is known as the language over the alphabet A. We can do better, however. This language can be interpreted as a monoid with as the empty string using concatenation, , as the binary operation. Since string concatenation is naturally associative and the empty string serves as the identity. For example:

 

a b = ab, aa abba = aaabba, bbaa ∗ ∅ = bbaa = ∅ ∗ bbaa

 

We can transform this monoid into a group by adjoining complementary elements a’ and b’ satisfying the equations:

 

a a’ = a’ a = ∅ = b b’ = b’ b

 

This makes it so that each element of L(A) has an inverse, i.e. for each string s1, there is a string s2 such that s1 s2 = s2 s1 = ∅. For example, the inverse of a’baa’b’ is baa’b’a (why?).

 

Operational semantics i.e. reduction rules

Lambda calculus

The rule for β-reduction in λ-calculus applies when an abstraction, which binds a variable in a term, is immediately followed by an application at the top level.

 

(λx.MN) → M{N/x}

 

Rho calculus

The comm rule for reduction in ρ-calculus applies when a send and a receive on the same channel are run in parallel.

 

Comm rule:

for(y x)P | x!(Q) → P{@Q/y}

The comm rule has the following interactions with the par operator and structural equivalence.

 

Par rule:

If P P’, then P | Q P’  | Q.

Structural equivalence rule:

 

If P P’, P’ Q’, and Q’ Q, then P Q.

 

Unlike the laws for structural equivalence (where information is preserved), through reduction, structure is lost or forgotten. Notice that the right side of the comm rule no longer refers to the name x.

 

Example

The reduction rules are purposely left in a succinct format because we can combine them at will. Say we have the expression:

 

for(y x)P | R | x!(Q)

 

We notice that there is a send and a receive on the channel x so there will be a comm event. However, we cannot immediately reduce this expression because the comm rule does not apply as is. We must first put the send and receive next to each other. Luckily, because of the structural equivalence laws, we know the par operator is commutative. Hence, we can change the order in which processes are par-ed together free of charge. So we switch the order of R and x!(Q) to get:

 

for(y x)P | x!(Q) | R

 

Now that the send and receive are adjacent, they can reduce under the comm rule, or can they?… The process R is also present. The par rule comes to the rescue. Since:

 

for(y x)P | x!(Q) → P{@Q/y}

 

we have:

for(y x)P | x!(Q) | R P{@Q/y} | R

 

Putting all the pieces together with the structural equivalence rule, we get:

 

for(y x)P | R | x!(Q) → P{@Q/y} | R

Summary

We covered the notions of program equivalence and operational semantics. We also discussed how a language can be interpreted as a monoid and how the grammar-style presentation of a language relates to a Lawvere theory and hence a monad. Since monads are generalizations of monoids, we presented the definition of a monoid. Lastly, we discussed the operational semantics for λ-calculus and ρ-calculus.

 

The next post in the DoCC series will discuss the injection of names into ρ-calculus.

Secure. Scalable. Sustainable

Twitter  youtube  Facebook  Reddit   Linkedin