С дополнительными сведениями о том, с чем связана необходимость в стандартизации отличия.

Возникает еще одна сложность: выше было сказано, что алгоритм Unify должен возвращать такую подстановку (или унификатор), в результате которой два параметра становятся одинаковыми. Но количество таких унификаторов может быть больше единицы. Например, вызов алгоритма Unify {Knows (John, x) , Knows {у, z) ) может возвратить [у/John,χ/z} или {у/ John, x/ John, z/ John]. Первый унификатор позволяет получить в качестве результата унификации выражение Knows {John, z), а второй дает Knows {John, John). Но второй результат может быть получен из первого с помощью дополнительной подстановки {z/John}] в таком случае принято считать, что первый унификатор является более общим по сравнению со вторым, поскольку налагает меньше ограничений на значения переменных. Как оказалось, для любой унифицируемой пары выражений существует единственный наиболее общий унификатор (Most General Unifier— MGU), который является уникальным вплоть до переименования переменных. В данном случае таковым является {у/ John, x/ z}.

Алгоритм вычисления наиболее общих унификаторов приведен в листинге 9.1. Процесс его работы очень прост: рекурсивно исследовать два выражения одновременно, "бок о бок", наряду с этим формируя унификатор, но создавать ситуацию неудачного завершения, если две соответствующие точки в полученных таким образом структурах не совпадают. При этом существует один дорогостоящий этап: если переменная согласуется со сложным термом, необходимо провести проверку того, встречается ли сама эта переменная внутри терма; в случае положительного ответа на данный вопрос согласование оканчивается неудачей, поскольку невозможно сформировать какой-либо совместимый унификатор. Из-за этой так называемой проверки вхождения (occur check) сложность всего алгоритма становится квадратично зависимой от размера унифицируемых выражений. В некоторых системах, включая все системы логического программирования, просто исключается такая проверка вхождения и поэтому в результате иногда формируются противоречивые логические выводы, а в других системах используются более развитые алгоритмы со сложностью, линейно зависящей от времени.