java - 实现统一和跳过变量

我正在以通常的方式实现通常的统一算法:通过表达式树递归下降，沿途向哈希表添加变量绑定(bind)，进行发生检查。碰巧在 Java 中，使用覆盖函数来配合语言的粒度，因此处理变量的实现部分是:

@Override
public boolean unify(Term a, Map<Var, Term> map) {
    if (this == a) {
        return true;
    }
    Term x = map.get(this);
    if (x != null) {
        return x.unify(a, map);
    }
    if (a instanceof Var) {
        x = map.get((Var) a);
        if (x != null) {
            return x.unify(this, map);
        }
    }
    if (a.occurs(this)) {
        return false;
    }
    map.put(this, a);
    return true;
}

这个版本是正确的，而且在许多情况下相当快，但它有一个问题，特别是在使用它进行类型推断时。当将许多变量统一到同一个目标时，它最终会得到一组基本上如下所示的绑定(bind):

a=b
b=c
c=d
d=e

然后每次必须将一个新变量统一到同一事物上时，它必须一次一步地遍历链以找到它现在所处的位置，这需要 O(N) 时间，这意味着将一组变量统一为同样的事情需要总时间 O(N^2)。

可能最好的解决方案是实现某种快捷方式，类似于更新 a 以直接指向当前最终目标，无论可能是什么。如何以一种在所有情况下都正确和有效的方式来做到这一点并不完全显而易见。

几十年来，统一已经广为人知并得到了相当广泛的应用，所以我想解决这个问题的解决方案也应该已经知道了几十年，但是我看到的关于统一的几次讨论似乎没有提到它。

究竟有什么方法可以修改算法来处理呢？

最佳答案

我同意捷径是正确的方法。你应该能够改变这一点:

    return x.unify(a, map);

对此:

    if (! x.unify(a, map)) {
        return false;
    }
    map.put(this, map.get(x));
    return true;

和这个:

        return x.unify(this, map);

对此:

        if (! x.unify(this, map)) {
            return false;
        }
        map.put(a, map.get(x));
        return true;

(每个单独的 map.put 只删除一级间接，但是因为您在递归调用之后立即执行它也会删除任何不必要的间接，所以您知道只有一级间接可以删除。)

这并不能完全阻止链，因为可以将 a 与 b 统一，然后将 b 与 c 统一，依此类推；但是每条链在第一次再次遇到时都会得到充分处理，因此您仍然可以摊销固定时间。

关于java - 实现统一和跳过变量，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/48352156/