edit2: 考虑到 de Bruijn 指数可能更易于使用，我重新制定了公式的大部分内部表示形式以使用混合 de Bruijn 代表 ala Connor McBride 的论文。这极大地简化了一些与必须处理 α-等价性的语法相关的算法，但也使其他算法变得更加复杂。无论如何，这意味着自由变量可以被标准化分开，而绑定(bind)变量具有由它们的绑定(bind)距离表示的规范名称。这并不完全令人满意，但至少是一个更好的开始。
edit1:我意识到问题约束不足以保证变量的标准化。特别是，量词的迭代意味着绑定(bind)器中的变量必须首先标准化。因此，可能无法避免需要多次遍历每个抽象语法树的解决方案。使用 de Bruijn 索引的建议通常是一个相当不错的解决方案，但它不会在不破坏符号及其实用性的情况下轻松实现标准化。
原创: 设 V 为由自然数索引的无限变量集，fv(φ) 表示 φ 的自由变量，bv(φ ) 表示 φ 的约束变量，对于任何一阶公式 φ。我要解决的问题如下。
Let φ and ψ be first-order formulae. Find substitutions θ1 and θ2 such that: (a) fv(θ1(φ)), fv(θ2(φ)), bv(θ1(φ)), and bv(θ2(ψ)) are disjoint; (b) the union of fv(θ1(φ)), fv(θ2(φ)), bv(θ1(φ)), and bv(θ2(ψ)) is isomorphic to an initial segment of the natural numbers; and (c) all variables in bv(θ1(φ)) are less than all variables in bv(θ2(ψ)) are less than all variables in fv(θ1(ψ)) are less than all variables in fv(θ2(ψ)).
困难在于公式中的绑定(bind)变量和自由变量集不一定不相交，并且量词可能会迭代，这意味着天真替换会产生意外的变量捕获，等等。
下面是一个低效的解决方案。给定 φ 和 ψ，首先将 φ 和 ψ 的自由变量标准化，使得标准化项中的所有自由变量大于最大绑定(bind)变量加上 φ 和 ψ 中的绑定(bind)运算符的数量，给出 φ' 和 ψ'。然后从 x0 开始重命名 φ' 的绑定(bind)变量。然后是 ψ' 的约束变量。然后是 φ' 的自由变量。然后是ψ'的自由变量。
我想要的是一种更有效的方法来满足问题约束。也就是说，不需要重命名自由变量的初始标准化的解决方案。有效地将变量标准化不是问题。但是，额外的约束给我带来了麻烦。
最佳答案
请务必使用 De Bruijn 指数。另外，请注意它们都是正面的。然后你可以在统一过程中使用负数。如果您想使用新索引，请使用全局索引。
关于performance - 一阶公式中变量的有效重命名，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/7764032/