Amb扩展λ演算的WHNF模拟：共归纳证明与程序等价

"该论文深入探讨了麦卡锡的Amb扩展λ-演算在理论计算机科学中的应用。Amb是麦卡锡提出的一种并行评估形式，它在函数式编程中展现出强大的表达力，不仅包含不规则选择、可数选择（随机分配）和并行或等其他著名非确定性和并行编程语言特性。论文主要关注的是Amb如何增强λ-calculus的模拟等价，特别是与共归纳证明原理相结合，这对于建立程序间的精细关系和非平凡等价至关重要。 作者首先回顾了相关研究，强调了Amb在λ-演算中的地位，以及它与Levy-Longo树等价理论的关系。Levy-Longo树是处理不确定性和并行性的重要工具，论文将其扩展到了带有Amb的按名调用λ-演算中。作者引入了弱头范式（whnf）相似性和模拟等价的概念，这两个概念构成了程序精化和等价性推理的基础。 whnf相似性被证明是一种预同余关系，这使得它成为Lévy-Longo树理论在λ-演算中的一个强化版本。同时，whnf模拟等价提供了一种更精确的判断标准，它能区分上下文等价无法区分的某些非确定性分支行为，这在Kleene等价和成本等价的基础上有所提升，避免了不必要的语法和运算上的区别。 论文结构上，第一部分概述了相关领域的研究背景，第二部分详细介绍了Amb的语法和操作语义，以及上下文修饰和等价关系的定义。第三部分则扩展了操作语义，而在第四部分，whnf相似性和模拟等价的理论被进一步发展和应用。 这篇论文的主要贡献在于为理解和比较带有Amb的λ-演算程序提供了新的精炼和等价性分析框架，这对于理解和设计并行和非确定性编程语言具有重要意义。通过论文中的方法，研究者可以更好地处理复杂程序间的相互关系，推动了理论计算的边界。”