完全抽象规范形式的双模拟在按值传递的程序计算框架（PCF）中的应用

《Journal of the ACM》：Fully Abstract Normal Form Bisimulation for Call-by-Value PCF

本文首次提出基于标签迁移系统的完全抽象正常形式双模拟方法，结合应用双模拟、环境双模拟和博弈语义，通过构建对应交互轨迹避免语义商取，实现PCF调用值递归式程序等价性检查工具，并验证了其在已知和新案例中的有效性。

　　

摘要

我们首次提出了针对按值调用（call-by-value）的PCF（PCF${}_{\text{v}}$的完全抽象正规形式双模拟（fullly abstract normal form bisimulation）。我们的模型基于一种标记转换系统（LTS），该系统结合了应用双模拟（applicative bisimulation）、环境双模拟（environmental bisimulation）和游戏语义（game semantics）的元素。为了在不使用语义商（semantic quotienting）的情况下实现完备性，LTS构建了与可能的功能上下文（functional contexts）交互相关的轨迹。该模型为检查PCF${}_{\text{v}}$程序的等价性提供了一种可靠且完备的方法，我们将其实现在一个有界双模拟检查工具（bounded bisimulation checking tool）中。我们通过文献中已知的等价性示例以及新的示例对该工具进行了测试。