Унификация. 
Символический искусственный интеллект: математические основы представления знаний

Для того чтобы применять метод резолюций, нам нужно уметь находить контрарные литералы. В случае исчисления высказываний такой проблемы нет. Любая переменная и та же переменная с отрицанием — это и есть пара контрарных литералов. В случае исчисления предикатов первого порядка это уже не так просто. Даже когда мы нашли два вхождения одного предиката, положительное и с отрицанием, это еще не значит, что найдена контрарная пара. Разные вхождения предиката могут иметь различающиеся аргументы, в том числе и выражаемые разными термами, в то время как для правила резолюции необходимо их синтаксическое равенство (посимвольное совпадение (см. п. 4.1.2)). В некоторых случаях можно сделать такие замены переменных, что наборы аргументов сделаются одинаковыми (унифицировать), но в других случаях этого сделать нельзя. Существуют алгоритмы (в частности, приведенный ниже алгоритм 4.1), которые проверяют, можно ли унифицировать два литерала, и находят набор унифицирующих подстановок, если унификация возможна.

Уточним определения.

Подстановка — это конечный набор пар вида [t/v_x, …, t_n/v_n], где в каждой паре tj/Vj Vj — переменная, t_i — терм, отличный от v_v и все различны. Подстановка, которая не содержит элементов, называется пустой и обозначается 8.

