Ещё одни лекции В.А. Захарова, страница 11

Тогда z(θη) = z и zμ = z.3. z = yi ∈ЗАДАЧА УНИФИКАЦИИПримерθ = {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 },η = {x/g (y ), y /z, u/c}.θη =ЗАДАЧА УНИФИКАЦИИПримерθ = {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 (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 (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}ЗАДАЧА УНИФИКАЦИИОпределениеПусть E1 и E2 — два логических выражения (термы, атомы,формулы и др.)Подстановка θ называется унификатором выражений E1 и E2 ,если E1 θ = E2 θ.Подстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2 , если1.

θ — унификатор выражений E1 и E2 ;2. для любого унификатора η выражений E1 и E2 существуеттакая подстановка ρ, для которой верно равенствоη = θρНОУ(E1 , E2 ) — множество наиболее общих унификатороввыражений E1 и E2 .ЗАДАЧА УНИФИКАЦИИПримерE1 = P(f (x1 ), x2 )E2 = P(y1 , c)η = {x1 /f (c), x2 /c, y1 /f (f (c))} — унификатор E1 и E2 , т.к.E1 η = P(f (f (c)), c) = E2 η.θ = {x2 /c, y1 /f (x1 )} — наиболее общий унификатор E1 и E2 ,т.к.E1 θ = P(f (x1 ), c) = E2 θ,η = θ{x1 /f (c)}.Выражения E1 и E2 унифицируемы , и θ ∈ НОУ(E1 , E2 ).ЗАДАЧА УНИФИКАЦИИПримерE1 = R(f (x1 ), x1 )E2 = R(y1 , f (y1 ))Выражения E1 и E2 не имеют унификаторов, иНОУ(E1 , E2 ) = ∅.ЗАДАЧА УНИФИКАЦИИЗадача унификациисостоит в том, чтобы для двух выражений E1 и E2 выяснить,являются ли эти выражения унифицируемыми,и, в случае их унифицируемости, вычислитьнаиболее общий унификатор.КОНЕЦ ЛЕКЦИИ 7.Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А.

ЗахаровЛекция 8.Алгоритм унификации.АЛГОРИТМ УНИФИКАЦИИПодстановка θ называется наиболее общим унификатором(НОУ) выражений E1 и E2 , если1. θ — унификатор выражений E1 и E2 , т. е. E1 θ = E2 θ;2. для любого унификатора η выражений E1 и E2 существуеттакая подстановка ρ, для которой верно равенствоη = θρЗадача унификациисостоит в том, чтобы для двух выражений E1 и E2 выяснить,являются ли эти выражения унифицируемыми,и, в случае их унифицируемости, вычислитьнаиболее общий унификатор E1 и E2 .АЛГОРИТМ УНИФИКАЦИИНачнем с самой простого варианта задачи унификации.Как найти НОУ выражений E1 и E2 , если одно из этихвыражений — переменная, т.

е. E1 = x ∈ Var ?Лемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x = t, то НОУ(x, t) = ∅.АЛГОРИТМ УНИФИКАЦИИЛемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x = t, то НОУ(x, t) = ∅.Доказательство.1. Случай x ∈/ Vart .θ = {x/t} — унификатор выражений x и t.Действительно, xθ = t и tθ = t (т. к. x ∈/ Vart ).Каков бы ни был унификатор η выражений x и t, верноη = {x/t}η.Возьмем произвольную переменную y , y ∈ Var .Если y = x, то x{x/t}η = tη = xη.

(почему? ) А еслиy = x, то y {x/t}η = y η.Таким образом, для любой переменной y верноy {x/t}η = y η, т. е. {x/t}η = η.АЛГОРИТМ УНИФИКАЦИИЛемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x = t, то НОУ(x, t) = ∅.Доказательство.2. Случай x ∈ Vart .Для любой подстановки θ длина терма xθ превосходит длинутерма t(x)θ.Поэтому xθ = tθ для любой подстановки θ, т. е. НОУ(x, t) = ∅.АЛГОРИТМ УНИФИКАЦИИОбщий случай.Пусть E1 = P(t1 , t2 , . . . , tn ), E2 = P(s1 , s2 , . .

. , sn ).Для решения задачи унификации сопоставим паре атомовE1 , E2 систему уравнений⎧t1 = s 1⎪⎪⎨t2 = s 2E(E1 , E2 ) :···⎪⎪⎩tn = s nи будем решать задачу унификации для систем уравнений.АЛГОРИТМ УНИФИКАЦИИОпределениеПодстановкаθ называется унификатором системы уравнений E⎧t=s⎪11⎪⎨t2 = s 2E:···⎪⎪⎩tn = s nесли для любого i, 1 ≤ i ≤ n, термы ti θ и si θ одинаковы.Фактически, унификатор θ = {x1 /r1 , . . . , xk /rk } — это решениесистемы уравнений E в свободной алгебре термов(эрбрановской интерпретации).Соответствующим образом определяется и наиболее общийунификатор системы уравнений(определение дать самостоятельно ).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))E1 :g (y ) = zявляется подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 θ :E1 :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 θ :E1 :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zне имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПримерНаиболее общим унификатором системы уравненийf (c, x) = f (y , g (y ))f (c, g (c)) = f (c, g (c))E1 θ :E1 :g (y ) = zg (c) = g (c)является подстановка θ = {x/g (c), y /c, z/g (c)}.А система уравненийf (c, y ) = f (y , g (y ))E1 :g (y ) = zПочему?не имеет решений (неунифицируема).АЛГОРИТМ УНИФИКАЦИИПростой случай.ОпределениеСистема уравнений E называется приведенной , если⎧⎪⎪ x1 = s 1⎨x2 = s 2E:···⎪⎪⎩xn = s nи при этом{x1 , .

. . , xn } ⊆ Var ,все переменные x1 , . . . , xn попарно различные,n{x1 , . . . , xn } ∩Varsi = ∅.i=1АЛГОРИТМ УНИФИКАЦИИПримерСистема уравнений E1 является приведенной, а E2 — нет.⎧⎧⎨ x = f (y , g (y ))⎨ x = f (y , g (y ))z =wz =wE1 :E2 :⎩⎩u = g (c)u = g (x)АЛГОРИТМ УНИФИКАЦИИПростой случай.Лемма (о приведенной системе)Если⎧ система уравнений E⎪ x1 = s 1⎪⎨x2 = s 2E:···⎪⎪⎩xn = s nявляется приведенной, то подстановка {x1 /s1 , x2 /s2 , . .

. , xn /sn }является наиболее общим унификатором системы E.ДоказательствоСамостоятельно. С использованием леммы о связке.АЛГОРИТМ УНИФИКАЦИИОбщий случай.Найти унификатор — это значит решить систему уравнений.Решать систему будем методом исключения переменных (как в«обычной» алгебре). Исключив все переменные, получимрешение (приведенную систему). Важно, чтобы все системыуравнений, которые мы будем строить в процессе «исключенияпеременных» были равносильны исходной системе.ОпределениеСистемы уравнений E1 и E1 называются равносильными , еслиНОУ(E1 ) = НОУ(E2 ).АЛГОРИТМ УНИФИКАЦИИОписание алгоритма унификации(Алгоритм Мартелли–Монтанари).Это — недетерминированный алгоритм, состоящий из 6 правил,которые можно применять в любом порядке до тех пор, покалибо ни одно из правил применить невозможно(построена приведенная система уравнений),либо применяется правило, устанавливающееневозможность унификации.Исходная система E0 ; i = 0;while применимо одно из 6 правил doвыбрать правило R, применимое к Ei ;Ei++ = R(Ei )odАЛГОРИТМ УНИФИКАЦИИПравила преобразования решения уравнений.(1) уравнение f (t1 , t2 , .

. . , tk ) = f (s1 , s2 , . . . , sk ) замещаетсясовокупностью уравнений t1 = s1 , t2 = s2 , . . . , tk = sk ; ),(2) если в системе есть уравнение f (t1 , . . . , tk ) = g (s1 , . . . , smгде f , g ∈ Func ∪ Const, f = g , то система уравненний неимеет решений: СТОП: “Нет унификатора";(3) уравнение s = x , где x ∈ Var , s ∈/ Var , замещаетсяуравнением x = s ;(4) уравнение s = s удаляется из системы;АЛГОРИТМ УНИФИКАЦИИПравила преобразования решения уравнений.(5) если в системе есть уравнение x = s , причемx ∈ Var ,x∈/ Vars , ипеременная x встречается в каких-либо другихуравнениях системы,то ко всем другим уравнения системы применяетсяподстановка {x/s} ;(6) если в системе есть уравнение x = s , причемx = s, x ∈ Vars , то система уравненний не имеет решений:СТОП: “Нет унификатора".АЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = yАЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y(1)=⇒АЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y⎧⎨ f (x, c) = y(1)y = f (z, z)=⇒ E1 :⎩f (u, v ) = yАЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y⎧⎨ f (x, c) = yy = f (z, z)E1 :⎩f (u, v ) = y⎧⎨ f (x, c) = y(1)y = f (z, z)=⇒ E1 :⎩f (u, v ) = yАЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y⎧⎨ f (x, c) = yy = f (z, z)E1 :⎩f (u, v ) = y⎧⎨ f (x, c) = y(1)y = f (z, z)=⇒ E1 :⎩f (u, v ) = y⎧⎨ y = f (x, c)(3)y = f (z, z)=⇒ E2 :⎩f (u, v ) = yАЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y⎧⎨ f (x, c) = yy = f (z, z)E1 :⎩f (u, v ) = y⎧⎨ y = f (x, c)y = f (z, z)E2 :⎩f (u, v ) = y⎧⎨ f (x, c) = y(1)y = f (z, z)=⇒ E1 :⎩f (u, v ) = y⎧⎨ y = f (x, c)(3)y = f (z, z)=⇒ E2 :⎩f (u, v ) = yАЛГОРИТМ УНИФИКАЦИИПример 1.E0 :f (f (x, c), y ) = f (y , f (z, z))f (u, v ) = y⎧⎨ f (x, c) = yy = f (z, z)E1 :⎩f (u, v ) = y⎧⎨ y = f (x, c)y = f (z, z)E2 :⎩f (u, v ) = y⎧⎨ f (x, c) = y(1)y = f (z, z)=⇒ E1 :⎩f (u, v ) = y⎧⎨ y = f (x, c)(3)y = f (z, z)=⇒ E2 :⎩f (u, v ) = y⎧⎨ y = f (x, c)(5)f (x, c) = f (z, z)=⇒ E3 :⎩f (u, v ) = f (x, c)АЛГОРИТМ УНИФИКАЦИИПример⎧ 1.E3 :⎨ y = f (x, c)f (x, c) = f (z, z)⎩f (u, v ) = f (x, c)АЛГОРИТМ УНИФИКАЦИИПример 1.⎧⎨ y = f (x, c)f (x, c) = f (z, z)E3 :⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨(1)x =z=⇒ E4 :c=z⎪⎪⎩f (u, v ) = f (x, c)АЛГОРИТМ УНИФИКАЦИИПример 1.⎧⎨ y = f (x, c)f (x, c) = f (z, z)E3 :⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨x =zE4 :c =z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨(1)x =z=⇒ E4 :c=z⎪⎪⎩f (u, v ) = f (x, c)АЛГОРИТМ УНИФИКАЦИИПример 1.⎧⎨ y = f (x, c)f (x, c) = f (z, z)E3 :⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨x =zE4 :c =z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨(1)x =z=⇒ E4 :c=z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (z, c)⎪⎪⎨(5)x =z=⇒ E5 :c =z⎪⎪⎩f (u, v ) = f (z, c)АЛГОРИТМ УНИФИКАЦИИПример 1.⎧⎨ y = f (x, c)f (x, c) = f (z, z)E3 :⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨x =zE4 :c =z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (z, c)⎪⎪⎨x =zE5 :c =z⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (x, c)⎪⎪⎨(1)x =z=⇒ E4 :c=z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (z, c)⎪⎪⎨(5)x =z=⇒ E5 :c =z⎪⎪⎩f (u, v ) = f (z, c)АЛГОРИТМ УНИФИКАЦИИПример 1.⎧⎨ y = f (x, c)f (x, c) = f (z, z)E3 :⎩f (u, v ) = f (x, c)⎧y = f (x, c)⎪⎪⎨x =zE4 :c =z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (z, c)⎪⎪⎨x =zE5 :c =z⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (x, c)⎪⎪⎨(1)x =z=⇒ E4 :c=z⎪⎪⎩f (u, v ) = f (x, c)⎧y = f (z, c)⎪⎪⎨(5)x =z=⇒ E5 :c =z⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (z, c)⎪⎪⎨(3)x =z=⇒ E6 :z =c⎪⎪⎩f (u, v ) = f (z, c)АЛГОРИТМ УНИФИКАЦИИПример⎧ 1.y = f (z, c)⎪⎪⎨x =zE6 :z =c⎪⎪⎩f (u, v ) = f (z, c)АЛГОРИТМ УНИФИКАЦИИПример⎧ 1.y = f (z, c)⎪⎪⎨x =zE6 :z =c⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (c, c)⎪⎪⎨(5)x =c=⇒ E7 :z =c⎪⎪⎩f (u, v ) = f (c, c)АЛГОРИТМ УНИФИКАЦИИПример⎧ 1.y = f (z, c)⎪⎪⎨x =zE6 :z =c⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (c, c)⎪⎪⎨x =cE7 :z =c⎪⎪⎩f (u, v ) = f (c, c)⎧y = f (c, c)⎪⎪⎨(5)x =c=⇒ E7 :z =c⎪⎪⎩f (u, v ) = f (c, c)АЛГОРИТМ УНИФИКАЦИИПример⎧ 1.y = f (z, c)⎪⎪⎨x =zE6 :z =c⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (c, c)⎪⎪⎨x =cE7 :z =c⎪⎪⎩f (u, v ) = f (c, c)⎧y = f (c, c)⎪⎪⎨(5)x =c=⇒ E7 :z =c⎪⎪⎩f (u, v ) = f (c, c)⎧y = f (c, c)⎪⎪⎪⎪⎨ x =c(1)z =c=⇒ E8 :⎪⎪u=c⎪⎪⎩v =cАЛГОРИТМ УНИФИКАЦИИПример⎧ 1.y = f (z, c)⎪⎪⎨x =zE6 :z =c⎪⎪⎩f (u, v ) = f (z, c)⎧y = f (c, c)⎪⎪⎨x =cE7 :z =c⎪⎪⎩f (u, v ) = f (c, c)⎧y = f (c, c)⎪⎪⎪⎪⎨ x =cz =cE8 :⎪⎪u=c⎪⎪⎩v =c⎧y = f (c, c)⎪⎪⎨(5)x =c=⇒ E7 :z =c⎪⎪⎩f (u, v ) = f (c, c)⎧y = f (c, c)⎪⎪⎪⎪⎨ x =c(1)z =c=⇒ E8 :⎪⎪u=c⎪⎪⎩v =c— приведенная системаАЛГОРИТМ УНИФИКАЦИИПример 1.⎧y = f (c, c)⎪⎪⎪⎪⎨ x =cf (f (x, c), y ) = f (y , f (z, z)) (1,3,5)z =cE0 :=⇒ E8 :f (u, v ) = y⎪⎪u=c⎪⎪⎩v =cθ = {x/c, y /f (c, c), z/c, u/c, v /c} ∈ НОУ(E0 )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )(1)=⇒АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(1)g (x) = v=⇒ E1 :⎩f (u, v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE1 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(1)g (x) = v=⇒ E1 :⎩f (u, v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE1 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(1)g (x) = v=⇒ E1 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(5)g (x) = v=⇒ E2 :⎩f (y , v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE1 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE2 :⎩f (y , v ) = f (x, y )⎧⎨ u=y(1)g (x) = v=⇒ E1 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(5)g (x) = v=⇒ E2 :⎩f (y , v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE1 :⎩f (u, v ) = f (x, y )⎧⎨ u=yg (x) = vE2 :⎩f (y , v ) = f (x, y )⎧⎨ u=y(1)g (x) = v=⇒ E1 :⎩f (u, v ) = f (x, y )⎧⎨ u=y(5)g (x) = v=⇒ E2 :⎩f (y , v ) = f (x, y )⎧⎨ u=y(3)v = g (x)=⇒ E3 :⎩f (y , v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )⎧⎨ u=yv = g (x)=⇒ E4 :⎩f (y , g (x)) = f (x, y )(5)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )⎧⎨ u=yv = g (x)=⇒ E4 :⎩f (y , g (x)) = f (x, y )⎧⎨ u=yv = g (x)E4 :⎩f (y , g (x)) = f (x, y )(5)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )⎧⎨ u=yv = g (x)=⇒ E4 :⎩f (y , g (x)) = f (x, y )⎧⎧u=y⎪⎪u=y⎨⎨(1)v = g (x)v = g (x)E4 :=⇒ E5 :y =x⎪⎩⎪f (y , g (x)) = f (x, y )⎩g (x) = y(5)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )⎧⎨ u=yv = g (x)=⇒ E4 :⎩f (y , g (x)) = f (x, y )⎧⎧u=y⎪⎪u=y⎨⎨(1)v = g (x)v = g (x)E4 :=⇒ E5 :y =x⎪⎩⎪f (y , g (x)) = f (x, y )⎩g (x) = y⎧u=y⎪⎪⎨v = g (x)E5 :y =x⎪⎪⎩g (x) = y(5)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧⎨ u=yv = g (x)E3 :⎩f (y , v ) = f (x, y )E4 :E5 :⎧⎨⎩⎧⎪⎪⎨⎪⎪⎩⎧⎨ u=yv = g (x)=⇒ E4 :⎩f (y , g (x)) = f (x, y )⎧u=y⎪⎪u=y⎨(1)v = g (x)v = g (x)=⇒ E5 :y =x⎪⎪f (y , g (x)) = f (x, y )⎩g (x) = y⎧u=yu=x⎪⎪⎨(5)v = g (x)v = g (x)=⇒ E6 :y =xy =x⎪⎪⎩g (x) = yg (x) = x(5)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧u=x⎪⎪⎨v = g (x)E6 :y =x⎪⎪⎩g (x) = xАЛГОРИТМ УНИФИКАЦИИПример 2.⎧u=x⎪⎪⎨v = g (x)E6 :y =x⎪⎪⎩g (x) = x⎧u⎪⎪⎨(3)v=⇒ E7 :y⎪⎪⎩x=x= g (x)=x= g (x)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧u=x⎪⎪⎨v = g (x)E6 :y =x⎪⎪⎩g (x) = x⎧u=x⎪⎪⎨v = g (x)E7 :y =x⎪⎪⎩x = g (x)⎧u⎪⎪⎨(3)v=⇒ E7 :y⎪⎪⎩x=x= g (x)=x= g (x)АЛГОРИТМ УНИФИКАЦИИПример 2.⎧u=x⎪⎪⎨v = g (x)E6 :y =x⎪⎪⎩g (x) = x⎧u=x⎪⎪⎨v = g (x)E7 :y =x⎪⎪⎩x = g (x)⎧u⎪⎪⎨(3)v=⇒ E7 :y⎪⎪⎩x(6)=x= g (x)=x= g (x)=⇒ СТОП: НЕТ УНИФИКАТОРА.АЛГОРИТМ УНИФИКАЦИИПример 2.⎧u=x⎪⎪⎨v = g (x)E6 :y =x⎪⎪⎩g (x) = x⎧u=x⎪⎪⎨v = g (x)E7 :y =x⎪⎪⎩x = g (x)⎧u⎪⎪⎨(3)v=⇒ E7 :y⎪⎪⎩x=x= g (x)=x= g (x)(6)=⇒ СТОП: НЕТ УНИФИКАТОРА.Система уравнений⎧⎨ g (u) = g (y )g (x) = vE0 :⎩f (u, v ) = f (x, y )не имеет решения (унификатора).АЛГОРИТМ УНИФИКАЦИИТеорема (об унификации)Какова бы ни была система уравнений E,1.