Унификация: неформальное описание

Алгоритм унификации применяется к предложениям, записанным в сколемовской нормальной форме и представленным в теоретико-множественной форме как множество дизъюнктов S. Если в этом множестве имеются одноименные атомы, то к ним можно попытаться (это возможно не всегда) применить процедуру унификации. Пусть множество S содержит дизъюнкты

В дизъюнкты С1 и С2 входит двуместный атом Р, однако его аргументы в C1 и С2 различны. Процедура унификации проверяет, существует ли такая подстановка q, выполнив которую, можно привести оба рассматриваемых атома к одному и тому же виду. Обнаружив одноименные атомы, алгоритм унификации выполняет поочередно проверку совпадения их аргументов. Аргументами атомов являются термы. При выполнении подстановки композиций необходимо иметь в виду:

вместо констант нельзя подставлять ничего;

если оба аргумента являются переменными, имеющими разные имена, подстановкой является переименование переменных;

если один из унифицируемых термов является переменной, а другой-константой, выполняется подстановка константы вместо переменной;

если один из термов образован функциональным символом (по второму пункту определения терма), а в другом атоме этот же терм является переменной, то выполняется подстановка этого функционального символа вместо переменной;

если унифицируемые термы образованы разными функциональными символами, унификация невозможна;

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

Используем этот алгоритм для унификации дизъюнктов С1 и С2.

Шаг 1. В оба рассматриваемых дизъюнкта входит двуместный атом Р. Алгоритм унификации сравнивает соответствующие термы атомов в обоих дизъюнктах слева направо. Обнаружив несоответствие термов в рассматриваемой паре аргументов, алгоритм образует множество рассогласования DS. Для С1 и С2 первым множеством рассогласования будет DS1={x, g(c)}.

Шаг 2. Производится проверка вхождений (ПВ), которая выясняет для каждой переменной, входящей в первый терм множества рассогласования DS, есть ли вхождение этой переменной в другой терм. Если ДА, то ПВ дает ответ ДА. Это означает, что унификация невозможна. ПВ дает такой же ответ, если в DS нет переменных. Если ПВ дает ответ НЕТ, то выполняется подстановка. В противном случае дизъюнкты не унифицируемы, и применение алгоритма заканчивается неудачей. Если ПВ дает отрицательный, ответ, то формируется подстановка, заменяющая переменную из множества рассогласования на терм из того же множества. Для С1 и С2 применяем подстановку q1={x/g(c)}. В результате дизъюнкты С1 и С2 принимают вид

Шаг 3. Продолжаем двигаться вправо, выполняя шаги 1, 2. Новым множеством рассогласования будет DS2={y, g(d)}. Проверка вхождений дает отрицательный ответ. Применяем подстановку q2={y/g(d)} и получаем

В результате выполненных подстановок атомы P в обоих дизъюнктах стали полностью идентичными.

Алгоритм заканчивает работу, выдавая в качестве ответа множество подстановок, позволяющих унифицировать C1 и C2. Это множество подстановок называется общим унификатором (ОУ) дизъюнктов. Для С1 и С2 общим унификатором является множество q=q1Èq2={x/g(c), y/g(d)}. Если дизъюнкты не могут быть унифицируемы, алгоритм останавливается на шаге 2.

Унификатор q называется наиболее общим унификатором (НОУ), если для любого другого унификатора y существует подстановка g такая, что y=qg.

Для множества дизъюнктов S НОУ определяется единственным образом.

Теорема Дж. А. Робинсона. Результатом применения алгоритма унификации к множеству атомов {P₁,…, P_n} является одно из двух сообщений:

· если множество атомов унифицируемо, то алгоритм останавливается, выдавая в качестве ответа НОУ;

· если множество атомов не унифицируемо, то алгоритм останавливается, объявляя, что унификатора не существует.

Теорема утверждает, что если множество дизъюнктов S унифицируемо, то алгоритм унификации останавливается, определяя именно НОУ множества атомов.

Примеры

1. Рассмотрим множество атомов S={Q(g(x),w), Q(y, b)}, где b – константа. Используя описанную выше процедуру унификации, для множества атомов S определим НОУ: Однако для получения множества основных примеров требуется дополнить эту подстановку, заменив переменную x константой b, присутствующей в эрбрановском множестве для этого множества дизъюнктов, т.е. применить подстановку g={x/b}. Композиция подстановок qg={y/g(b), x/b, w/b}=y является унификатором для S. Дальнейшее исследование формулы заключается в построении эрбрановского множества и множества основных примеров. Эрбрановское множество в данном случае будет иметь вид H={b, g(b), g(g(b)),…}. Соответствующее множество основных примеров: {Q(b,b), Q(g(b),b), Q(b,g(b)), Q(g(b),g(b)),…}.

2. Пусть получено множество дизъюнктов S={{Q(а,x,f(g(z)))}, {Q(z,f(y), f(y))}}. Определить, унифицируемо ли S. Если да, найти НОУ.

Процедура унификации окончена. Следовательно, S унифицируемо и его НОУ, получаемый объединением всех подстановок, имеет вид

НОУ= q0q1q2q3 = {z/a, x/f(g(a)), y/g(a)}.

2. Дано множество дизъюнктов: S={{Q(y,y)}, {Q(z, f(z))}}. Определить, унифицируемо ли S. Если да, найти НОУ.

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

Дата добавления: 2014-11-08; просмотров: 574; Нарушение авторских прав

Мы поможем в написании ваших работ!