我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：证明按值调用 λ-演算编码进两个 π-演算子演算后，所诱导的项等价恰为含 η-等式的 Lassen 急切范式互模拟。

本文重新审视 Milner 将按值调用（call-by-value）λ-演算编码到 π-演算的经典工作。作者通过把编码精细地调整到两个 π-演算子演算——Internal π 与 Asynchronous Local π——使得编码在 λ-项上诱导的等价关系恰好与 Lassen 的急切范式互模拟（eager normal-form bisimilarity）重合，并且该对应关系可扩展以处理 η-等式。在 π-演算一侧，作者以上下文等价（contextual equivalence）和 barbed congruence 作为行为等价的标准，证明了编码是可靠且完备的：两个 λ-项在上述行为等价下不可区分，当且仅当它们在扩展后的急切范式互模拟下等价。文中进一步把结果从前述等价关系推广到相应的前序（preorder），从而给出按值调用函数式计算与并发进程行为之间更完整的语义对应图景。

问题

Milner 的按值调用 λ-演算到 π-演算编码所诱导的 λ-项等价关系究竟是什么，能否与已知的按值调用行为等价（Lassen 的急切范式互模拟）精确对应。

方法

把编码调整到两个 π-演算子演算（Internal π 与 Asynchronous Local π），以 π-演算的上下文等价和 barbed congruence 作为行为等价，并借助互模拟论证建立对应，进而将结论从前述等价扩展到前序并纳入 η-等式。

评估

通过理论证明（互模拟与上下文等价/bar bed congruence 的对应定理）给出编码的可靠性与完备性，并考察加入 η-等式后的情形。

链接与引用

DOI 原文 · PDF（开放获取） ·

@inproceedings{paperbot4387,
  title = {Eager Functions as Processes},
  author = {Adrien Durier and Daniel Hirschkoff and Davide Sangiorgi},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209152}
}