7. Задача унификации. Алгоритм унификации (1131918)

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла

Математическая логикаЛектор:Подымов Владислав Васильевичe-mail:valdus@yandex.ru2017, весенний семестрЛекция 7Задача унификацииАлгоритм унификацииНапоминание|= ∃x (P(x) &(∀x P(x) → ∃y R(x, y)) → ∃y R(x, y)) ?⇔ отрицание ψ = ¬ϕ противоречиво¬∃x (P(x) &(∀x P(x) → ∃y R(x, y)) → ∃y R(x, y))⇔ предварённая нормальная форма ψpnf противоречива∀x ∃z ∃y ∀u (P(x) &(¬P(z) ∨ R(x, y)) & ¬R(x, u))⇔ сколемовская стандартная форма ψssf противоречива∀x ∀u (P(x) &(¬P(f(x)) ∨ R(x, g(x))) & ¬R(x, u))⇔ система дизъюнктовSϕ противоречива P(x)¬P(f(x)) ∨ R(x, g(x))¬R(x, u)А как эффективно проверитьпротиворечивость системы дизъюнктов?Противоречия в системах дизъюнктовI{P(x), ¬P(x)}¬P(x)P(x)явное противоречиеI{¬P(x), ¬Q(y), P(x) ∨ Q(y)}¬P(x)P(x) ∨ Q(y)Q(y)явное противоречие∀x ¬P(x), ∀x ∀y (P(x) ∨ Q(y)) |= ∀y Q(y)¬Q(y)Противоречия в системах дизъюнктовI{P(f(x), y), ¬P(u, g(v))}¬P(u, g(v))P(f(x), y)неявное противоречиеP(f(x), g(v))¬P(f(x), g(v))∀x ∀y P(f(x), y) |= ∀x ∀v P(f(x), g(v))∀u ∀v ¬P(u, g(v)) |= ∀x ∀v ¬P(f(x), g(v))Чтобы обнаружить неявное противоречие, потребовалосьпривести дизъюнкты к общему частному случаюПриведение выражений к общему виду — это унификацияА насколько просто унифицироватьатомы в логике предикатов?Задача унификацииУнификация атомов A, B достигается применением к нимподстановки θ, такой что Aθ = BθНапоминаниеПодстановка — это отображение θ : Var → TermКонечная подстановка задаётся множеством связок:{x1 /t1 , .

. . , xn /tn }E θ — это результат применения подстановки θ к выражению EЧтобы поставить и решить задачу унификации, исследуемалгебраические свойства подстановокЗадача унификацииКомпозиция подстановок θ, η — это подстановка θη, такая чтодля любой переменной x верно:x(θη) = (xθ)ηУтверждениеПусть θ = {x1 /t1 , . . .

, xn /tn } и η = {y1 /s1 , . . . , yk /sk }. Тогдаθη = {xi /ti η | 1 ≤ i ≤ n, xi 6= ti η}∪ {yj /sj | 1 ≤ j ≤ k, yj ∈/ {x1 , . . . , xn }}Доказательство. Рассмотрим переменную z ∈ VarЕсли z ∈/ Domθ ∪ Domη , то z(θη) = (zθ)η = zη = zЕсли z = yj ∈ Domη \ Domθ , то z(θη) = (zθ)η = zη = sjИначе z = xi ∈ Domθ , и z(θη) = (zθ)η = ti ηHЗадача унификацииПримерθ = {x/f(x, c), y/g(u), z/y}η = {x/g(y), y/z, u/c}θη = ?{x/f(x, c)η, y/g(u)η, z/yη} ∪ {u/c}{x/f(g(y), c), y/g(c), z/z} ∪ {u/c}{x/f(g(y), c), y/g(c)} ∪ {u/c}θη = {x/f(g(y), c), y/g(c), u/c}Задача унификацииПодстановка θ — унификатор выражений E1 , E2 , если E1 θ = E2 θВыражения E1 , E2 унифицируемы, если существует унификаторэтих выраженийПодстановка θ —наиболее общий унификатор выражений E1 , E2 , если1.

