Унификация

Чтобы применять правила вывода типа модус поненс, система вывода должна уметь определять, когда два выражения являются эквивалентными, или равносиль­ными. В исчислении высказываний это тривиально: два выражения равносильны то­гда и только тогда, когда они синтаксически идентичны. В исчислении предикатов определение равносильности двух предложений усложняется наличием переменных. Правило универсального инстанцирования позволяет заменять переменные под зна­ком квантора всеобщности термами из области определения. Необходимо определить процесс замены переменных, при котором несколько выражений могут стать идентичными (обычно для того, чтобы можно было применять правила вывода).

Унификация — это алгоритм определения необходимых подстановок с целью приве­дения в соответствие двух выражений исчисления предикатов. Пример такого процесса приведен в предыдущем подразделе, где терм socrates из выражения man(socrates) был использован в качестве подстановки для X в выражении VX(man(X)=3-morfa/(X)). Эта подстановка позволила применить правило модус поненс и получить вывод mortal{socrates). Еще один пример унификации был рассмотрен выше, когда обсужда­лись фиктивные переменные (dummy). Поскольку р(Х) ир(У) эквивалентны, для приве­дения предложений в соответствие (match) друг другу У можно заменить на X.

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

Весьма важный аспект этой формы заключается в требовании, чтобы все переменные стояли под знаком квантора всеобщности. Это обеспечивает полную свободу в выполне­нии подстановок. Переменные, стоящие под квантором существования, можно устранить из предложений в базе данных, заменив их константами, обеспечивающими истинность предложения. Например, ЭХ parent(X,tom) может быть заменено выражением parent(bob,tom) илиparent(mary,tom), принимая во внимание, что Боб (bob) и Мэри (тагу) являются родителями Тома (torn) в этой интерпретации.

Процесс удаления переменных, связанных квантором существования, усложнен тем фактом, что значение этих подстановок может зависеть от значения других переменных в выражении. Например, в высказывании VX ЗУ mother(X,Y) значение переменной У под квантором существования зависит от значения X. Сколемизация (skolemization) — это замена каждой переменной, связанной квантором существования, функцией несколь­ких или всех имеющихся в предложении переменных, которая возвращает соответст­вующую константу. В вышеупомянутом примере, поскольку значение У зависит от X, У можно заменить сколемовской функцией (skolem function) f от X. Это порождает предикат VX mother(X,f(X)). Сколемизация— это процесс, который также позволяет связывать переменные, стоящие под квантором всеобщности, с константами. Этот аспект подробно обсуждается в главе 12.

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

Процесс унификации осложняется тем фактом, что переменная может быть заменена любым термом, включая другие переменные и функциональные выражения произволь­ной сложности. Эти выражения могут тоже содержать переменные. Например, father(jack) можно использовать в качестве подстановки для X в выражении тал(Х) для получения вывода, что отец Джека смертен.

Приведем несколько реализаций выражения

foo(X,a,goo(Y)). Их можно получить путем следующих подстановок.

1. foo(fred,a,goo(Z))

2. foo(W,a, goo(jack))

3. foo(Z,a,goo(moo(Z)))

В этом примере экземпляры подстановки, или унификации, которые делают началь­ное выражение идентичным каждому из трех, можно записать в виде

{fred/X,Z/Y} {W/XJack/Y} {Z/X,moo(Z)/Y}

Запись X/Y, ... означает, что X является подстановкой для переменной Y в первона­чальном выражении. Подстановка также называется связыванием. Говорят, что перемен­ная связана со значением, используемым в качестве подстановки.

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

Хотя константу можно систематически использовать в качестве подстановки для пе­ременной, любая константа рассматривается как "базовый экземпляр" и не может быть заменена. Нельзя также два различных "базовых экземпляра" использовать в качестве подстановки для одной и той же переменной.

