8. Алгоритм унификации (1158022), страница 2
Текст из файла (страница 2)
алгоритм унификации Мартелли-Монтанари всегдазавершает работу;2. если система уравнений E унифицируема , то в результатеработы алгоритма унификации будет построенаприведенная система уравнений, равносильная исходнойсистеме E;3. если система уравнений E неунифицируема , то врезультате работы алгоритма унификации будет выданосообщение СТОП: НЕТ УНИФИКАТОРА.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.
Завершаемость алгоритма.Уравнение x = t, где x ∈ Var , x ∈/ Vart , будем называтьприведенным уравнением системы E , если переменная x несодержится ни в каких других уравнениях системы E.Переменную x в этом случае будем называть приведеннойпеременной системы EКаждой системе уравнений E сопоставим характеристикуH(E) = hh1 (E), h2 (E), h3 (E)i, — упорядоченную тройкунатуральных чисел, в которой1. h1 (E) — общее число неприведенных переменных,содержащихся в системе E;2. h2 (E) — общее число функц. символов и констант,содержащихся в левых частях уравнений системы E;3. h3 (E) — общее число уравнений в системе E.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.На множестве упорядоченных троек натуральных чисел введемотношение лексикографического порядка :hM1 , M2 , M3 i hN1 , N2 , N3 imN 1 < M1или N1 = M1 и N2 < M2или N1 = M1 , N2 = M2 и N3 < M3 .Пример.h2, 11, 2i h2, 10, 5578i h1, 1001, 78iАЛГОРИТМ УНИФИКАЦИИДоказательство.
1. Завершаемость алгоритма.Вспомогательная лемма.В множестве троек натуральных чисел не существуетбесконечно убывающей последовательностиhk1 , m1 , n1 i hk2 , m2 , n2 i · · · hki , mi , ni i hki+1 , mi+1 , ni+1 i . . .Доказательство вспомогательной леммы.Самостоятельно.АЛГОРИТМ УНИФИКАЦИИИдея доказательства вспомогательной леммы.Предположим, что у Вас есть 1 000 000 руб.
в произвольныхкупюрах. Сыграем в игру. Правила игры таковы.1. Вы даете мне денежную купюру и взамен получаете правопотребовать от меня любую сумму в купюрах меньшегодостоинства.2. Если Вы вручаете мне купюру наименьшего достоинства,то взамен не получаете ничего.Докажите, что игра всегда будет оканчиваться тем, что Выостаетесь без денег.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.
Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 ) H(E 00 ),где i = 1, 3, 4, 5.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 ) H(E 00 ),где i = 1, 3, 4, 5.Правило (1) ...f (t1 , . . . , tn ) = f (s1 , . .
. , sn )E0 :......t1 = s 1(1)...−→ E 00 :t = s1 1...h1 (E 0 ) h1 (E 00 ), h2 (E 0 ) h2 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т. е.(i)E 0 −→ E 00 ⇒ H(E 0 ) H(E 00 ),Правило (3) ...0s=xE :...где i = 1, 3, 4, 5. ...(3)00x =s−→ E :...h1 (E 0 ) h1 (E 00 ), h2 (E 0 ) h2 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т.
е.(i)E 0 −→ E 00 ⇒ H(E 0 ) H(E 00 ),Правило (4) ...0s=sE :...где i = 1, 3, 4, 5. ...(4)00...−→ E :...h1 (E 0 ) h1 (E 00 ), h2 (E 0 ) h2 (E 00 ), h3 (E 0 ) h3 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)характеристика системы уравнений убывает, т.
е.(i)E 0 −→ E 00 ⇒ H(E 0 ) H(E 00 ),Правило (5)t1 = s 1 ...x = sjE0 :...tn = s nгде i = 1, 3, 4, 5.t1 {x/sj } = s1 {x/sj }...(5)x = sj−→ E 00 :...tn {x/sj } = sn {x/sj }h1 (E 0 ) h1 (E 00 )АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.Значит, правила (1), (3, (4), (5) не могут применятьсябесконечно долго.Значит, рано или поздно либо будет применено одно из правил(2), (6), либо будет получена система, к которой неприменимони одно правило. В любом случае работа алгоритмаунификации завершится.АЛГОРИТМ УНИФИКАЦИИДоказательство. 2. Корректность алгоритма.Покажем, что в результате применения правил (1), (3, (4), (5)получается система уравнений, равносильная исходной, т.
е.(i)E 0 −→ E 00 ⇒ E 0 ' E 00 ,где i = 1, 3, 4, 5.Это, очевидно, верно для правил (1), (3, (4) (убедитесь сами ).Покажем, что правило (5) также приводит к равносильнойсистеме.t1 = s 1t1 {x/sj } = s1 {x/sj } ... ...(5)x = sjx = sjE0 :−→ E 00 :......tn = s ntn {x/sj } = sn {x/sj }АЛГОРИТМ УНИФИКАЦИИДоказательство. 2. Корректность алгоритма.Предположим,что θ — унификатор системы уравнений E 0 , т. е.t1 θ ≡ s 1 θ ...xθ ≡ sj θ...tn θ ≡ s n θТ. к. xθ ≡ sj θ, x ∈/ Varsj , согласно лемме о связке θ = {x/sj }θ.Следовательно,t1 {x/sj }θ ≡ s1 {x/sj }θ ...xθ ≡ sj θ...tn {x/sj }θ ≡ sn {x/sj }θЗначит, θ — унификатор системы уравнений E 00 . Аналогичнодоказывается, что всякий унификатор системы E 00 являетсяунификатором системы E 0 .АЛГОРИТМ УНИФИКАЦИИДоказательство.
3. Полнота алгоритма унификации.Как мы показали, рано или поздно при работе алгоритма либобудет применено одно из правил (2), (6), либо будет полученасистема, к которой неприменимо ни одно правило.Если к системе применяется правило (2), то в системе естьуравнение f (s1 , . . . , sn ) = g (t1 , . . . , tm ), f 6= g . Очевидно, длялюбой подстановки θ верно f (s1 , . . . , sn )θ 6≡ g (t1 , . . . , tm )θ.Значит, система, содержащая такое уравнение,неунифицируема.Если к системе применяется правило (6), то в системе естьуравнение x = s, x ∈ Vars . Согласно лемме о связке для любойподстановки θ верно xθ 6≡ sθ. Значит, система, содержащаятакое уравнение, неунифицируема.Значит, выдача сообщения СТОП: НЕТ УНИФИКАТОРАозначает, что система неунифицируема.АЛГОРИТМ УНИФИКАЦИИДоказательство. 3.
Полнота алгоритма унификации.Если к системе уравнений неприменимо ни одно правило, тоIв левых частях уравнений содержатся только переменные(иначе применимы правила (1), (2) или (3));Iни одна переменная из левой части больше нигде несодержится (иначе применимы правила (4), (5) или (6)).Значит, построенная система уравнений является приведеннойи имеет унификатор, который вычисляется по лемме оприведенной системе .КОНЕЦ ЛЕКЦИИ 8..
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