θ — унификатор выражений E1 , E22. для любого унификатора η выражений E1 , E2 существуетподстановка µ, такая чтоη = θµНОУ(E1 , E2 ) — множество всех наиболее общих унификатороввыражений E1 , E2Задача унификацииПримерыПодстановка η = {y/g(g(v)), u/f(c), v/g(v), x/c} — унификаторатомов P(f(x), y), P(u, g(v)):P(f(x), y)η = P(f(c), g(g(v))) = P(u, g(v))ηА подстановка θ = {y/g(v), u/f(x)} — более общий ихунификатор: η = θ {v/g(v), x/c}Оказывается, что θ —наиболее общий унификатор атомов P(f(x), y), P(u, g(v))Но как это доказать, и как построить такой унификатор?А выражения P(x, f(x)), P(g(y), y) неунифицируемыА это как доказать?Задача унификацииформулируется следующим образом:для заданных выражений E1 , E2выяснить, унифицируемы ли эти выражения,и если это так, товычислить их наиболее общий унификаторАлгоритм унификацииУнификация, простой случай: НОУ(x, t) =? (x ∈ Var, t ∈ Term)Лемма о связкеПусть x ∈ Var и t ∈ Term.

Тогда:1. если x ∈/ Vart , то {x/t} ∈ НОУ(x, t)2. если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅Доказательство.1. x ∈/ VartДостаточно показать, что:а) {x/t} — унификатор (переменной x и терма t)б) для любого унификатора θ существует унификатор η, такойчто θ = {x/t} ηа) x {x/t} = t = t {x/t}Алгоритм унификацииУнификация, простой случай: НОУ(x, t) =? (x ∈ Var, t ∈ Term)Лемма о связкеПусть x ∈ Var и t ∈ Term. Тогда:1. если x ∈/ Vart , то {x/t} ∈ НОУ(x, t)2.

если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅Доказательство.1б) x ∈/ Vart ;xθ = tθ?⇒∃ηθ = {x/t} ηРассмотрим произвольную переменную yЕсли y = x, то yθ = xθ=tθ = x {x/t}θ = y {x/t} θЕсли y =6 x, то yθ = y {x/t}θИтог: для любой переменной y верно равенство y {x/t} θ = yθ,а значит, θ = {x/t} θАлгоритм унификацииУнификация, простой случай: НОУ(x, t) =? (x ∈ Var, t ∈ Term)Лемма о связкеПусть x ∈ Var и t ∈ Term.

Тогда:1. если x ∈/ Vart , то {x/t} ∈ НОУ(x, t)2. если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅Доказательство.2. x ∈ Vart , x 6= tРассмотрим произвольную подстановку θ, θ ∈ SubstПусть xθ = sТогда |xθ| = |s| < |t {x/s}| ≤ |tθ||xθ| < |tθ|, а значит, xθ 6= tθ(|p|— длина терма p)HАлгоритм унификацииУнификация атомовE1 = P(t1 , . . . , tk ), E2 = P(s1 , . .

. , sk )⇔Вычисление подстановки θ, такой что левая (ti ) и правая (si )части каждого уравнения в системе t 1 = s1...E(E1 , E2 ) =t k = skстановятся посимвольно одинаковыми при применении θ ковсем термам системы⇔Вычисление решения системы уравнений E(E1 , E2 ) всвободной1 алгебре термов21Значение терма — это сам терм, то есть термы равны, если онипосимвольно совпадают2Операция композиции — это подстановка терма на место переменнойАлгоритм унификацииДля устранения неоднозначности нотации будем до концалекции использовать такие обозначения:(t, s ∈ Term)I t=s — уравнение с левой частью t и правой частью sI t≡s — “термы t и s посимвольно совпадают”Подстановка θ — унификатор системы уравнений t1 = s1...,tk = skесли ti θ ≡ si θ для каждого i, 1 ≤ i ≤ kПодстановка θ — наиболее общий унификатор системыуравнений E, если1.

θ — унификатор системы E2. для любого унификатора η системы E существуетподстановка µ, такая что η = θµАлгоритм унификацииПримерE=f(c, x) = f(y, g(y))g(y) = zEθ =f(c, g(c)) = f(c, g(c))g(c) = g(c)θ = {x/g(c), y/c, z/g(c)} —(наиболее общий) унификатор системы EА системаf(c, y) = f(y, g(y))g(y) = zнеунифицируема (не имеет решений)(почему?)Алгоритм унификацииУтверждениеПусть заданы атомыE1 = P(t1 , . .

. , tk ), E2 = P(s1 , . . . , sk )и система уравнений t1 = s1...E = E(E1 , E2 ) =tk = skТогда НОУ(E1 , E2 ) = НОУ(E)Доказательство. Очевидно(следует из определений наиболее общего унификатора)А как найти наиболее общий унификатор системы уравнений?Алгоритм унификацииСистема уравнений является приведённой, если она имеет вид x1 = t1...,xk = tkгде x1 , . . . , xk — попарно различные переменные, невстречающиеся в правых частях уравнений:S{x1 , . .

. , xk } ∩Vartk = ∅1≤i≤kПример x = f(y, g(y))z=w— приведённая системаu = g(c)Алгоритм унификацииСистема уравнений является приведённой, если она имеет вид x1 = t1...,xk = tkгде x1 , . . . , xk — попарно различные переменные, невстречающиеся в правых частях уравнений:S{x1 , . . . , xk } ∩Vartk = ∅1≤i≤kПримерx = f(y, g(y))x=w— неприведённая система:y = g(c, c)g(z) = f(c, x)1. g(z) — не переменная, стоит в левой части уравнения2.

