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

Математическая логикаЛектор:Подымов Владислав Васильевич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неунифицируема(полнота)Доказательство теоремы.