Пусть 0 = _x/v_Xy…, t_n/v_n — подстановка и? — формула или терм (выражение), тогда ?0 означает выражение, полученное из? заменой одновременно всех вхождений переменной термом t_{ для каждого i, 1 В этом случае ?0 называется примером (или частным случаем) исходного выражения ?.

Пусть 0 = [t_x/x_Xy…, t_n/x_n иХ = и_х/у_{,…, и_т/у_т — две подстановки, тогда композиция подстановок 0 и X (обозначается 0о? о) есть подстановка, получаемая из набора [t_xX/x_v …, t_nX/x_n, и_{/у_{у…, и_т/у_т] вычеркиванием всех элементов t_tX/x_iy для которых t_iX = x_i (синтаксически равно), и всех элементов Uj/y_jy таких что у^ текстуально совпадает с одним из х_х,…, х_п.

Приведем пример, иллюстрирующий последнее определение.

Рассмотрим 0 = _x/x_x, t₂/x₂ = f (y)/x, z/y] iX = ujy_x, u₂/y₂, u₃/y₃] = = [a/x_y b/y, y/z]. Тогда QoX= _{X/x_{y t₂X/x₂, щ/у_ь и₂/у_ъ u₃/y₃] = [f (b)/x_y y/y, a/x_y b/y_y y/z], однако, поскольку t₂X = x₂ (у = y)_y то пара t₂X/x₂ должна быть вычеркнута. Кроме того, у_{ (имеющий значение х) совпадает с х_х (имеющим то же значение), а у₂ (имеющий значение у) совпадает с х₂(у), следовательно, должны быть вычеркнуты и и_х/у_{у и₂/у₂. Таким образом, окончательно в качестве результата композиции мы получим 0оА, = |f (b)/x_y y/z.

Следует отметить также, что композиция подстановок ассоциативна, а пустая подстановка s является левой и правой единицей, т. е. (0о?о)о^ = = 0o (^oQ и 0ое = 800 = 0.

Напомним, что применение правила резолюции в исчислении предикатов первого порядка сопряжено с умением находить контрарные пары предикатных символов, аргументами которых являются термы (литералы). Сформулируем процедуру (алгоритм), которая отвечает на вопрос «Могут ли два литерала считаться контрарной парой?» и в случае положительного ответа предъявляет подстановку, обеспечивающую свойство контрарности. Подчеркнем также, что используемое в этом параграфе равенство (знак «=») является равенством синтаксическим (посимвольным совпадением).

Введем еще несколько необходимых понятий.

Подстановка 0 называется унификатором для набора выражений {Е_и Е₂, …, Е_п) тогда и только тогда, когда Е_х0 = E₂Q = Е_п0, при этом говорят, что набор {fj, Е₂,…, Е_п) является унифицируемым.

Поскольку нас интересует вопрос унифицируемости пары литералов, то наш «набор выражений» естественно переходит в «два литерала».

Унификатор, а двух литералов Р_{ и Р₂ называется наиболее общим унификатором (Н.О.У.) тогда и только тогда, когда для каждого унификатора 0 этой пары существует такая подстановка X, что 0 = аоХ.

Сделаем два важных замечания к определениям.

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

Например, две формулы Р (х, f (a)) и P (g (b)_} у) унифицируемы, и их II.О.У. является подстановка а= [g (b)/x, f (a)/y]^[. В то же время литералы P (x, f (a)) и Р (у_} g (b)) не унифицируемы, потому что f (a) *g (b) при любых подстановках формул вместо переменных. Также не унифицируемы формулы P (x, f (a)) и P (g (b), х), поскольку для унификации требуется подставить вместо переменной х формулу f (a) и формулу g (b) одновременно, что, очевидно, невозможно.

Мы приводим классический алгоритм унификации (алгоритм 4.1), предложенный Робинсоном, в несколько упрощенной формулировке. Сразу заметим, что этот алгоритм — далеко не самый эффективный из известных в настоящее время. На вход алгоритма подаются два выражения (литерала) А и В, на выходе получается значение false, если выражения не унифицируемы, или значение true и Н.О.У а.

Алгоритм 4.1. Унификация двух формул

proc Unify (in А, В; out а): bool, а := 0^[1]

while АФВ do.

[A', B'] := FisrtNeqTerms (A, B).

ifi IsSubst (A', B', t, v) then return (false) end if ct := ao[t/v].

A := Subst (A, t, v).

В := Subst (B, t, v) end while return (true) end proc.

В этом алгоритме используются следующие функции и операции:

• • функция FisrtNeqTerms сравнивает свои аргументы слева направо и находит первые подформулы, в которых сравниваемые формулы отличаются. Например, сравнивая формулы Р (х, /(a)) и P (g (b), у)), функция FisrtNeqTerms вернет пару [.г, g (6)] — пару рассогласования-,
• • функция IsSubst (А', В', t, v) проверяет, образует ли первая пара аргументов А' и В' допустимую подстановку, т. е. является ли один из этих аргументов некоторой переменной v, а второй — формулой t, не содержащей вхождений этой переменной v. Например, если первый и второй аргументы функции равны х и g (b) соответственно, то функция вернет значение true, причем третий аргумент t получит значение g (b), а четвертый аргумент v получит значение х;
• • функция Subst (A, t, v) подставляет в формулу, А формулу t вместо всех вхождений переменной v. Например, если аргументы функции равны Р (х, /(a)), g (b), х соответственно, то результатом функции является формула P (g (b), f (a)).

Рассмотрим пример — протокол работы алгоритма 4.1 для пары формул Р (а, х, f (g (y))) и P (z, f (z), f (u)). В этом примере в каждой строке выписаны текущие значения переменных, А и В, причем найденные функцией FirstNeqTerms несовпадающие подформулы подчеркнуты. Справа выписан построенный унификатор:

Р (а, х, f (g (y))) P (z, /(z), /(a)) ст = [a/z].

P (a, x, f (g (y))) P (a, /(a), /(a)) ct = [a/z, f (a)/x]

P (a, /(a), f (g (y))) P (a, /(a), /(a)) ct = [a/z, f{a)/x, g (y)/u].

P (a, /(a), f (g (y))) P (a, /(a), f (g (y)))

Мы видим, что всего за четыре шага алгоритм заканчивает работу и находит наиболее общий унификатор. Однако не следует обольщаться и считать, что задача унификации — это простая задача. В действительности все «элементарные» операции, использованные в этом алгоритме, — нахождение несовпадающих подформул, проверка допустимости подстановки, выполнение подстановки и даже вычисление композиции подстановок — в реализации отнюдь не элементарны, и их фактическая трудоемкость кардинально зависит от выбранного способа представления формул. Между тем, представление формул для алгоритма 4.1 не определено.

Рассмотрим еще один алгоритм унификации, в котором структура формул фиксирована более явно. Применительно к рассматриваемому методу резолюций нам нужно проверять унифицируемость атомарных формул, синтаксис которых описан в п. 4.1.3. Чтобы не затуманивать идею ал горитма, мы оставим в языке только функциональные символы и переменные^[2].

В алгоритме 4.2 предполагается, что функция ор осуществляет синтаксический разбор формулы и возвращает знак главной операции (имя предиката, функциональный символ или имя переменной), функция var проверяет, является ли ее аргумент именем переменной, а функция args возвращает список аргументов главной операции. Набор подстановок (унификатор) представлен в виде глобального массива S, значениями индекса которого являются имена переменных, а значениями элементов — формулы, которые подставляются вместо соответствующих переменных.

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

Алгоритм 4.2. Рекурсивная унификация двух формул

proc Unify (in А, В): bool, а := f (А); b := f (В).

// обе формулы суть переменные if var (а) & var (b) then.

if a = b then return true end if.

if S[a]=0 & S[b]*0 then S[a] := S[b] return true end if if S[b]=0 & S[a]*0 then S[b] := S[a] return true end if if S[a]* 0 & S[b]*0 then Unify (S[a], S [b ]) end if S[a] := b II или S (b] := a.

end if.

// одна формула — переменная, а другая — нет if var (a)v var (b) then if var (a) & aeB then return false else.

if S[a] = 0 then S[a] := B; return true else return (S[a] = B) end if end if.

if var (b) & beA then return false else.

if S [b] = 0 then S[b] := A; return true else.

return (S[b] = A) end if end if.

end if.

/ / обе формулы не переменные.

if a*b then return false end if // главные операции различны for aeargs (A) || beargs (B) do if —I Unify (a, b) then return false end if end for return true end proc.

В данном алгоритме заголовок цикла for aeargs (А) | | beargs (В).

do означает параллельный цикл по спискам аргументов.

• [1] Напоминаем, что первыми буквами латинского алфавита а, Ь, с … мы обозначаем константы, последними буквами х, у, z … обозначаем переменные, для имен функций берембуквы f, g, h…
• [2] Предикатные символы с точки зрения унификации ничем нс отличаются от функциональных символов, а константы, хотя и требуют в коде алгоритма большого числа отдельныхпроверок, по существу подчиняются одному простому правилу: константа унифицируетсятолько с переменной.