x встречается в левых частях два раза3. y встречается и в левой, и в правой частяхАлгоритм унификацииСистема уравнений является приведённой, если она имеет вид x1 = t1...,xk = tkгде x1 , . . . , xk — попарно различные переменные, невстречающиеся в правых частях уравнений:S{x1 , . . .

, xk } ∩Vartk = ∅1≤i≤kУнификация, более сложный случай: НОУ(E) =?(E — приведённая система уравнений)Лемма о приведённойсистеме x1 = t1...Если E =— приведённая система,xk = tkто {x1 /t1 , . . . , xk /tk } ∈ НОУ(E)Доказательство. Следует из леммы о связкеHАлгоритм унификацииУнификация, общий случай: НОУ(E) =?(E — произвольная система уравнений)Системы уравнений E1 , E2 равносильны, еслиНОУ(E1 ) = НОУ(E2 )Будем преобразовывать систему E методом исключенияпеременных так, чтобы в результате получилась равносильнаяприведённая системаАлгоритм унификацииАлгоритм унификации1Далее будут описаны 6 правил преобразования системыуравненийЭти правила произвольно (недетерминированно) применяются ксистеме, пока не станет верным одно из условий:Iполучена приведённая система уравненийIIявно установлена невозможность унификации системыI1ответ: унификатор из леммы о приведённой системеответ: СТОП: система неунифицируемаMartelli A., Montanari U.

An efficient unification algorithm. 1982Алгоритм унификацииПравила преобразования системы уравненийУпрощение системы:Triv:(x ∈ Var, t ∈ Term)удалить t = tSwap: заменить t = x на x = t, если t ∈/ Var  t1 = s1Func: заменить f(t1 , . . . , tk ) = f(s1 , . . . , sk ) на... t =skkRed:если в системе есть уравнение Eq : x = t, гдеI x ∈/ VartI x встречается в других уравнениях системыто применить подстановку {x/t} ко всем уравнениямсистемы, кроме EqАлгоритм унификацииПравила преобразования системы уравненийЯвная неунифицируемость:NRed:(x ∈ Var, t ∈ Term)если в системе есть уравнение x = t, где x ∈ Vart иx 6≡ t, тоСТОП: система неунифицируемаNFunc: если в системе есть уравнение f(t1 , .

. . , tk )g(s1 , . . . , sm ), где f 6= g, тоСТОП: система неунифицируема=Алгоритм унификацииПримерf(x, g(y)) = f(g(y), x)E=c = yFuncx = g(y)g(y) = xc =ySwapx = g(c)g(c) = g(c)y = cRed × 2x = g(y)g(y) = xy =cTrivx = g(c)y=cОтвет: {x/g(c), y/c} ∈ НОУ(E)приведённая системаАлгоритм унификацииПримерE=f(x, g(y)) = h(g(y), x)c = yNFuncСТОПОтвет: НОУ(E) = ∅Алгоритм унификацииПримерf(x, g(x)) = f(g(y), x)E=c = yСТОПNRedОтвет: НОУ(E) = ∅А всегда ли это работает как надо?Funcx = g(y)g(x) = xc = ySwap x = g(y)x = g(x)c = yАлгоритм унификацииТеорема об унификацииДля любой системы уравнений EI алгоритм унификации завершает работу на E(завершаемость)I по завершении работы алгоритмом выдаётсяподстановка или сообщение СТОП(успешность)I если выдана подстановка θ, то θ ∈ НОУ(E)(корректность)I если выдано сообщение СТОП, то система Eнеунифицируема(полнота)Доказательство теоремы.

Характеристики

Тип файла PDF

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

Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.

Список файлов лекций