二阶抽象语法的E-一致化
摘要：高阶一致化(HOU)涉及λ-演算的扩展的一致化，可以看作是对λ-项的η-等价关系进行等式一致化(E-一致化)的一个实例。我们研究了在具有任意变量绑定构造的语言中，对项进行等式一致化，同时考虑任意二阶等式理论。具有通用变量绑定和参数化元变量的抽象语法使得我们可以处理任意的绑定器，而无需专注于λ-演算或使用不便且易于出错的项编码，从而建立起更灵活的框架。本文介绍了对二阶抽象语法的E-一致化，并描述了一种解决这类问题的一致化过程，合并了全面的HOU和通用的E-一致化的思想。我们证明了该过程是正确且完备的。
作者：Nikolai Kudasov
论文ID：2302.05815
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-08