Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics
For researchers in semantics of programming languages, this work unifies two major models of computation, enabling cross-fertilization of techniques.
This paper establishes a tight connection between Milner's encoding of the λ-calculus into the π-calculus and operational game semantics (OGS), showing that the behavioural equivalences induced by various labelled transition systems coincide. This allows transferring results and techniques between the two models, including a new full abstraction result for λ-terms with store.
We establish a tight connection between two models of the $λ$-calculus, namely Milner's encoding into the $π$-calculus (precisely, the Internal $π$-calculus), and operational game semantics (OGS). We first investigate the operational correspondence between the behaviours of the encoding provided by $π$ and OGS. We do so for various LTSs: the standard LTS for $π$ and a new `concurrent' LTS for OGS; an `output-prioritised' LTS for $π$ and the standard alternating LTS for OGS. We then show that the equivalences induced on $λ$-terms by all these LTSs (for $π$ and OGS) coincide. We also prove that when equivalence is based on complete traces, the `concurrent' and `alternating' variants of OGS also coincide with the `well-bracketed' variant. These connections allow us to transfer results and techniques between $π$ and OGS. In particular: we import up-to techniques from $π$ onto OGS; we derive congruence and compositionality results for OGS from those of $π$; we transport the notion of complete traces from OGS onto $π$, obtaining a new behavioural equivalence that yields a full abstraction result for the encoding of $λ$-terms with respect to contexts written in a $λ$-calculus extended with store. The study is illustrated for both call-by-value and call-by-name.