# Determinism and pi-calculus

Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-calculus typically have several possible non-confluent reductions, so one can use the $\pi$-calculus to model non-deterministic concurrency.

Type systems are used to prove certain desirable behaviour of programs. For example, simply typed lambda terms always terminate to a lambda abstraction value (the calculus is strongly normalising). So it's just natural to wonder whether we can find a good type system for $\pi$-calculus such that some of its processes correspond to deterministic computations.

Is there a type system for the $\pi$-calculus probably with types for processes such that processes under certain types are always confluent? Even more, could there be certain types such that their values are processes coming from lambda expressions, e.g. encoded in one of Milner's encodings?

There are plenty such typing systems.

Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy). In (4) the typing system gives a precise interpretation of the simply typed λ-calculus. (5) does the same thing for System F, (6) does the same for the λμ-calculus.

The typing systems in (3, 4, 5, 6) are precise in the sense that the inhabitants of translations of λ-calculus types "are processes coming from lambda expressions", at least up to $\simeq$ (weak typed bisimulation). More precisely, if $\alpha$ is a type in the λ-calculus, and $\Gamma = x_1 : \beta_1, ..., x_n : \beta_n$ is a corresponding typing environment, then the processes $P$ that are typable as

$$\vdash P \triangleright x_1 : \overline{\langle\beta_1\rangle}, ..., x_n : \overline{\langle\beta_n\rangle}, u : (\langle\alpha\rangle)^{\uparrow}$$

are (up to $\simeq$) the translations of λ-terms $M$ with

$$\Gamma \vdash M : \alpha$$

(Here $\langle \alpha \rangle$ is the translation of a λ-type $\alpha$ into π-types, and $\overline{\tau}$ the dualisation of the π-type $\tau$.) The translations are fully abstract in the sense that

$$M =_{\beta\eta} N \quad\text{iff}\quad \langle M \rangle_u \simeq \langle N \rangle_u$$ (Here $\langle M \rangle_u$ is the translation of $M$, located at $u$.) So the embedding is as precise as one can hope for. (NB, I'm skating over some details above, for ease of presentation.) Note that the systems in (3, 4, 5, 6) are closely related -- indeed they are in some sense the same system, although this viewpoint has not yet been published.

If you want a brief summary of how those typing systems ensure confluence, then it is this: they ensure that there is always at most one active output (i.e. an output not under a prefix). This is brutal/syntactic.

Session types (7, 8) can also be used for this purpose, but the correspondence is not that precise, in parts because session types are not as constraining as the types deriving from (1). See (9) as an example where sessions are used to model effects (such as state) in PCF.

Davide Sangiorgi and others have also worked on this problem, see (10) for a summary.

Aside: as the question correctly guesses, λ-calculus can be seen as an especially well-behaved form of message passing, a viewpoint put forward 1976 in Carl Hewitt's pioneering work (11) in the actors tradition. The typing systems above essentially constrain π-calculus so only this well-behaved message passing is typable. Coincidentally, Milner invented the π-calculus in parts to give a formal model of actors. In hindsight, as (12) explains nicely, there is a small mismatch between actors and π-calculi.

1. K. Honda, V. Vasconcelos, N. Yoshida: Secure Information Flow as Typed Process Behaviour.

2. K. Honda, N. Yoshida, A uniform type structure for secure information flow.

3. M. Berger, K. Honda, N. Yoshida: Sequentiality and the Pi-Calculus

4. N. Yoshida, K. Honda, M. Berger: Strong Normalisation in the Pi-Calculus

5. M. Berger, K. Honda, N. Yoshida: Genericity and the Pi-Calculus

6. K. Honda, N. Yoshida, M. Berger: Control in the Pi-Calculus

7. K. Takeuchi, K. Honda, M. Kubo, An Interaction-based Language and its Typing System.

8. K. Honda, V. T. Vasconcelos, M. Kubo, Language Primitives and Type Disciplines for Structured Communication-based Programming.

9. D. Orchard, N. Yoshida, Effects as sessions, sessions as effects.

10. D. Sangiorgi, D. Walker: The π-Calculus: A Theory of Mobile Processes

11. C. Hewitt, Viewing Control Structures as Patterns of Passing Messages.

12. S. Fowler, S. Lindley, P. Wadler, Mixing Metaphors: Actors as Channels and Channels as Actors.

• Fantastic answer. Now I have a a lot to read up on. – Turion Jun 14 '17 at 6:02
• @MartinBerger: One of the major insights I got from your papers (#4 in your list especially) was that linearity wasn't enough to ensure liveness properties. Additionally, we need some way to ensure the causality of communication (ie, that deadlocks arise from cyclic communication dependencies). This is also true for sequential programs (my real interest), but IMO it's harder to understand because what the communication dependencies actually are is either trivial (purely functional programming) or implicit (stateful). – Neel Krishnaswami Jun 14 '17 at 7:42
• @Turion Please feel free to contact me if you have more questions. – Martin Berger Jun 14 '17 at 9:12
• @NeelKrishnaswami Yes, that's one of the reasons why I believe that computation -- including sequential -- is easier to study as message passing. Coincidentally, the causality tracking in (4) is simple, there is no conceptual problem with tracking more complicated causality. But we were not aware of a lambda-calculus where that is needed. – Martin Berger Jun 14 '17 at 9:17