Games, mobile processes, and functions
Guilhem Jaber, Davide Sangiorgi
TL;DR
This paper establishes a tight correspondence between Operational Game Semantics (OGS) and Milner’s encoding of the untyped call-by-value $\lambda$-calculus into the Internal $\pi$-calculus (I$\pi$), showing that for both Alternating and Concurrent OGS variants the induced λ-term semantics coincide with the π-encoded semantics under refined LTSs (including an output-prioritized version). By mapping OGS configurations to I$\pi$ processes and importing up-to techniques, it derives congruence and full abstraction results for $\Lambda_{V}$ (and sketches for call-by-name) with respect to contexts in $\lambda$-calculus extended with store. A key contribution is transferring complete-trace equivalence from OGS to I$\pi$, yielding a robust notion of full abstraction for Milner’s encoding and enabling the transfer of proof techniques between formalisms. The framework further develops Well-Bracketed OGS and a tensor-product operation to handle interleavings and composition, demonstrating that complete-trace equivalences coincide across A-OGS, C-OGS, and WB-OGS, and aligning these with contextual equivalence in typed store-enabled languages. Overall, the work provides a unified, transferable methodology for reasoning about higher-order languages with store and concurrency through the dual lenses of OGS and the $\pi$-calculus.
Abstract
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.