 |
Унификация: неформальное описание
|
|
|
|
Алгоритм унификации применяется к предложениям, записанным в сколемовской нормальной форме и представленным в теоретико-множественной форме как множество дизъюнктов S. Если в этом множестве имеются одноименные атомы, то к ним можно попытаться (это возможно не всегда) применить процедуру унификации. Пусть множество S содержит дизъюнкты
В дизъюнкты С1 и С2 входит двуместный атом Р, однако его аргументы в C1 и С2 различны. Процедура унификации проверяет, существует ли такая подстановка q, выполнив которую, можно привести оба рассматриваемых атома к одному и тому же виду. Обнаружив одноименные атомы, алгоритм унификации выполняет поочередно проверку совпадения их аргументов. Аргументами атомов являются термы. При выполнении подстановки композиций необходимо иметь в виду:
1. вместо констант нельзя подставлять ничего;
2. если оба аргумента являются переменными, имеющими разные имена, подстановкой является переименование переменных;
3. если один из унифицируемых термов является переменной, а другой-константой, выполняется подстановка константы вместо переменной;
4. если один из термов образован функциональным символом (по второму пункту определения терма), а в другом атоме этот же терм является переменной, то выполняется подстановка этого функционального символа вместо переменной;
5. если унифицируемые термы образованы разными функциональными символами, унификация невозможна;
6. если оба аргумента являются константами, и эти константы различны, то унификация невозможна.
Используем этот алгоритм для унификации дизъюнктов С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 НОУ определяется единственным образом.
Теорема Дж. А. Робинсона. Р езультатом применения алгоритма унификации к множеству атомов {P1,…, Pn} является одно из двух сообщений:
|
|
|
· если множество атомов унифицируемо, то алгоритм останавливается, выдавая в качестве ответа НОУ;
· если множество атомов не унифицируемо, то алгоритм останавливается, объявляя, что унификатора не существует.
Теорема утверждает, что если множество дизъюнктов 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. Если да, найти НОУ.
| Шаг 0. | Полагаем q0=Е (здесь Е – пустая подстановка, E={ }). Пустая подстановка вводится для удобства написания программы. |
| Шаг 1: | S q0 = S. DS(S q0)=DS1= { a,z }. ПВ дает ответ НЕТ. Полагаем q1={ z/a }. |
| Шаг 2. | Sq0q1={ Q(a,x,f(g(a))), Q(a,f(y), f(y)) }. DS(Sq0q1)=DS2={ x, f(y) }. ПВ дает ответ НЕТ. Полагаем q2={ x/f(y) }. |
| Шаг 3. | Sq0q1q2={ Q(a, f(y), f(g(a))), Q(a, f(y), f(y)) }. DS(Sq0q1q2)=DS2={ g(a), y }. ПВ дает ответ НЕТ. Полагаем q3={ y/g(a) }. |
| Шаг 4. | Sq0q1q2q3={ Q(a, f(g(a)), f(g(a))), Q(a, f((a)), f(g(a))) }. DS(Sq0q1q2q3)=Æ. |
Процедура унификации окончена. Следовательно, S унифицируемо и его НОУ, получаемый объединением всех подстановок, имеет вид
НОУ= q0q1q2q3 = { z/a, x/f(g(a)), y/g(a) }.
2. Дано множество дизъюнктов: S={{ Q(y,y)}, {Q(z, f(z)) }}. Определить, унифицируемо ли S. Если да, найти НОУ.
| Шаг 0. | Полагаем q0=Е. |
| Шаг 1. | S q0 = S. DS(S q0)=DS1= { y,z }. ПВ дает ответ НЕТ. Полагаем q1={ y/z }. |
| Шаг 2. | Sq0q1={Q(z,z), Q(z,f(z)) }. DS(Sq0q1)=DS2={ z, f(z) }. ПВ дает ответ ДА, так как z встречается во втором терме f(z). |
Результатом положительного ответа на проверку вхождений является сообщение, что множество дизъюнктов S не унифицируемо.
|
|
|
|
|
|
