8. Алгоритм унификации (В.А. Захаров - Лекции)

Описание файла

Файл "8. Алгоритм унификации" внутри архива находится в папке "В.А. Захаров - Лекции". PDF-файл из архива "В.А. Захаров - Лекции", который расположен в категории "лекции и семинары". Всё это находится в предмете "математическая логика и логическое программирование" из седьмого семестра, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст из PDF

Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 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 6= t, то НОУ(x, t) = ∅.АЛГОРИТМ УНИФИКАЦИИЛемма (о связке)Пусть x ∈ Var , t ∈ Term. Тогда1. Если x ∈/ Vart , то {x/t} ∈ НОУ(x, t);2. Если x ∈ Vart и x 6= t, то НОУ(x, t) = ∅.Доказательство.1.

Случай x ∈/ Vart .Iθ = {x/t} — унификатор выражений x и t.Действительно, xθ = t и tθ = t (т. к. x ∈/ Vart ).IКаков бы ни был унификатор η выражений x и t, верноη = {x/t}η.Возьмем произвольную переменную y , y ∈ Var .Если y = x, то x{x/t}η = tη = xη. (почему? ) А еслиy 6= 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 6= t, то НОУ(x, t) = ∅.Доказательство.2.

Случай x ∈ Vart .Для любой подстановки θ длина терма xθ превосходит длинутерма t(x)θ.Поэтому xθ 6= 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и при этомI{x1 , .

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

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

. . , tk0 ) = f (s10 , s20 , . . . , sk0 ) замещаетсясовокупностью уравнений t10 = s10 , t20 = s20 , . . . , tk0 = sk0 ;0 ),(2) если в системе есть уравнение f (t10 , . . . , tk0 ) = g (s10 , . . . , smгде f , g ∈ Func ∪ Const, f 6= g , то система уравненний неимеет решений: СТОП: “Нет унификатора";(3) уравнение s = x , где x ∈ Var , s ∈/ Var , замещаетсяуравнением x = s ;(4) уравнение s = s удаляется из системы;АЛГОРИТМ УНИФИКАЦИИПравила преобразования решения уравнений.(5) если в системе есть уравнение x = s , причемIIIx ∈ Var ,x∈/ Vars , ипеременная x встречается в каких-либо другихуравнениях системы,то ко всем другим уравнения системы применяетсяподстановка {x/s} ;(6) если в системе есть уравнение x = s , причемx 6= 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)=⇒ E5 :E4 :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)=⇒ E5 :E4 :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) = xg (x) = y(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.

Свежие статьи
Популярно сейчас