(Redirected from
Process calculi)
In the first half of the 20th century, various formalisms were
proposed to capture the informal concept of computable function,
μ-recursive functions, Turing Machines
and the λ-calculus possibly being the most well-known
examples today. The surprising fact that they are essentially
equivalent in the sense that they are all encodable into each other
is the content of the Church-Turing thesis.
Another shared feature is more rarely commented on: they
all are most readily understood as models of sequential
computation.
The subsequent consolidation of computer science required a more
subtle formulation of the notion of computation, in particular
explicit representations of concurrency and communication. Petri-Nets
and calculi such as Tony Hoare's CSP, Robin Milner's CCS and
the π-calculus by Milner, Joachim Parrow and David Walker are
currently the most prominent calculi to have emerged from this line of
enquiry.
The process calculus approach gathered momentum in the 1970s when it
became increasingly clear that the then dominant approaches to
modelling computation were unlikely to yield satisfactory accounts of
non-deterministic, non-terminating and interacting agents. Instead,
early pioneers such as Milner and Hoare decided to make interaction
between agents executing in parallel the basic computational
primitive. This can be done in several ways that can be characterised
by three core design decisions.
- Computing agents have zero or more discrete points of connection and interaction called, interchangeably, names, channels or interaction points. Parallel composition of two agents involves connecting their interaction points by links, whenever they share a name. Crucially, a link does not preclude further connections at a name. The Internet is a good source of analogies here: names correspond roughly to IP addresses (plus port numbers, but let's ignore this detail for simplicity).
- Computation itself is binary, point-to-point interaction between independent agents. Interaction happens along names by handshaking or synchronisation between a sender and a receiver. This handshaking may or may not involve passing data from the sender to the receiver. In the Internet, interaction happens by sending IP packets between computers.
- Interaction is an atemporal event in the sense that it does not have a duration. Interactions may be ordered in time. Here the Internet analogy breaks down because the duration of packet delivery from sender to receiver has important semantic consequences.
To define a process calculus, one starts with a set of names,
the discrete interaction points. Names have no internal structure
apart from what is required to distinguish names from one
another. Hence names are pure. Their only purpose is to denote
interaction points. In many implementations, names have rich internal
structure to improve efficiency, but this is abstracted away in
most theoretic models. In addition to names, one needs
a means to form new processes from old: the crucial operators, always
present in some form or other, allow
- the parallel composition of processes,
- to specify which channels to use for sending and receiving data,
- sequentialisation of interactions,
- hiding of interaction points and
- recursion or replication.
Parallel composition of two processes P and Q, usually written
P | Q is the key primitive distinguishing sequential models of
computation from process calculi. It allows computation in P and
Q to proceed simultaneously and independently. But it also allows
interaction, that is synchronisation and flow of information from
P to Q on a channel shared by both (or vice versa). Channels
are created by shared names in parallel composition.
Interaction is a directed flow of information. That means, input
and output are distinguished
as dual interaction primitives. We have an input operator x(v)
and an output operator x<y>, both of which name
an interaction point (here x) that is used to synchronise with a
dual interaction primitive.
Should
information be exchanged, it will flow from the outputting to the
inputting process. The output primitive will specify the data to be
sent. In x<y>, this data is y. Similarly, if an input expects to receive
data, one or more bound variables will act as place-holders to
be substituted by data, when it arrives. In x(v), v plays that
role. But what kind of data is exchanged in an interaction? There are
various choices. It will turn out that this choice is a key
distinguishing feature between process calculi.
Sometimes interactions must be temporally ordered, because we might
want to specify algorithms like: first receive some data on x and
then send that data on y. Sequential composition can be used
for such purposes. It is well-known from other models of computation.
In process calculi, the sequentialisation operator is usually
integrated with input or output or both. For example the process
x(v).P will wait for an input on x. Only when this input
occurs, P will be activated with the
received data substituted for v.
The key operational rule, containing the computational essence of process
calculi, can be given solely in terms of parallel composition,
sequentialisation, input and output: although the details vary, it
always looks something like this.
x<y>.P | x(v).Q ---→P | Q[y/v]
The process x<y>.P sends a message, here y, along the channel
x. Once that message has been sent, x<y>.P becomes the process
P. Dually, the
process x(v).Q receives that message on channel x to become
Q[y/v], which is Q with the place-holder v
substituted by y, the data received on x. The class of
processes that P is allowed to range over as the continuation of
the output operation substantially influences the properties of the
calculus.
Processes
do not limit the
number of connection that can be made at a given interaction point.
But interaction points allow interference (i.e. interaction). For the
synthesis of compact, minimal and compositional systems, the ability
to restrict interference is crucial. Hiding operations allow to
control the connections made between interaction points when composing
agents in parallel. In sequential models of computation, scoping
rules, procedures and objects facilitate hiding (but they might have
other uses, too: functional features in the case of procedures and
subtyping with its associated dispatch mechanisms for objects). We
denote the hiding of a name x in P by (ν x)P. Figure
shows the effect of going from P to (ν x)P. The process
P on the left can interact with the outside world on x, y and
z. In contrast, (ν x)P on the right can only use y and
z for this purpose. The restriction does not prevent usage of
x inside P. But what happens if x gets sent to a process
outside of (ν x)P, as may happen in (ν x)(y<x> | Q),
provided x \neq y? Whether or not it is possible to communicate a
name hidden this way is another important point of divergence between
different calculi.
The operations presented so far allow to describe only finite
interaction and are consequently insufficient for full computability,
which includes non-terminating behaviour. Recursion or
replication are operations that allow finite descriptions of
infinite behaviour. Recursion is well-known from the sequential
world. Replication !P can be understood as abbreviating
the parallel composition of a countably infinite number of
P 's.
Finally, we mention the
null process which has no interaction points. It is utterly
inactive and its sole purpose is to act as the inductive anchor on top
of which we can generate more interesting processes.
Many different variants of process calculi have been studied and not
all of them fit the paradigm sketched here. The most prominent example
may be the Ambient calculus. This is to be expected as process calculi
are an active field of study. Currently research on process calculi focuses
on the following problems.
- Development of new process calculi for better modelling of computational phenomena.
- Finding well behaved subcalculi of a given process calculus. This is valuable because (1) most calculi are fairly wild in the sense that they are rather general and not much can be said about arbitrary processes; and (2) computational application rarely exhaust the whole of a calculus. Rather they use only processes that are very constrained in form. Constraining the shape of processes is mustly studied by way of Datatype.
- Logics for processes that allow to reason about (essentially) arbitrary properties of processes, following the ideas of Hoare logic.
- Behavioural theory: what does it mean for two processes to be the same? How can we decide whether two processes are different or not? Can we find representatives for equivalence classes of processes. Generally, processes are considered to be the same if no context, that is other processes running in parallel, can detect a difference. Unfortunately, making this intuition precises is subtle and mostly yields unwieldy characterisations of equality (which must also be undecidable, as a consequence of the Halting Problem in most cases). Bisimulations are a technical tool that aids reasoning about process equivalences.
- Expressivity of calculi. Programming experience shows that certain problems are easier to solve in some languages than in others. This phenomenon calls for a more precise characterisation of the expressivity of calculi modelling computation than that afforded by the Church-Turing thesis. One way of doing this is to consider encodings between two formalisms and see what properties encodings can potentially preserve. The more properties can be preserved, the more expressive the target of the encoding is said to be. For process calculi, the celebrated results are that the synchronous π-calculus is more expressive than its asynchronous variant, has the same expressive power as the higher-order π-calculus, but less than the Ambient calculus.
- Using process calculus to model biological systems. It is thought by some that the compositionality offered by process-theoretic tools can help biologists to organise their knowledge more formally.