The Pi-Calculus: A Theory of Mobile Processes [Paperback]

It is interesting that the pi-calculus, which on first inspection can be viewed as a highly abstract formalism somewhat removed from reality, has now found application in a variety of fields, such as business process modeling, computational biology, artificial intelligence, and network modeling. It is one of the many examples of process algebra that have appeared in the last two decades, and has been the subject of intense research. This book gives an overview of the formalism of pi-calculus, both in its original form as envisaged by its creator Robin Milner, and from the standpoint of its variations and extensions. For readers (such as this reviewer) who are relatively new to process algebra, the writing may be somewhat difficult to follow, this due mostly to the choice of notation. On the other hand, readers (such as this reviewer) who are familiar with the lambda calculus or functional programming will find familiar territory in the book, and will more fully appreciate the sixth part of the book, which deals with the interpretation of functions as processes. Those readers interested in applications will have to consult other books and papers.

Conceptually the pi-calculus is fairly easy to understand: it is a method of passing values that can respect the local scope. This ability distinguishes it from being merely a value-passing process algebra, which would be helpful in some contexts but not of much use in applications. The authors describe pi-calculus as being a theory of mobile systems, in that one can use it to understand mobility and to study the patterns executed by mobile systems. They distinguish between two kinds of 'mobility', one being that of 'links' that can move in an abstract space of 'linked processes', while the other deals with 'processes' that can move in an abstract space of linked processes. The (first-order) pi-calculus deals with the first kind of mobility, and does this via the manipulation of 'names' and 'processes.' A 'name' in the pi-calculus is the name of a link, and a process can interact with another one via the names that they share. When a particular process receives a name, it can then interact with processes that were unknown to it. The authors do treat the second kind of mobility in the book in the guise of 'higher-order' pi-calculus.

Of particular importance to the pi-calculus is in the binding of names in a process. Remembering the same concepts in mathematical logic, particularly in the lambda calculus, one speaks of the occurrence of name in a process as 'bound' if it lies within the scope of a binding of occurrence of the name; it is 'free' if it is not bound. The interaction of two processes via a name can only occur if that name occurs freely in both of them. But the pi-calculus also has the notion of 'scope extrusion', wherein the scope of a restricted name is extended to include only the process that receives the name. Therefore in the pi-calculus a restricted name can move as long as it is renamed. The ability of the pi-calculus to do scope extrusion has been one of its major selling points.

Processes no matter how they look syntactically may have essentially the same behavior. The pi-calculus has a few notions of behavioural equivalence and these are discussed in great detail by the authors. A process can be classified according to its 'internal' behavior as well as how it is 'observed' to behave. The authors describe, and then reject, the notions of 'reduction bisimilarity'of two processes, for two processes can be related if they have no internal actions. To mend this triviality, the authors introduce a notion of the 'observable' of a process. The observables of a process are viewed as the collection of names that it can use for sending and for receiving. Using the construction of an 'observability predicate', the reduction bisimilarity relation is modified to that of the 'strong barbed bisimilarity' between two processes. The observability predicate is a kind of measure as to whether a process can perform an input or output action. Two processes are 'strong barbed bisimilar' if they have the same observables and to each internal transition of one there is an internal transition of the other to a process that is strong barbed bisimilar. Using an example as motivation, the authors go on to reject strong barbed bisimilarity as being a satisfactory notion of equivalence of processes. This leads them to the notion of 'strong barbed congruence', where two processes are strong barbed congruent if they are strong barbed bisimilar in all contexts.

For this reviewer, who prefers to view all processes as applications of functions, the most interesting part of the book was Part 6, which deals with the relation between the pi-calclulus and the lambda-calculus, the latter of which has resulted in many successful (functional) programming languages. The authors study how functions in the lambda-calculus can be represented as processes in the pi-calculus. Their discussion is very interesting, in that it sheds light on to what extent the lambda-calculus can be used to model concurrency. The lambda-calculus is traditionally been viewed as one that involves only sequential operations, so this discussion may point the way in using it to deal with concurrent processes. One should not expect that both of these calculi are the same in terms of their semantics, and this is born out in the authors' proof that the semantics of the pi-calculus is strictly finer than the operational semantics of the lambda-calculus. The encoding of the lambda-calculus into the pi-calculus also involves some rather interesting mathematical constructions, such as the Levy-Longo and Bohm trees. The authors use these trees to show that the equality induced by the pi-calculus is the same as that induced by certain models of the lambda-calculus. Functions are therefore processes.

› Go to Amazon.com to see the review  5.0 out of 5 stars