Переменная не может быть унифицирована с термом, содержащим ее. Поэтому пере­менная X не может быть заменена на р(Х), поскольку это порождает бесконечное выра­жение: р{р(р(р{...Х)...). Тест для этой ситуации называется проверкой вхождения (occurs check).

Вообще, процесс решения задачи требует ряда выводов и, следовательно, ряда последова­тельных унификаций. Логические решающие устройства задач должны поддерживать согла­сованность подстановок для переменных. Важно, чтобы любая унифицирующая подстановка была сделана согласованно по всем вхождениям этой переменной во все выражения. А выра­жения должны быть приведены в соответствие друг другу- Эта ситуация уже встречалась, ко­гда терм сократ использовался не только в качестве подстановки для переменной X в предложении человек(Х), но и для переменной X в выражении смертен(Х).

Если переменная связана, все последующие унификации и процедуры вывода должны учитывать это. Если переменная связана с константой, ее уже нельзя связы­вать с другим термом при последующих унификациях. Если переменная Х\ использо­валась в качестве подстановки для другой переменной Хг, а затем была заменена константой, то вХгТоже необходимо отразить это связывание. Множество замен, ис­пользуемых в последовательности выводов, играет важную роль, потому что оно может содержать ответ на первоначальный вопрос (подраздел 12.2.5). Например, ес­ли р(а,Х) унифицировать с предпосылкой правила p{Y,Z)=>q(Y,Z) при помощи под­становки {a/Y,X/Z}, модус поненс позволяет вывести q(a,X) при той же подстанов­ке. Если мы сопоставим этот результат с предпосылкой правила q(W,b)=>r(W,b), то выведем r(a,b) с учетом множества подстановок {a/W,b/X}.

Другое важное понятие — это композиция подстановок унификации. Если S и S' яв­ляются двумя множествами подстановок, то композиция S и S' (пишется SS') получается после применения S' к элементам S и добавления результата к S. Рассмотрим пример композиции последовательности подстановок

{X/Y,W/Z}, {V/X), {а/У, f(b)/W}. Они эквивалентны единственной подстановке {a/Y, f(b)/Z}.

Последняя подстановка была выведена путем компоновки {X/Y, W/Z) с {V/X) для полу­чения {V/Y, W/Z} и компоновки результата с {a/I/, f(b)/W) для получения {a/Y, f(b)/Z}.

Композиция подстановок— это метод, с помощью которого объединяются подста­новки унификации. Его можно реализовать, используя рекурсивную функцию unify, ко­торая представлена ниже. Можно показать, что композиция является ассоциативной, но не коммутативной. В упражнениях эти вопросы рассмотрены более подробно.

Последнее требование алгоритма унификации— унификатор (unifier) должен быть максимально общим, т.е. для любых двух выражений должен быть найден наиболее об­щий унификатор. Это очень важно, поскольку при потере общности в процессе решения уменьшается вероятность достижения окончательного решения или такая возможность исчезает полностью.

Например, предложения р(Х) и р( У) можно унифицировать любым константным вы­ражением вида {fred/X, fred/Y). Однако fred не является наиболее общим унификато­ром. Используя в качестве унификатора любую переменную, можно получить более об­щее выражение: {Z/X, Z/Y]. Решения, полученные при использовании первой подста­новки, всегда будут ограничены содержащейся в них константой fred, лимитирующей логические выводы. Следовательно, fred можно использовать в качестве унификатора, но это снижает универсальность результата.

ОПРЕДЕЛЕНИЕ

НАИБОЛЕЕ ОБЩИЙ УНИФИКАТОР

Если s — произвольный унификатор выражения Б, а д — наиболее общий унифика­тор (most general unifier — mgu) этого набора выражений, то в случае применения s к Е будет существовать еще один унификатор s' такой, что Es=Egs\ где Es и Egs' — композиции унификаций, примененные к выражению Е.

Наиболее общий унификатор для набора выражений определяется с точностью до обозначения. В конечном счете, не имеет никакого значения, как называется перемен­ная — X или У, поскольку это не снижает общности для результирующей унификации.

Унификация важна для любой системы решения задач искусственного интеллекта, использующей в качестве средства представления исчисление предикатов. Унифика­ция определяет условия, при которых два (или больше) выражения исчисления преди­катов могут быть эквивалентными. Это позволяет использовать для логического пред­ставления такие правила вывода, как резолюция (resolution), хотя этот процесс часто требует поиска с возвратом (backtracking) для нахождения всех возможных интерпре­таций (см. главу 14).

Ниже будет представлен псевдокод для функции unify (унифицировать), которая вы­числяет подстановки унификации (если это возможно) для двух выражений исчисления предикатов. Функция unify получает в качестве параметров два выражения исчисления предикатов и возвращает либо наиболее общую подстановку унификации, либо констан­ту FAIL (отказ), если унификация невозможна. Эта функция определена рекурсивно: вна­чале она пытается рекурсивно унифицировать исходные компоненты выражений. Если это удается, все подстановки, возвращаемые в результате этой унификации, применяют­ся к остальным выражениям. Затем выполняется второй рекурсивный вызов функции unify, в котором завершается унификация. Рекурсия прекращается, когда параметром становится символ (предикат, имя функции, константа или переменная), или когда все элементы выражения приводятся в соответствие.

Чтобы упростить работу с выражениями, в алгоритме применяется слегка изме­ненный синтаксис. Поскольку функция unify просто проверяет синтаксическое соот-

[А.Д.1]

[А.Д.2]

[А.Д.3]

[А.Д.4]

[А.Д.5]

[А.Д.6]

[А.Д.7]

[А.Д.8]

[А.Д.9]

[А.Д.10]

[А.Д.11]

[А.Д.12]

[А.Д.13]

[А.Д.14]