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.

翻译：我们建立了λ-演算两种模型之间的紧密联系，即米尔纳向π-演算（具体而言，内部π-演算）的编码与操作博弈语义（OGS）。我们首先研究π编码与OGS行为之间的操作对应关系。为此，我们考虑了多种标记转移系统：π的标准LTS与OGS的新型“并发”LTS；π的“输出优先”LTS与OGS的标准交错LTS。随后证明，通过所有这些LTS（针对π和OGS）在λ-项上诱导的等价关系是一致的。我们还证明，当等价性基于完全迹时，OGS的“并发”与“交错”变体同样与“良括号”变体一致。这些联系使我们得以在π与OGS之间移植结果和技术：将π中的“up-to”技术引入OGS；从π的结论推导OGS的相容性与组合性结果；将OGS中的完全迹概念移植到π上，从而获得一种新的行为等价性，该等价性对带有存储扩展的λ-演算语境下λ-项的编码给出了完全抽象结果。本研究分别对传值调用和传名调用进行了阐述。