Лекции В.А. Захарова (1157993), страница 12

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

Текст из файла (страница 12)

. . , 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.

алгоритм унификации Мартелли-Монтанари всегдазавершает работу;2. если система уравнений E унифицируема , то в результатеработы алгоритма унификации будет построенаприведенная система уравнений, равносильная исходнойсистеме E;3. если система уравнений E неунифицируема , то врезультате работы алгоритма унификации будет выданосообщение СТОП: НЕТ УНИФИКАТОРА.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1.

Завершаемость алгоритма.Уравнение x = t, где x ∈ Var , x ∈/ Vart , будем называтьприведенным уравнением системы E , если переменная x несодержится ни в каких других уравнениях системы E.Переменную x в этом случае будем называть приведеннойпеременной системы EКаждой системе уравнений E сопоставим характеристикуH(E) = hh1 (E), h2 (E), h3 (E)i, — упорядоченную тройкунатуральных чисел, в которой1. h1 (E) — общее число неприведенных переменных,содержащихся в системе E;2. h2 (E) — общее число функц. символов и констант,содержащихся в левых частях уравнений системы E;3.

h3 (E) — общее число уравнений в системе E.АЛГОРИТМ УНИФИКАЦИИДоказательство. 1. Завершаемость алгоритма.На множестве упорядоченных троек натуральных чисел введемотношение лексикографического порядка :hM1 , M2 , M3 i  hN1 , N2 , N3 imN 1 < M1или N1 = M1 и N2 < M2или N1 = M1 , N2 = M2 и N3 < M3 .Пример.h2, 11, 2i  h2, 10, 5578i  h1, 1001, 78iАЛГОРИТМ УНИФИКАЦИИДоказательство.

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

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