• 0 | 0

This is arguably the second simplest process; it concurrently runs the stopped process with itself. Should we be able to simplify this process?

• *@0

Since 0 is the simplest process, @0 is the simplest name. This process dereferences the name @0. Should we be able to simplify this process?

• @(0 | 0)!(0)

Since 0 | 0 is a process, @(0 | 0) is a name which provides a channel to send messages on. This process sends the message @0 on the channel @(0 | 0).

• for(@(0 | 0) ← @0)0

This process waits for a message on the channel @0. When it is received, it substitutes the received name for @(0 | 0) in the process 0.

• @0!(0) | for(@0 ← @0)0

This process concurrently sends and receives the message @0 on the channel @0. Just like in π-calculus, this will result in a communication!

• @(@0!(0))!(0)

Since @0!(0) is a process, we can quote it to form the name @(@0!(0)) which gives us another channel to send messages on. This process sends the name @0 on the channel @(@0!(0)).

• for(@0 ← @(0 | 0))@0!(0)

This process waits for a message on the channel @(0 | 0) to substitute for the name @0 in the process @0!(0).
Now we will discuss the different notions of equivalence in [latex]ρ[/latex]-calculus.

Notions of equivalence

Structural congruence

Just like in π-calculus, we expect some of the processes to be equivalent from the viewpoint of computation. Again, this equivalence, denoted by ≡, is called structural congruence. This is the least equivalence, containing α-equivalence that satisfies the following laws:

• P | 0 ≡ P
• P | Q ≡ Q | P
• (P | Q) | R ≡ P | (Q | R)

Structural congruence pertains to processes, not names.

Name equivalence

Name equivalence, denoted by ≡N, has two instantiations pertaining to (i) a single name and (ii) structurally congruent processes:

(i)   @(*x) ≡N  x

This equivalence says quoting a dereferenced name is name equivalent to the name itself. The thinking is that if we turn some code into a program and turn that program into its code, then we should simply reproduce the original code.

(ii) If P ≡ Q, then @P ≡N  @Q.

This equivalence says that structurally congruent processes, P and Q, have name equivalent quotations, @P and @Q. The idea is that two programs which have equivalent execution also have equivalent code.

α-equivalence

Recall the concept of α-conversion in λ-calculus. It said two terms were equivalent if they only differ by their bound names, i.e. they only differ by what we call the variables in the term. There is an analogous concept called α-equivalence, denoted by ≡α, in [latex]ρ[/latex]-calculus (and also π-calculus). Two [latex]ρ[/latex]-calculus processes are called α-equivalent if they differ only by what they call the names they reference. That is, P ≡α Q if P and Q only differ by the names used to construct these processes. A few examples of α-equivalent processes:

x!(0) ≡α  y!(0),

P | for(y ← x)0 ≡α  P | for(w ← u)0.

Two α-equivalent processes have the same code so they both represent the same program.

Substitutions & operational semantics

As in other computational calculi, we have rules for substitutions and what these substitutions mean in terms of computation, i.e. the comm rule. We will denote the substitution of the name y for the name x within the process P by (P){y/x}.

Syntactic substitution

The rules for syntactic substitutions dictate how the substitution of names translates to that of processes (because processes are built from 0 and names). On the level of names, substitution is straight forward, but we must build the concept of name substitution in a process. Thus, we have a rule for each term constructor. The rules for name substitution in processes are built from:

• (0){@Q/@P} = 0

Any substitution of names in the stopped process does not change the stopped process;

• (!R){@Q/@P} =!(R){@Q/@P}

There is only one process to do substitution with in replication and it proceeds in the obvious way, we replicate the substituted process;

• (R | S){@Q/@P} = (R){@Q/@P} | (S){@Q/@P}

Substitution in processes running in parallel is just a substitution in each process separately, then the substituted processes are run in parallel;

• (x!(R)){@Q/@P} = (x){@Q/@P}!((R){@Q/@P})

Substitution in a send works as expected. First, we do the appropriate substitution with the channel name x; this explains the appearance of (x){@Q/@P}, a new channel to send a message on. Then, we do the appropriate substitution with the process R; this explains the appearance of (R){@Q/@P}, a new message to send on the channel;

• (for(y ← x)R){@Q/@P} = for(z ← (x){@Q/@P})((R){z/y}){@Q/@P}

This rule looks very complicated so let’s unravel it. First, we do a name substitution with the receiving channel x; this explains the appearance of (x){@Q/@P} within the for-comprehension. Then, we call the message we’re waiting for, y, by a different name, z. Since we switched this label, we must substitute z for every appearance of y in the process R, hence the appearance of (R){z/y}. Ultimately, we need to do name substitution within the process (R){z/y}; this explains the appearance of ((R){z/y}){@Q/@P};

• (*x){@Q/@P} = *@Q if x ≡N @P, *x otherwise

