7. Задача унификации. Алгоритм унификации (1131918), страница 2
Текст из файла (страница 2)
Завершаемость (E 6; ∞)Основная идея — сформулировать строго следующий факт:на каждом шаге система становится немного проще, исамая простая система рано или поздно будет полученаПридумаем характеристику системы, которая убывает накаждом шаге и при этом не может убывать бесконечно долгоАлгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)Переменная x — приведённая в E, если E содержит уравнениевида x = t, где x ∈/ Vart , и не содержит x в других уравненияхХарактеристика системы E — упорядоченная тройка чиселH(E) = hvr (E), fs(E), eq(E)i, гдеIIIvr (E) — число неприведённых переменных системы Efs(E) — суммарное число функциональных символов иконстант в левых частях уравнений Eeq(E) — число уравнений системы EВведём лексикографический порядок на тройках целых чисел:n1 > m1hn1 , n2 , n3 i hm1 , m2 , m3 i ⇔ n1 = m1 , n2 > m2n1 = m1 , n2 = m2 , n3 > m3Пример: h2, 11, 2i h2, 10, 5578i h2, 10, 5577i h1, 1001, 78iАлгоритм унификацииДоказательство теоремы.
Завершаемость (E 6; ∞)1. Характеристика убывает при применении правил упрощения:(Triv, Swap, Func, Red)E 7→ E 0⇒H(E) H(E 0 )Правило Triv: ...t=tE=...vr (E) ≥ vr (E 0 )7→E0 =fs(E) ≥ fs(E 0 ) ......eq(E) > eq(E 0 )Алгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)1. Характеристика убывает при применении правил упрощения:(Triv, Swap, Func, Red)E 7→ E 0⇒H(E) H(E 0 )Правило Swap: ...t=xE=...vr (E) ≥ vr (E 0 )7→ ...0x=tE =...fs(E) > fs(E 0 )Алгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)1.
Характеристика убывает при применении правил упрощения:(Triv, Swap, Func, Red)E 7→ E 0⇒H(E) H(E 0 )Правило Func: ...f(t1 , . . . , tk ) = f(s1 , . . . , sk )E=...vr (E) ≥ vr (E 0 )7→... t1 = s1...E0 =tk = sk...fs(E) > fs(E 0 )Алгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)1. Характеристика убывает при применении правил упрощения:(Triv, Swap, Func, Red)E 7→ E 0⇒H(E) H(E 0 )Правило Red: ...x=tE=...7→ .
. . {x/t}0x=tE =. . . {x/t}vr (E) > vr (E 0 )Алгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)2. Характеристика не может убывать бесконечно долгоЛеммаНесуществуетбесконечнойпоследовательноститроек неотрицательных целых чисел, убывающейотносительно лексикографического порядкаДоказательство леммы. Попробуйте самиИными словами, (N30 , ) — фундированное множествоИли, по-другому, множество (N30 , ) обладаетсвойством обрыва убывающих цепейАлгоритм унификацииДоказательство теоремы. Завершаемость (E 6; ∞)2. Характеристика не может убывать бесконечно долгоИллюстрацияПредставьте, что у Вас есть 10 килограммов конфет: вкусных,обычных и невкусныхНачнём меняться конфетами:IIIВы даёте мне вкусную конфету, а я взамен — сколькопопросите обычных и невкусныхВы даёте мне обычную конфету, а я взамен — сколькопопросите невкусныхВы даёте мне невкусную конфету и не получаете ничеговзаменЕсли продолжать меняться конфетами, пока это возможно, торано или поздно Вы останетесь ни с чемАлгоритм унификацииДоказательство теоремы.
Успешность (E ; θ/СТОП)Что означает неуспешность алгоритма?Она означает, что алгоритмом получена неприведённаясистема E 0 , к которой невозможно применить ни одно изправил Triv, Swap, Func, Red, NFunc, NRedПравила Triv, Swap, Func, NFunc невозможно применить к E 0 :В левых частях уравнений системысодержатся только переменныеПравила Red, NRed невозможно применить к E 0 :Переменная, стоящая в левой части уравнения Eq,встречается только в левой части EqИтог: если к системе уравнений невозможно применить ни одноиз правил Triv, Swap, Func, Red, NFunc, NRed, то она обязанабыть приведённойАлгоритм унификацииДоказательство теоремы. Корректность (E ; θ ⇒ θ ∈ НОУ(E))Достаточно показать, что при применении правил Triv, Swap,Func, Red получается система, равносильная исходнойДля правил Triv, Swap, Func это показать довольно простоОстановимся на правиле Red: ...x = t 7→E=... .
. . {x/t}x=tE0 =. . . {x/t}Покажем, что системы E и E 0 равносильныАлгоритм унификацииДоказательство теоремы. Корректность (E ; θ ⇒ θ ∈ НОУ(E)) . . . {x/t} ...x=tx = t 7→ E 0 =E=. . . {x/t}...Покажем, что системы E и E 0 равносильны(⇒): Пусть η — унификатор системы EТогда xη ≡ tηИз доказательства леммы о связке: η = {x/t} η, а значит, .
. . {x/t} η ...ηxη ≡ tη ⇔xη ≡ tη. . . {x/t} η...ηЗначит, η — унификатор системы E 0(⇐): Рассуждения аналогичныАлгоритм унификацииДоказательство теоремы. Полнота (E ; СТОП ⇒ НОУ(E) = ∅)Пусть сообщение СТОП выдано для системы E 0Пусть для этого было применено правило NFuncТогда E 0 содержит уравнение f(. . . ) = g(. . . ), где f 6= gНи для какой подстановки θ не будет верно f(. . .
)θ ≡ g(. . . )θПусть для этого было применено правило NRedТогда E 0 содержит уравнение x = t, где x ∈ Vart и x 6≡ tЛемма о связке: ни для какой подстановки θ не верно xθ ≡ tθИтог: система E 0 неунифицируемаСистема E 0 была получена из E применением правил Triv, Swap,Func, RedКорректность алгоритма: системы E и E 0 равносильныЗначит, система E неунифицируемаHКонец лекции 7.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
