From π-calculus to higher-order π-calculus — and back

Abstract

We compare the first-order and the higher-order paradigms for the representation of mobility in process algebras. The prototypical calculus in the first-order paradigm is the π-caleulus. By generalising its sort mechanism we derive an ω-order extension, called Higher-Order π-calculus. We give examples of its use, including the encoding of λ-calculus. Surprisingly, we show that such an extension does not add expressiveness: Higher-order processes can be faithfully represented at first order. 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 λ-calculus encodings shows that a higher-order calculus can be very useful for reasoning at a more abstract level.