Реализация унификации и пропуска переменных

Я работаю над реализацией обычного алгоритма унификации обычным способом: рекурсивный спуск по деревьям выражений, попутно добавляя привязки переменных к хеш-таблице, выполняя проверку возникновения. В 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;
}

Эта версия правильная и для многих случаев довольно быстрая, но у нее есть проблема, которая возникает, в частности, при ее использовании для вывода типов. При объединении множества переменных с одной и той же целью получается набор привязок, который в основном выглядит следующим образом:

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

Затем каждый раз, когда новая переменная должна быть объединена с одним и тем же объектом, она должна проходить по цепочке один шаг за раз, чтобы найти, где она находится на данный момент, что занимает время O (N), что означает объединение коллекции переменных для то же самое занимает общее время O (N ^ 2).

Вероятно, лучшее решение - реализовать какой-то ярлык, что-то вроде обновления a, чтобы он указывал непосредственно на текущую конечную цель, какой бы она ни была. Не совсем очевидно, как это сделать правильно и эффективно во всех случаях.

Унификация была хорошо известна и довольно широко использовалась в течение десятилетий, поэтому я полагаю, что решение этой проблемы также должно было быть известно в течение десятилетий, но несколько обсуждений, которые я видел по поводу объединения, похоже, не упоминают об этом.

Как именно можно изменить алгоритм, чтобы справиться с этим?


java performance algorithm unification
person rwallace    schedule 20.01.2018    source источник
comment
Понятия не имею (на первый взгляд), но отлично вопрос!   -  person Elliott Frisch    schedule 20.01.2018

Ответы (2)


arrow_upward
2
arrow_downward

Я согласен с тем, что сокращение - правильный подход. Вы должны иметь возможность изменить это:

    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 удаляет только один уровень косвенного обращения, но поскольку вы делаете это сразу после рекурсивного вызова, который также будет вырезать любое ненужное косвенное обращение, вы знаете, что существует только один уровень косвенного обращения от к < / em> вырезано.)

Это не полностью предотвращает цепочки, потому что можно объединить a с b и затем b с c и так далее; но каждая цепочка полностью обрабатывается при первом повторном обнаружении, поэтому вы все равно получаете амортизированное постоянное время.

person ruakh    schedule 20.01.2018
comment
Думаю, это в принципе правильный ответ! Единственное предостережение: каждому вызову map.put должна предшествовать проверка, чтобы убедиться, что map.get не равен нулю. Я думаю, это связано с тем, что рекурсивный вызов мог просто объединить переменную с самой собой, не оставив новой привязки. С этим дополнением он проходит мои модульные тесты и работает намного быстрее. - person rwallace; 21.01.2018

arrow_upward
2
arrow_downward

Вот идея: все вары, связанные =, являются классом эквивалентности. Итак, вы можете сделать карту

unify(Term a, Map<VarClass, Term> map) {...

где VarClass реализован с помощью классического алгоритма поиска объединения для непересекающихся множеств.

Когда вы обнаружите пару переменных x=y, которую вы ранее добавляли на карту, вместо этого добавьте x к VarClass, содержащему y (создавая пару и добавляя ее с изменяемым отображением пустого заполнителя, если его еще нет).

Term в правой части карты никогда не будет Var.

Операции объединения-поиска для всех практических целей амортизируются за постоянное время и довольно быстрые на практике.

person Gene    schedule 20.01.2018