编辑2: 得知de Bruijn指数可能更易于处理，我已经重新构建了公式的内部表示形式，使用混合de Bruijn表示法，这与Connor McBride的论文类似。这极大地简化了一些涉及α等价性的语法算法，但使其他算法更加复杂。无论如何，这意味着自由变量可以被标准化，并且绑定变量具有由其绑定距离表示的规范名称。这并不完全令人满意，但至少是一个更好的开始。
编辑1: 我意识到问题约束条件不足以保证变量的标准化。特别是，量词的迭代意味着必须首先将绑定器中的变量标准化。因此，可能没有逃避需要对每个抽象语法树进行多次遍历的解决方案。使用de Bruijn指数的建议通常是相当好的解决方案，但它不会轻易地给出标准化，而不破坏符号和其实用性。
原始内容: 设 V 为自然数索引的无限变量集合，fv(φ) 表示公式 φ 的自由变量，bv(φ) 表示公式 φ 的绑定变量。我要解决的问题是：
设 φ 和 ψ 是一阶公式。找到替换 θ1 和 θ2 使得： (a) fv(θ1(φ)), fv(θ2(φ)), bv(θ1(φ)) 和 bv(θ2(ψ)) 互不相交; (b) fv(θ1(φ)), fv(θ2(φ)), bv(θ1(φ)) 和 bv(θ2(ψ)) 的并集同构于自然数的一个初始段; 以及 (c) 所有在θ1(φ)中的变量都小于所有在θ2(ψ)中的变量，而这些又都小于所有在fv(θ1(ψ)) 中的变量，这些又都小于所有在fv(θ2(ψ)) 中的变量。
困难在于公式中的绑定变量和自由变量集合不一定互不相交，量词可能会迭代，这意味着简单的替换会产生意外的变量捕获等问题。
一个低效的解决方案是：给定φ和ψ，首先将φ和ψ的自由变量标准化，使标准化后的项中所有自由变量均大于最大限制变量加上φ和ψ绑定运算符的数量，得到φ'和ψ'。然后从x0开始重命名φ'的绑定变量，再重命名ψ'的绑定变量，接着重命名φ'的自由变量，最后重命名ψ'的自由变量。我需要的是一个更有效的方法来满足问题的约束条件，即不需要重命名自由变量的初始标准化方法。高效地分离变量并不是问题，但附加约束条件让我苦恼。