Унификация
Применение поднятых правил логического вывода связано с необходимостью поиска подстановок, в результате которых различные логические выражения становятся идентичными. Этот процесс называется унификацией и является ключевым компонентом любых алгоритмов вывода в логике первого порядка. Алгоритм Unify принимает на входе два высказывания и возвращает для них унификатор, если таковой существует:
Unify(p,q) = 9 где Subst(9,p) = Subst(9,g)
Рассмотрим несколько примеров того, как должен действовать алгоритм Unify. Предположим, что имеется запрос Knows (John, х) — кого знает Джон? Некоторые ответы на этот запрос можно найти, отыскивая все высказывания в базе знаний, которые унифицируются с высказыванием Knows {John, х). Ниже приведены результаты унификации с четырьмя различными высказываниями, которые могут находиться в базе знаний.
Unify (Knows (John, х) , Knows (John, Jane) ) - {x/Jane}
Unify(Knows(John,x), Knows(y,Bill)) = {xfBill,у/John)
Unify (Knows (John, x) , Knows (y, Mother (y) ) ) = {у/John, x/Mother (John) }
Unify(Knows(John,x), Knows(x, Elizabeth)) = fail
Последняя попытка унификации оканчивается неудачей (fail), поскольку переменная х не может одновременно принимать значения John и Elizabeth. Теперь вспомним, что высказывание Knows (х, Elizabeth) означает "Все знают Элизабет", поэтому мы обязаны иметь возможность вывести логически, что Джон знает Элизабет. Проблема возникает только потому, что в этих двух высказываниях, как оказалось, используется одно и то же имя переменной, х. Возникновения этой проблемы можно избежать, стандартизируя отличие (standardizing apart) одного из этих двух унифицируемых высказываний; под этой операцией подразумевается переименование переменных в высказываниях для предотвращения коллизий имен. Например, переменную х в высказывании Knows (х, Elizabeth) можно переименовать в z17 (новое имя переменной), не меняя смысл этого высказывания. После этого унификация выполняется успешно:
Unify (Knows (John, х) , Knows (zn, Elizabeth) ) = {х/ Elizabeth, zn I John}
Возникает еще одна сложность: выше было сказано, что алгоритм Unify должен возвращать такую подстановку (или унификатор), в результате которой два параметра становятся одинаковыми. Но количество таких унификаторов может быть больше единицы. Например, вызов алгоритма Unify [Knows (John, х) , Knows {у, z) ) может возвратить {у/ John,x/z} или {у/John, х/John, z/John). Первый унификатор позволяет получить в качестве результата унификации выражение Knows {John, z), а второй дает Knows {John, John). Но второй результат может быть получен из первого с помощью дополнительной подстановки {z/John}\ в таком случае принято считать, что первый унификатор является более общим по сравнению со вторым, поскольку налагает меньше ограничений на значения переменных. Как оказалось, для любой унифицируемой пары выражений существует единственный наиболее общий унификатор (Most General Unifier— MGU), который является уникальным вплоть до переименования переменных. В данном случае таковым является {у/ John,x/z}.
Алгоритм вычисления наиболее общих унификаторов приведен в листинге 9.1. Процесс его работы очень прост: рекурсивно исследовать два выражения одновременно, "бок о бок", наряду с этим формируя унификатор, но создавать ситуацию неудачного завершения, если две соответствующие точки в полученных таким образом структурах не совпадают. При этом существует один дорогостоящий этап: если переменная согласуется со сложным термом, необходимо провести проверку того, встречается ли сама эта переменная внутри терма; в случае положительного ответа на данный вопрос согласование оканчивается неудачей, поскольку невозможно сформировать какой-либо совместимый унификатор. Из-за этой так называемой проверки вхождения (occur check) сложность всего алгоритма становится квадратично зависимой от размера унифицируемых выражений. В некоторых системах, включая все системы логического программирования, просто исключается такая проверка вхождения и поэтому в результате иногда формируются противоречивые логические выводы, а в других системах используются более развитые алгоритмы со сложностью, линейно зависящей от времени.
Листинг 9.1. Алгоритм унификации. Алгоритм действует путем поэлементного сравнения структур входных высказываний. В ходе этого формируется подстановка 8, которая также является параметром функции Unify и используется для проверки того, что дальнейшие сравнения совместимы со связываниями, которые были определены ранее. В составном выражении, таком как F{ А, в), функция Op выбирает функциональный символ F, а функция Args выбирает список параметров (А, В)
function Unify(х, у, 9) returns подстановка, позволяющая сделать х и у идентичными inputs: х, переменная, константа, список или составной терм у, переменная, константа, список или составной терм 9, подстановка, подготовленная до сих пор (необязательный параметр, по умолчанию применяется пустой терм)
if 9 = failure then return failure else if x = у then return 9
else if Variable?(x) then return Unify-Var(x, y, 9) else if Variable?(y) then return Unify-Var(y, x, 9) else if Compound?(x) and Compound?(y) then
return Unify(Args[x], Args[y] , Unify(Op[x], Op[y] , 8)) else if List?(x) and List?(y) then
return Unify(Rest[xj , Rest[y], Unify(First[x] , First[y], 0) ) else return failure
function Unify-Var(var, x, 0) returns подстановка inputs: var, переменная
x, любое выражение
0, подстановка, подготовленная до сих пор
if {var/val} е 0 then return Unify(val, x, 0) else if {x/val} e 0 then return Unify(var, val, 0) else if Occur-Check?{var, x) then return failure else return добавление {var/х) к подстановке 0