The Fusion Calculus:
Expressiveness and Symmetry
in Mobile Processes

Björn Victor

Abstract

The fusion calculus is presented as a significant step towards a canonical calculus of concurrency. It simplifies and extends the pi-calculus of Milner, Parrow and Walker.

The fusion calculus contains the polyadic pi-calculus as a proper subcalculus and thus inherits all its expressive power. In addition fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models with shared state, including concurrent constraint formalisms. It is also easy to represent the so called strong reduction strategies in the lambda-calculus, involving reduction under abstraction. In the pi-calculus these tasks require elaborate encodings.

The fusion calculus simplifies the pi-calculus by reducing the number of binding operators and the number of bisimulation equivalences, and by making input and output symmetric like in pure CCS. We attain a calculus where concepts from other models of computation are more easily expressed than in the pi-calculus, thereby taking a step towards a unified yet simple model of computation.

In this thesis we present a broad foundational theory of the fusion calculus. We define its labelled and unlabelled operational semantics, and treat strong and weak bisimulation equivalences for both semantics in some detail, including complete axiom systems for finite terms. The equivalences are given symbolic characterizations, leading to algorithms and an automatic tool for equivalence checking. We demonstrate the expressive power of the fusion calculus to give simple encodings of foundational calculi for functional and concurrent constraint programming.


Last modified: Mon, 08-Jun-1998 15:44 MEST | URL http://user.it.uu.se/~victor/thesis-abstract.shtml
© Björn Victor 1998