nLab pi-calculus

Context

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

The π\pi-calculus is a computational model for concurrent processes that communicate messages through named channels. It subsumes λ-calculus.

In the monadic (here meaning: unary) π\pi-calculus, outputs and inputs only send and receive single names, while the polyadic (here meaning: n n -ary) π\pi-calculus allows outputs of tuples of names and corresponding inputs.

This calculus permits non-confluent reductions by design, as opposed to other process calculi such as the Interactive Lambda Calculus (ILC).

Syntax

A process is either:

  • an inactive process 00;
  • the parallel composition of two processes PQP\mid Q;
  • the replication of a process !P!P;
  • a restriction (νn)P(\nu n)\,P (that is the generation of a fresh name only known to PP);
  • prefixed by an input n(m).Pn(m).P;
  • prefixed by an output n¯m.P\overline{n}\langle m\rangle.P.

Sometimes an indeterministic choice operator ++ is added to the syntax.

Example

  • a server that increments the value it receives: S=!incr(a,x).a¯x+1S=!\mathrm{incr}(a,x).\overline{a}\langle x+1\rangle;
  • a client that calls to the incr\mathrm{incr} server: C=(νa)(incr¯a,4a(y))C=(\nu a)\bigl(\overline{\mathrm{incr}}\langle a,4\rangle\mid a(y)\bigr);
  • the final process by composing the server and the client: SCS\mid C.

Reduction-based operational semantics

The central reduction rule of the π\pi-calculus is the following:

n¯a.Pn(b).QPQ ab.\overline{n}\langle a\rangle.P\mid n(b).Q\longrightarrow P\mid Q_{a\mapsto b}\,.

Typed π\pi-calculus

Several attempts have been made to give the π\pi-calculus typing systems. It is crucial for HOπ\mathrm{HO}\pi, a higher-order π\pi-calculus in which messages can be processes themselves.

Simple types

Simple types are defined by the following grammar:

TT˜T\longrightarrow\sharp\widetilde{T}

where T˜\widetilde{T} ranges over (possibly empty) tuples of simple types.

Typing contexts? are lists of hypotheses of the form n:Tn:T where nn is a channel name and TT is a simple type.

Simply typed π\pi-calculus corresponds to a distributed logic?: using a property proven at some place supposes therefore a call to that property under a name. Theorems can be used many times, but lemmas are limited to one use.

TypingIntuitive signification
a(x,y).P:p,qra(x,y).P:p,q\to rLemma 1. Under hypotheses pp, qq, then rr.
a¯M,N:r\overline{a}\langle M,N\rangle:rUse Lemma 1, knowing that pp and qq, to prove rr.

Session types

Session types were introduced by Kohei Honda. A session links exactly two subprocesses that interact with each other, and multiple sessions can run simultaneously.

Example

The process x(n).x¯n+1.0x(n).\overline{x}\langle n+1\rangle.0 may be given type x:?int.!int.endx:?\mathsf{int}.!\mathsf{int}.\mathsf{end}.

Caires and Pfenning 2010 established a correspondence between dual intuitionistic linear logic? (DILL) and session typed π\pi-calculus. Later on, Wadler 2012 established a correspondence between classical linear logic (CLL) and the same calculus.

Other process calculi

The Calculus of Communicating Systems (CCS) is an important predecessor of the π-calculus. It can be seen as a restriction of π in which only a dummy name ww is exchanged in communications, and ww cannot be used in subject position (Hirschkoff 2003).

References

  • Robin Milner, Joachim Parrow and David Walker, A Calculus of Mobile Processes, Information and Computation, 100 (1992) 1-40.
  • Peter Sewell, Applied π\pi – A Brief Tutorial, (2000) (pdf).
  • Jeannette M. Wing, FAQ on π\pi-Calculus, (2002) (pdf).
  • Daniel Hirschkoff, A brief survey of the theory of the π\pi-calculus, (2003) (pdf).
  • Pierre-Louis Curien, Introduction to CCS and pipi-calculus, (2003) (ps).

On types:

  • Kohei Honda, Types for dyadic interaction, 4th International Conference on Concurrency Theory (1993) 509–523.
  • Noël Bernard, Investigating the Logical Aspects of the Pi-calculus, Schedae Informaticae, 12 (2003) 57-66 (hal-00386109).
  • Luís Caires and Frank Pfenning, Session Types as Intuitionistic Linear Propositions, 21st International Conference on Concurrency Theory (2010) 222-236 (pdf).
  • Philip Wadler, Propositions as Sessions (pdf, doi:10.1145/2398856.2364568).

Other process calculi:

  • Kevin Liao, Matthew A. Hammer and Andrew Miller, ILC: A Calculus for Composable, Computational Cryptography, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, (2019) 640-654 (doi:10.1145/3314221.3314607, pdf).

Last revised on March 8, 2024 at 11:21:47. See the history of this page for a list of all contributions to it.