一阶公式中变量的有效重命名

Question

编辑₂：考虑到 de Bruijn 指数可能更容易使用，我重新制定了公式的大部分内部表示形式，以使用混合 de Bruijn 表示< em>ala Connor McBride 的论文。这极大地简化了一些必须处理 α 等价的语法算法，但也使其他算法变得更加复杂。无论如何，这意味着自由变量可以被标准化，而绑定变量具有由其绑定距离表示的规范名称。这并不完全令人满意，但至少是一个更好的开始。

编辑₁：我意识到问题约束不足以保证变量的标准化。特别是，量词的迭代意味着绑定器中的变量必须首先标准化。因此，可能无法避免需要多次遍历每个抽象语法树的解决方案。使用 de Bruijn 指数的建议通常是一个相当好的解决方案，但它不会在不破坏符号及其实用性的情况下轻松实现标准化。

原文： 设V是由自然数索引的无限变量集，fv(φ)表示φ的自由变量，bv(φ ) 表示 φ 的约束变量，对于任何一阶公式 φ。我试图解决的问题如下。

设 φ 和 ψ 为一阶公式。找到替换 θ₁ 和 θ₂ 使得： (a) fv(θ₁(φ))， fv(θ₂(φ))、bv(θ₁(φ)) 和 bv(θ₂(ψ)) 是不相交； (b) fv(θ₁(φ)), fv(θ₂(φ)) 的并集)、bv(θ₁(φ)) 和 bv(θ₂(ψ)) 是同构的到自然数的初始段； (c) bv(θ₁(φ)) 中的所有变量均小于 bv(θ_{2< /sub>(ψ)) 小于 fv(θ1(ψ)) 中的所有变量 小于 fv( θ2(ψ))。}

困难在于公式中的绑定变量和自由变量集不一定是不相交的，并且量词可能会迭代，这意味着朴素替换会产生意外的变量捕获，等等。

一个低效的解决方案如下。给定 φ 和 ψ，首先将 φ 和 ψ 的自由变量标准化，使得标准化项中的所有自由变量都大于最大绑定变量加上 φ 和 ψ 中的绑定算子的数量，得到 φ' 和 ψ'。然后从 x₀ 开始重命名 φ' 的绑定变量。然后是ψ'的绑定变量。然后是 φ' 的自由变量。然后是ψ'的自由变量。

我想要的是一种更有效的方法来满足问题约束。也就是说，解决方案不需要重命名自由变量的初始标准化。有效地标准化变量并不是问题。然而，额外的限制给我带来了麻烦。

Answer 1

一定要使用 De Bruijn idices。另外，请注意它们都是积极的。然后您可以在统一过程中使用负数。如果您想使用新索引，请使用全局索引。