Overview
The first post in this series covered grammar and operational semantics for λ-calculus.
Our interest in π-calculus lies in the fact that it is the precursor of [latex]ρ[/latex]-calculus. It is a model of concurrent computation, or more specifically, a process calculus based upon a notion of naming. In a process calculus, we represent interactions between independent agents or processes as message-passing, as opposed to modifications of shared variables (as in λ-calculus).
π-calculus differs from λ-calculus in the distinction made between names and processes and by the addition of term constructors, including parallel composition, which is responsible for concurrency. So, there are two distinct entities in π-calculus, processes and names, and different interactions between processes and names. However, just like λ-terms, the processes in π-calculus are built from names.
Parallel composition allows the computation in processes to either to proceed either concurrently and independently or to communicate on a shared channel. This is useful for smart contract applications and storing state transitions of a virtual machine.
In this post, we discuss the grammar, structural congruence, and operational semantics of π-calculus.
π-calculus
Here we will discuss a simplified version of π-calculus proposed by Robin Milner [1].
Grammar
The BNF presentation of a grammar for π-calculus
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (????x)P | P|Q | !P (1.1)
much like that of λ-calculus, is parametric in a set of names X. Without even knowing what these operators mean, we already know that we can write
P[X] ::= 0 | X(X).P[X] | X̅⟨X⟩.P[X] | (????X)P[X] | P[X]|P[X] | !P[X]
to express this dependence on X explicitly.
Returning to (1.1), the admissible terms in this grammar, i.e. the expressions on the right-hand side of this presentation, are also called term constructors. We discuss these term constructors below.
Stopped process: 0
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
This process represents “do nothing”, i.e. execution is complete, and it has stopped.
Input-guarded continuation or input prefixing: x(y).P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
This process waits for a name sent on channel x to substitute for the name y in the process P. This plays an analogous role to abstraction of the name y, λy.P, in λ-calculus, binding the name y in the process P.
Send on a channel and execute or output prefixing: x̅⟨y⟩.P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
Sends the name y on the channel x as a substitute name in an input-guarded process waiting on the channel x and then runs P.
Restriction or creation of a new name: (νx)P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
(νx)P – read “new x in P” – defines x as a new name and binds it in the process P.
Parallel composition: P | Q
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
P | Q – read “P par Q” – means the processes P and Q are concurrently active; they can act independently, or they can communicate with one another.
Replication: !P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q | !P
!P – read “bang P” – means P | P | …; as many copies as you wish. This process can always create a new copy of P. The reduction rules make it so that there is no risk of infinite concurrent activity.
Every process in π-calculus is built from the stopped process 0. Let’s build a few simple processes.
A few simple processes
- 0
This is the simplest process, out of which all other processes are created.
- x(y).0
This process waits for the message y on the channel x and then stops.
- x̅⟨y⟩.0
This process sends the message y on the channel x and then stops.
- (????x)0
This process declares a new name x in the stopped process.
Do you think this should correspond to a process we already have?
- 0 | 0
The stopped process runs concurrently with the stopped process.
Do you think this should correspond to a process we already have?
- x̅⟨y⟩.0 | x(z).0
This process concurrently sends and receives a message on the channel x. This is how communication occurs!
Concurrently sending and receiving messages on the same channel allows for communication on that channel. In general, the process x̅⟨y⟩.P | x(z).Q corresponds to a communication on channel x. It is said that x and x̅ are in a name/co-name relationship.
Structural congruence
Intuitively, we expect equivalence between some processes. For instance, P | 0, 0 | P, and P should all be equivalent. Think about it.
The process P | 0 means that we are running the process P concurrently with the stopped process 0. That shouldn’t be any different than running the process P by itself. Generally speaking, we denote the structural congruence of processes P and Q by P ≡ Q. Our intuitions are codified by the following axioms of structural congruence.
- α-equivalence:
P ≡ Q if Q can be obtained from P by renaming one or more names bound in P (we will discuss free and bound names in more depth later in the series). This is analogous to α-conversion in λ-calculus. This amounts to two programs being equivalent if they only differ by the names of variables used within. They execute the same code, but maybe calls things by different names in a consistent manner.
- Axioms for parallel composition:
– P | Q ≡ Q | P
The order in which we list concurrent processes shouldn’t matter because they execute at the same time. Therefore, the processes P | Q and Q | P are equivalent.
– (P | Q) | R ≡ P | (Q | R)
The par operator should be associative. We only ever talk about “par-ing” two processes together, so if we want to throw a third process into the mix, there are two distinct ways to do that. This equivalence says these two ways are the same because we are running these processes concurrently.
– P | 0 ≡ P
Running the stopped process along with another process P shouldn’t be any different than running P alone. This equivalence says exactly that. Par-ing a process with the stopped process is analogous to addition of the number 0.
- Axioms for restriction:
– (????x)(????y)P ≡ (????y)(????x)P
When declaring new names in a process, the order shouldn’t matter. This equivalence captures that notion.
– (????x)0 ≡ 0
Declaring a new name in the stopped process shouldn’t do anything. Therefore, it should be equivalent to the stopped process.
- Axiom for replication:
– !P ≡ P | !P
With replication of a process, we can always create a new copy of the process. Therefore, the processes !P and P | !P are equivalent.
- Axiom relating restriction and parallel:
If the name x is bound in Q, then (νx)(P | Q) ≡ (νx)P | Q.
These are the properties of structural congruence in π-calculus. Structural congruence captures the notion of computational indistinguishability. That is, two structurally congruent processes are identical from the point of view of computation.
Structural congruence is an example of what is called an equivalence relation in mathematics. We view it as computational equivalence of processes.
We will now make the notion of communication in π-calculus precise and discuss the operational semantics.
Operational semantics, i.e. reduction rules
Recall that the prefix represents sending a message y on the channel x, and the prefix x(z) represents receiving a message z on the channel x. The thinking is that when a send and receive on the same channel happen concurrently, communication takes place and the receiver then uses the passed information. In symbols, this is written
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
The → is notation for “reduces to” and we call this the comm reduction or comm rule. This means that if we find two processes x̅⟨y⟩.P and x(z).Q running concurrently, then y is sent on channel x, y replaces z in the process Q, and the processes P and Q{y/z} run concurrently. This is analogous to β-reduction in λ-calculus. It’s so important, I’ll write it
twice
- Comm rule:
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
The comm rule interacts with parallel composition, restriction, and structural congruence:
- Parallel composition:
If P → Q, then P | R → Q | R.
- Restriction:
If P → Q, then (????x)P → (????x)Q.
- Structural congruence:
If P ≡ P’, Q ≡ Q’, and P’ → Q’, then P → Q.
We should get our feet wet with some examples.
Examples
(i) x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
Proof: The first two processes, x̅⟨y⟩.0 and x(z).P, will comm to give us
x̅⟨y⟩.0 | x(z).P → 0 | P{y/z}
and we have that 0 | P{y/z} ≡ P{y/z}. By the way the comm rule interacts with parallel composition, we now get
x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
(ii) x̅⟨y⟩.0 | x(u).P| x(v).Q does not reduce uniquely
We have two valid reductions as there are two possible comms that can occur. One reduction results from a comm between the first and second terms, i.e. reduces to
P{y/u} | x(v).Q
and the other results from a comm between the first and third terms, i.e. reduces to
x(u).P | Q{y/v}
(iii) (νx)(x̅⟨y⟩.0 | x(z).P) | x(u).Q → P{y/z} | x(u).Q
Proof: The restriction of the name x to the first two terms in the parallel composition results in a unique reduction in this case, as opposed to the previous example. Here the name x restricted by (νx) is distinct from the name x appearing in the term x(u).Q. Therefore, only the first two terms comm resulting in the reduction
P{y/z} | x(u).Q
(iv) !x̅⟨y⟩.0 | x(u).P→ !x̅⟨y⟩.0 | P{y/u}
Proof: We know that !x̅⟨y⟩.0 ≡ !x̅⟨y⟩.0 | x̅⟨y⟩.0 because replication always allows for the creation of another copy. Now we have a comm between x̅⟨y⟩.0 and x(u).P, which we have seen reduces to P{y/u}. Thus, we are left with
!x̅⟨y⟩.0 | P{y/u}
To summarize, the π-calculus is a concurrent model of computation based on the notion of naming, in which we represent interactions between agents as message-passing. This message-passing occurs when we have concurrent send and receive processes on the same channel. In π-calculus, we make a distinction between names and processes and we have the option to run computations concurrently. These are the major differences with λ-calculus.
To see the full version of π-calculus, see [1]. We have not discussed the choice operator and normal processes because our intention in introducing π-calculus was to investigate concurrency and how that is dealt with in a grammar.
The goals of this computational calculi primer series are to introduce [latex]ρ[/latex]-calculus and set the foundation for the DoCC lectures. We will achieve both goals with the next article.
References
- Milner, R. (1991). The Polyadic π-Calculus: A Tutorial. Retrieved August 18, 2018