Substitution with a dereferenced name is straight forward. If the name x is name equivalent to @P, then we do the expected substitution, i.e. @Q is substituted for x. If x is not name equivalent to @P, nothing changes;

Usual name substitution has the rule

(x){@Q/@P} = @Q if x ≡N @P, x otherwise.

In [latex]ρ[/latex]-calculus, we must also take name equivalence into consideration. So, we perform the substitution for any name equivalent name also.

These syntactic substitution rules tell us how to write down the substitutions for processes, but they do not necessarily tell us what these substitutions mean in terms of computation. This is where the semantic substitution comes in.

Semantic substitution

Some real special sauce comes from the notion of semantic substitution. We have discussed quoting processes and dereferencing names, how quoting a process results in a name, and how dereferencing a name results in a process, but we have not explicitly connected the two ideas.
Formally speaking, we have the rule

(*x){@Q/@P} = Q if x ≡N @P, *x otherwise,

which says that if we substitute the name @Q for the name @P in the dereference process *x, then we get the process Q if x is name equivalent to @P, and just ignore the substitution altogether if x is not name equivalent to @P.
This is exactly what we need to happen to ensure that we can think about processes as programs and names as code. We want to be able to take a program (process), write down its code (quote the process), then run the code as a program (dereference the quoted process) and get back the original program (process). The semantic substitution brings this all together.

Operational semantics

We also have the notion of a comm event in [latex]ρ[/latex]-calculus. The idea is that we have communication when we concurrently send and receive on the same channel. Communication is the reduction of a process of the form

x!(Q) | for(z ← x)P → (P){@Q/z}.

We extend this notion of communication using name equivalence. This amounts to communication being generalized to the concurrent sending and receiving of messages on name equivalent channels.

• Comm rule: If x ≡N y, then we have the reduction rule

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

This rule says that the concurrent send, x0!(Q), and receive, for(z ← y)P, on name equivalent channels, x and y, reduces to the substituted process, (P){@Q/z}. The communication rule makes it possible for agents to synchronize and communicate processes packaged as names.

The comm rule interacts with parallel composition and structural congruence just like it does in π-calculus:

• Parallel composition: If P → P’, then P | Q → P’ | Q.

This rule says that if a process P reduces to the process P’, then the process P | Q will reduce to the process P’ | Q.

• Structural congruence: If P ≡ P’, Q ≡ Q’, and P’ → Q’, then P → Q.

This rule says that if we have a process P which is structurally congruent to the process P’, a process Q which is structurally congruent to the process Q’, and the process P’ reduces to the process Q’, then the process P reduces to the process Q.

It’s time for a few examples of reduction.

Examples

@0!(0) | for(@(@0!(0)) ← @0)0 → 0

The send, @0!(0), and receive, for(@0 ← @0)0, processes run concurrently on the same channel, @0. Thus, a comm event occurs and this process reduces to the substitution

(0){@0/@(@0!(0))}.

Recall that (0){z/y} = 0 for any names y, z, thus the process ultimately simplifies to the stopped process 0.

for(@0 ← x)@0!(0) | x!(@0!(0)) → @(@0!(0))!(0)

First, we notice that we are sending and receiving messages on the same channel x so communication occurs. To simplify matters, let’s make P = @0!(0) and Q = @0!(0) so the process we are dealing with can be rewritten as

for(@0 ← x)P | x!(Q).

Using the comm rule (here z = @0), this reduces to

(P){@Q/@0}.

Using the definitions of P and Q, we have

(@0!(0)){@(@0!(0))/@0}

and using the syntactic substitution rule for a send process, we substitute in the name and the process, to get

(@0){@(@0!(0))/@0}!((0){@(@0!(0))/@0}).

Again, using the rules of syntactic substitution, this expression simplifies to

@(@0!(0))!(0).

Therefore, the original process ultimately reduces to a send of @0 on the channel @(@0!(0)).

for(@0 ← @(@0!(0)))*(@0) | @(@0!(0))!(!(@0!(0))) → !(@0!(0))

First, let’s pin down exactly what is going on here. There are two processes running concurrently, the receive process, for(@0 ← @(@0!(0)))*(@0), and the send process, @(@0!(0))!(!(@0!(0))). To simplify matters, let’s call y = @0, P = *y, Q = y!(0), x = @Q, and R =!Q. Now we rewrite the original process

for(y ← x)P | x!(R).

In this format, we clearly see that a comm event occurs and thus, reduces to

(P){@R/y}

Going back to the definitions of P and Q, we have

(*y){@R/y}.

By the semantic substitution rule for dereferencing, this substitution simplifies to the process R, which is just

!(@0!(0)),

replication of the process which sends the message @0 on the channel @0.

This concludes the computational calculi primer series. The next set of posts will follow the DoCC lectures.

References

1. Meredith, Radestock (2005). A Reflective Higher-Order Calculus. Retrieved June 16, 2018.