In
theoretical computer science
computer science (TCS) is a subset of general computer science and mathematics that focuses on mathematical aspects of computer science such as the theory of computation, lambda calculus, and type theory.
It is difficult to circumscribe the ...
, the -calculus (or pi-calculus) is a
process calculus. The -calculus allows channel names to be communicated along the channels themselves, and in this way it is able to describe
concurrent computations whose network configuration may change during the computation.
The -calculus has few terms and is a small, yet expressive language (see ). Functional programs can be encoded into the -calculus, and the encoding emphasises the dialogue nature of computation, drawing connections with
game semantics
Game semantics (german: dialogische Logik, translated as '' dialogical logic'') is an approach to formal semantics that grounds the concepts of truth or validity on game-theoretic concepts, such as the existence of a winning strategy for a play ...
. Extensions of the -calculus, such as the spi calculus and applied , have been successful in reasoning about
cryptographic protocol
A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol descri ...
s. Beside the original use in describing concurrent systems, the -calculus has also been used to reason about
business process
A business process, business method or business function is a collection of related, structured activities or tasks by people or equipment in which a specific sequence produces a service or product (serves a particular business goal) for a parti ...
es
[OMG Specification (2011)]
"Business Process Model and Notation (BPMN) Version 2.0"
'' Object Management Group''. p.21 and
molecular biology
Molecular biology is the branch of biology that seeks to understand the molecular basis of biological activity in and between cells, including biomolecular synthesis, modification, mechanisms, and interactions. The study of chemical and phys ...
.
Informal definition
The -calculus belongs to the family of
process calculi, mathematical formalisms for describing and analyzing properties of concurrent computation. In fact, the -calculus, like the
λ-calculus, is so minimal that it does not contain primitives such as numbers, booleans, data structures, variables, functions, or even the usual control flow statements (such as
if-then-else
,
while
).
Process constructs
Central to the -calculus is the notion of ''name''. The simplicity of the calculus lies in the dual role that names play as ''communication channels'' and ''variables''.
The process constructs available in the calculus are the following (a precise definition is given in the following section):
* ''concurrency'', written
, where
and
are two processes or threads executed concurrently.
* ''communication'', where
** ''input prefixing''
is a process waiting for a message that was sent on a communication channel named
before proceeding as binding the name received to the name Typically, this models either a process expecting a communication from the network or a label
c
usable only once by a
goto c
operation.
** ''output prefixing''
describes that the name
is emitted on channel
before proceeding as Typically, this models either sending a message on the network or a
goto c
operation.
* ''replication'', written
, which may be seen as a process which can always create a new copy of Typically, this models either a network service or a label
c
waiting for any number of
goto c
operations.
* ''creation of a new name'', written
, which may be seen as a process allocating a new constant within The constants of are defined by their names only and are always communication channels. Creation of a new name in a process is also called ''restriction''.
* the nil process, written
, is a process whose execution is complete and has stopped.
Although the minimalism of the -calculus prevents us from writing programs in the normal sense, it is easy to extend the calculus. In particular, it is easy to define both control structures such as recursion, loops and sequential composition and datatypes such as first-order functions,
truth value
In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values ('' true'' or '' false'').
Computing
In some pro ...
s, lists and integers. Moreover, extensions of the have been proposed which take into account distribution or public-key cryptography. The ''applied '' due to Abadi and Fourne
put these various extensions on a formal footing by extending the with arbitrary datatypes.
A small example
Below is a tiny example of a process which consists of three parallel components. The channel name is only known by the first two components.
:
The first two components are able to communicate on the channel , and the name becomes bound to . The next step in the process is therefore
:
Note that the remaining is not affected because it is defined in an inner scope.
The second and third parallel components can now communicate on the channel name , and the name becomes bound to . The next step in the process is now
:
Note that since the local name has been output, the scope of is extended to cover the third component as well. Finally, the channel can be used for sending the name . After that all concurrently executing processes have stopped
:
Formal definition
Syntax
Let Χ be a set of objects called ''names''. The
abstract syntax for the -calculus is built from the following
BNF grammar (where ''x'' and ''y'' are any names from Χ):
:
In the concrete syntax below, the prefixes bind more tightly than the parallel composition (, ), and parentheses are used to disambiguate.
Names are bound by the restriction and input prefix constructs. Formally, the set of free names of a process in –calculus are defined inductively by the table below. The set of bound names of a process are defined as the names of a process that are not in the set of free names.
Structural congruence
Central to both the reduction semantics and the labelled transition semantics is the notion of structural congruence. Two processes are structurally congruent, if they are identical up to structure. In particular, parallel composition is commutative and associative.
More precisely, structural congruence is defined as the least equivalence relation preserved by the process constructs and satisfying:
''Alpha-conversion'':
:*
if
can be obtained from
by renaming one or more bound names in
.
''Axioms for parallel composition'':
:*
:*
:*
''Axioms for restriction'':
:*
:*
''Axiom for replication'':
:*
''Axiom relating restriction and parallel'':
:*
if is not a free name of
.
This last axiom is known as the "scope extension" axiom. This axiom is central, since it describes how a bound name may be extruded by an output action, causing the scope of to be extended. In cases where is a free name of
, alpha-conversion may be used to allow extension to proceed.
Reduction semantics
We write
if
can perform a computation step, following which it is now
.
This ''reduction relation''
is defined as the least relation closed under a set of reduction rules.
The main reduction rule which captures the ability of processes to communicate through channels is the following:
*
: where