The Polyadic π-Calculus: a Tutorial

The Polyadic π-Calculus: a Tutorial

October 1991 | Robin Milner
The π-calculus is a model of concurrent computation based on the concept of naming. It is introduced in its simplest form, with examples, and then generalized from monadic to polyadic. The semantics are defined using a reduction system and labelled transitions called commitment. The paper presents the algebraic axiomatization of strong bisimilarity and a characterization in modal logic. Theorems about the replication operator are also proved. The polyadic form is justified by the concepts of sort and sorting, which it supports. Examples of different sortings are given, including the representation of data structures as processes that respect a particular sorting and the sorting for a known translation of the λ-calculus into the π-calculus. The equational validity of β-conversion is proved using replication theorems. The paper also extends the π-calculus to ω-order processes and discusses the encoding of higher-order processes in first-order. The paper introduces the concepts of sort and sorting, which are analogous to the simple type hierarchy in the λ-calculus but with significant differences. Data structures are shown to be represented as a particularly well-behaved class of processes that respect a distinctive sorting discipline. The paper also discusses the encoding of the λ-calculus into the π-calculus and provides a simple proof of the validity of β-conversion in this interpretation. The paper explores higher-order processes, extending the work of Thomsen. It shows how sorts and sorting extend naturally to second-order processes and even to ω-order processes. A theorem by Sangiorgi is given, asserting that ω-order processes can be faithfully encoded in the first-order π-calculus. The paper also discusses the use of structural congruence and reduction rules in the π-calculus, and provides examples of processes and their reductions. The paper concludes with a discussion of the theoretical and practical implications of the π-calculus for modeling concurrent computation.The π-calculus is a model of concurrent computation based on the concept of naming. It is introduced in its simplest form, with examples, and then generalized from monadic to polyadic. The semantics are defined using a reduction system and labelled transitions called commitment. The paper presents the algebraic axiomatization of strong bisimilarity and a characterization in modal logic. Theorems about the replication operator are also proved. The polyadic form is justified by the concepts of sort and sorting, which it supports. Examples of different sortings are given, including the representation of data structures as processes that respect a particular sorting and the sorting for a known translation of the λ-calculus into the π-calculus. The equational validity of β-conversion is proved using replication theorems. The paper also extends the π-calculus to ω-order processes and discusses the encoding of higher-order processes in first-order. The paper introduces the concepts of sort and sorting, which are analogous to the simple type hierarchy in the λ-calculus but with significant differences. Data structures are shown to be represented as a particularly well-behaved class of processes that respect a distinctive sorting discipline. The paper also discusses the encoding of the λ-calculus into the π-calculus and provides a simple proof of the validity of β-conversion in this interpretation. The paper explores higher-order processes, extending the work of Thomsen. It shows how sorts and sorting extend naturally to second-order processes and even to ω-order processes. A theorem by Sangiorgi is given, asserting that ω-order processes can be faithfully encoded in the first-order π-calculus. The paper also discusses the use of structural congruence and reduction rules in the π-calculus, and provides examples of processes and their reductions. The paper concludes with a discussion of the theoretical and practical implications of the π-calculus for modeling concurrent computation.
Reach us at info@futurestudyspace.com
Understanding The Polyadic %CF%80-Calculus%3A a Tutorial