Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms

Davide Sangiorgi

Abstract: We study mobile systems, i.e. systems with a dynamically changing communication topology, from a process algebras point of view. Mobility can be introduced in process algebras by allowing names or terms to be transmitted. We distinguish these two approaches as first-order and higher-order. The major target of the thesis is the comparison between them.

The prototypical calculus in the first-order paradigm is the pi-calculus. By generalising its sort discipline we derive an w-order extension called Higher-Order pi-calculus (HO-pi). We show that such an extension does not add expressiveness to the pi-calculus: Higher-order processes can be faithfully compiled down to first-order, and respecting the behavioural equivalence we adopted in the calculi. Such an equivalence is based on the notion of bisimulation, a fundamental concept of process algebras. Unfortunately, the standard definition of bisimulation is unsatisfactory in a higher-order calculus because it is over-discriminating. To overcome the problem, we propose barbed bisimulation. Its advantage is that it can be defined uniformly in different calculi because it only requires that the calculus possesses an interaction or reduction relation. As a test for barbed bisimulation, we show that in CCS and pi-calculus, it allows us to recover the familiar bisimulation-based equivalences. We also give simpler characterisations of the equivalences utilised in HO-pi. For this we exploit a special kind of agents called triggers, with which it is possible to reason fairly efficiently in a higher-order calculus notwithstanding the complexity of its transitions.

Finally, we use the compilation from HO-pi to pi-calculus to investigate Milner's encodings of lambda-calculus into pi-calculus. We present analogous encodings of lambda-calculus into HO-pi. By comparison with those into pi-calculus, these are easier to understand and with a closer correspondence between reduction on lambda-terms and on their process counterparts. We show that the two encodings of lazy lambda-calculus and the compilation from HO-pi to pi-calculus commute. Thus we can reason in HO-pi and the results hold for pi-calculus as well. In this way we are able to derive a direct characterisation of the equivalence upon lambda-terms induced by Milner's encoding and by the behavioural equivalence adopted on the process terms.

From the representability result of HO-pi in pi-calculus we conclude that the first-order paradigm, which enjoys a simpler and more intuitive theory, should be taken as basic. Nevertheless, the study of the lambda-calculus encodings shows that a higher-order calculus can be very useful for reasoning at a more abstract level.

LFCS report ECS-LFCS-93-266 (also published as CST-99-93)

Previous | Index | Next