Games, mobile processes, and functionss -- alternating, concurrent, and well-bracketed semantics

技术摘要：博弈、移动进程与函数

问题陈述
本文针对高阶语言两种主要语义框架之间缺乏紧密、形式化对应关系的问题：操作博弈语义（OGS）与$\pi$-演算（特别是内部$\pi$-演算，$I\pi$）。尽管这两种模型都用于刻画$\lambda$-演算项的行为，但它们的构建方式存在显著差异。OGS 提供内射模型，其中程序的指称是从代表与环境交互的配置中组合推导得出的，通常强调交替性和良好括号化等性质。相比之下，$\pi$-演算通过 Milner 的编码将函数建模为进程，利用代数结构和进程等价性（如互模拟）。作者旨在为无类型按值调用$\lambda$-演算（$\Lambda_V$）和按名调用建立这些模型之间精确的操作对应关系，证明它们诱导出相同的行为等价性，并且一种模型中的技术可以转移到另一种模型中。

方法论
作者对$\Lambda_V$在三种不同的 OGS 变体和两种$I\pi$变体下的操作语义进行了比较分析：

1. OGS 变体：
   • 交替 OGS（A-OGS）： 强制程序（玩家）与环境（对手）之间严格交替。
   • 并发 OGS（C-OGS）： 允许在配置中并行运行多个项。
   • 良好括号化 OGS（WB-OGS）： 对延续强制执行栈纪律，限制对手按后进先出顺序进行回答。
2. $I\pi$变体：
   • 标准$I\pi$LTS： 内部$\pi$-演算的标准标记转换系统。
   • 输出优先$I\pi$LTS（opLTS）： 一种受限的 LTS，其中输入动作仅在无待处理的输出或内部动作时才可见，从而强制执行顺序约束。

核心方法论涉及定义从 OGS 配置（包括环境和运行中的项）到$I\pi$进程的映射（$\mathcal{V}$）。该映射扩展了 Milner 对$\lambda$-项的编码。随后，作者证明了操作对应定理，表明在特定条件下，OGS 中的转换对应于$I\pi$中的转换（反之亦然）。至关重要的是，他们利用了从$I\pi$引入的“至”技术（特别是“至上下文”和“至组合”），以简化 OGS 中的互模拟证明。他们还引入了 OGS 配置的张量积来模拟迹的交错，这类似于进程演算中的并行组合。

主要贡献

1. 操作对应： 本文建立了以下两者之间紧密的操作对应关系：

   • A-OGS 与在输出优先LTS（opLTS）下的$I\pi$。
   • C-OGS 与在标准LTS 下的$I\pi$。
     这些对应关系对强转换和弱转换均成立，并利用扩展关系（$\lesssim$）来解释内部归约。

2. 等价性重合： 作者证明，所有这些模型在$\lambda$-项上诱导出行为等价性彼此重合。具体而言：

   • A-OGS、C-OGS 和$I\pi$（包括标准版和 opLTS 版）中的迹等价性和互模拟性在$\Lambda_V$项上定义了相同的关系。
   • 这种诱导出的等价性被确定为Lassen 的急切范式互模拟（通常可视作 Lassen 树）。
   • 对于完整迹（描述终止交互的迹），交替、并发和良好括号化 OGS 的语义也重合。

3. 技术转移：

   • 至组合： 作者将“至上下文”和“扩展”技术从$I\pi$引入到 OGS 中。他们为 OGS 定义了一种名为**“至组合”**的新颖技术，该技术允许将互模拟证明中的复杂配置拆分为基本组件（单例配置）并独立对其进行推理。
   • 同余性与组合性： 通过利用与$I\pi$的对应关系，本文推导出了 OGS 的同余性质（例如，若$M \sim N$，则$C[M] \sim C[N]$），并定义了用于计算迹交错的配置张量积。

4. 存储的全抽象性： 对良好括号化 OGS 中完整迹的研究与带有可变存储的$\lambda$-演算的上下文等价性相关联。本文表明，将$\lambda$-项编码到$I\pi$中，对于用扩展了存储的$\lambda$-演算编写的上下文而言，得出了全抽象结果。

5. 按名调用扩展： 本文概述了无类型按名调用$\lambda$-演算的类似对应关系，表明其诱导出的等价性与Lévy-Longo 树重合。

结果

• 定理 6.7 与 7.3： 建立了在各自 LTS 下 OGS 配置与$I\pi$进程之间的操作对应关系。
• 推论 6.12 与 7.7： 证明了对于$\lambda$-项，A-OGS、C-OGS 和$I\pi$中的迹等价性和互模拟性是相同的。
• 定理 8.1： 直接利用“至组合”技术证明了 C-OGS 互模拟性与 Lassen 的急切范式互模拟性重合。
• 定理 12.2： 证明了完整迹等价性在 WB-OGS、A-OGS 和 C-OGS 之间是相同的。
• 引理 7.16 与定理 7.17： 证明了从$I\pi$引入的“归约与组合至互模拟”对于 C-OGS 的可靠性。

意义
本文声称其主要意义在于建立了 OGS 与$\pi$-演算之间“紧密且精确的对应关系”。这种联系允许在两种模型之间转移结果和技术。具体而言：

• 它使 OGS 能够受益于$\pi$-演算丰富的代数结构和强大的证明技术（如“至”技术），而这些技术直接在博弈论框架内开发往往十分困难。
• 它使$\pi$-演算能够受益于 OGS 与源语言的接近性，以及其在建模特定计算效应（如控制算子或存储）方面的灵活性。
• 它提供了$\lambda$-演算语义的统一视图，表明 OGS 中的“语义立方”条件（交替性、良好括号化）与$I\pi$中的顺序约束（通过 opLTS）是同一枚硬币的两面，两者都刻画了相同的基础行为等价性（按值调用的 Lassen 树）。

作者指出，虽然博弈语义与进程演算之间的类比此前已有探索（例如将策略翻译为进程），但本工作的独特之处在于直接比较了函数的解释，并系统地转移证明技术以推导 OGS 的新结果。