改进的豪方法：解决函数式语言应用相似性预同余问题

Howe方法是理论计算机科学领域的一种重要工具，特别在证明函数式编程语言中不同概念之间相似性或双相似性的有效性上。首次由Paul Brian Levy在2006年的《电子笔记在理论计算机科学》(Electronic Notes in Theoretical Computer Science)第164期85-104页中提出，该方法通过构造特定性质的扩展来确保关系的同余或预同余性，这对于理解语言之间的模拟和互模拟至关重要。 在确定性语言中，豪氏方法起源于对并发理论中模拟和互模拟概念的模仿。豪方法不同于早期的指称方法，它采用了一种纯操作技术，通过扩展一个初始关系到一个兼容且具备模拟性质的关系，从而证明应用相似性和双相似性是预同余的。这使得豪方法成为处理确定性λ-演算的有效手段。 然而，豪方法的一个局限在于它要求语言的语法必须是无穷的，这导致了无法处理具有可数类型和有限语法的语言。这种限制曾引发了不少讨论。本研究的创新之处在于作者提出了“无限豪方法”（Infinite Howe Method），它巧妙地规避了这一问题，通过定义两个扩展的原始关系的相互coinduction，这两个扩展都保留了豪扩展的核心特性。 在第一部分，研究者展示了无限豪方法如何在具有可数类型和按值调用的确定性语言环境中运作，即使在有限语法的情况下也能保持有效性。在第二部分，他们进一步探讨了这种方法在语法变得非良基时的情况，即使用混合归纳/共归纳的参数，证明了各种形式的应用相似性和bisimilarity仍然可以被不同的上下文所保真。 关键词：“豪方法”、“确定性语言”、“应用模拟”、“预同余”、“无限豪方法”、“可数类型”和“coinduction”共同构成了这篇文章的核心内容，它不仅解决了豪方法的传统局限，而且为理解和证明函数式语言的相似性提供了新的视角和工具。