LectLog13 (1158006)
Текст из файла
Основыматематическойлогики и логическогопрограммированияЛЕКТОР: В.А. ЗахаровЛекция 13.Операционная семантикалогических программ:SLD–резолютивные вычисления.Корректность операционнойсемантики.ОПЕРАЦИОННАЯ СЕМАНТИКАЛОГИЧЕСКИХ ПРОГРАММКонцепция операционной семантикиПод операционной семантикой понимают правила построениявычислений программы.
Операционная семантикаописывает, КАК достигается результат работы программы.Результат работы логической программы — это правильныйответ на запрос к программе. Значит, операционная семантикадолжна описывать метод вычисления правильных ответов.Запрос к логической программе порождает задачу ологическом следствии. Значит, вычисление ответа на запросдолжно приводить к решению эту задачу.Таким методом вычисления может быть разновидностьметода резолюций, учитывающая особенности устройствапрограммных утверждений.ОПЕРАЦИОННАЯ СЕМАНТИКАЛогически предпосылки операционной семантикиЗапрос G (Y1 , . . .
Ym ) =? C1 , C2 , . . . , Cm к логической программеP = {D1 , . . . , DN } порождает задачу о логическом следствии:{D1 , . . . , DN } |= ∃Y1 . . . ∃Ym (C1 &C2 & . . . &Cm ),которая равносильна задаче об общезначимости|= D1 & . . . &DN → ∃Y1 . . . ∃Ym (C1 &C2 & . . . &Cm ),которая равносильна задаче о противоречивости формулы¬(D1 & . . . &DN → ∃Y1 .
. . ∃Ym (C1 &C2 & . . . &Cm ),равносильной формулеD1 & . . . &DN & ∀Y1 . . . ∀Ym (¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm ),ОПЕРАЦИОННАЯ СЕМАНТИКАЛогически предпосылки операционной семантикиПолученную формулуD1 & . . . &DN & ∀Y1 . . . ∀Ym (¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm ),можно рассматривать как систему дизъюнктовSP,G = {D1 , . . . , DN , ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬Cm },и доказывать ее противоречивость методом резолюций.ОПЕРАЦИОННАЯ СЕМАНТИКАЛогические программы и хорновские дизъюнктыКаждому утверждению логической программы сопоставимхорновский дизъюнкт:Правило: D 0 = A0 ← A1 , A2 , . .
. , AnD 0 = A0 ∨ ¬A1 ∨ ¬A2 ∨ · · · ∨ ¬AnФакт: D 00 = AD 00 = AЗапрос: G = ? C1 , C2 , . . . , CmG = ¬C1 ∨ ¬C2 ∨ · · · ∨ ¬CmКак это принято у дизъюнктов, предполагается, что всеОПЕРАЦИОННАЯ СЕМАНТИКАЛогические программы и хорновские дизъюнктыМы будем применять специальную стратегию построениярезолютивного вывода:G0Di 1?)G1Di 2?)Gq2qqDi k)?Selection rule driven Linear resolution with Definite clausesSLD-резолюцияSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)ПустьIG = ? C1 , .
. . , Ci , . . . , Cm — целевое утверждение, вкотором выделена подцель Ci ,ID 0 = A00 ← A01 , A02 , . . . , A0n — вариант некоторогопрограммного утверждения, в котором VarG ∩ VarD 0 = ∅,Iθ ∈ НОУ(Ci , A00 ) — наиб. общ. унификатор подцели Ci изаголовка программного утверждения A0 .Тогда запросG 0 = ?(C1 , . . . , Ci−1 , A01 , A02 , . . . , A0n , Ci+1 , . . .
, Cm )θназывается SLD-резольвентой программного утверждения D 0 изапроса G с выделенной подцелью Ci и унификатором θ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmКОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmКОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , .
. . , CmD = A0 ← A1 , A2 , . . . , An ;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , .
. . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;θ = НОУ(Ci , A00 )КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ? C1 , . . . , Ci , . . . , CmD 0 = A00 ← A01 , A02 , . . . , A0n ;9?θ = НОУ(Ci , A00 )G 0 = ? (C1 , . . .
, Ci−1 , A01 , A02 , . . . , A0n , Ci+1 , . . . , Cm )θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолюции)G = ¬C1 ∨ · · · ∨ ¬Ci ∨ · · · ∨ ¬CmD 0 = A00 ∨ ¬A01 ∨ ¬A02 ∨ · · · ∨ A0n ;9?θ = НОУ(Ci , A00 )G 0 = (¬C1 ∨· · · ∨¬Ci−1 ∨¬A01 ∨¬A02 ∨ · · · ∨¬A0n ∨¬Ci+1 ∨ · · · ∨¬Cm )θКОММЕНТАРИИ.Действительно, это резольвента двух дизъюнктовSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D = R(Y , X ) ← P(X ), R(c, Y );КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );?9θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}G 0 = ? (P(X ), P(X1 ), R(c, Y1 ), R(Y , c))θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 1.G = ? P(X ), R(X , f (Y )), R(Y , c)D 0 = R(Y1 , X1 ) ← P(X1 ), R(c, Y1 );?9θ = НОУ(R(X ,f (Y )),R(Y1 ,X1 )) = {Y1 /X ,X1 /f (Y )}G 0 = ? P(X ), P(f (Y )), R(c, X ), R(Y , c)КОММЕНТАРИИ.Вот она.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil)КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil)КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D = R(X nil, Y ) ←;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,так чтобы VarD 0 ∩ VarG = ∅.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;...
.θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.КОММЕНТАРИИ.Вычисляем Наиболее Общий Унификатор.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;?9... .θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.G 0 = ? ( )θКОММЕНТАРИИ.Строим SLD-резольвентуSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 2..G = ? R(X , X nil).D 0 = R(X1 nil, Y1 ) ←;?9G0 = КОММЕНТАРИИ.Вот она.... .θ = НОУ(R(X , X nil),R(X1 nil, Y1 )) ={X /X1 nil,Y1 /(X1 nil) nil}.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y )КОММЕНТАРИИ.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y )КОММЕНТАРИИ.Выделяем подцель в запросе.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D = R(X nil, X ) ←;КОММЕНТАРИИ.Выбираем программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, X1 ) ←;КОММЕНТАРИИ.Переименовываем переменные в выбранном утверждении,SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Атомы неунифицируемы!SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Значит, SLD-резольвенту нельзя построить.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 3..G = ? R(X , X nil), P(c, Y ).D 0 = R(X1 nil, Y1 ) ←;..НОУ(R(X , X nil),R(X1 nil, X1 )) = ∅КОММЕНТАРИИ.Нужно выделить другую подцель иливыбрать другое программное утверждение.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа.Тогда (частичным) SLD-резолютивным вычислением ,порожденным запросом G0 к логической программе Pназывается последовательность троек (конечная илибесконечная)(Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , Gn ), . . . ,в которой для любого i, i ≥ 1,IDji ∈ P, θi ∈ Subst, Gi — целевое утверждение (запрос);Iзапрос Gi является SLD-резольвентой программногоутверждения Dji и запроса Gi−1 с унификатором θi .SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)Частичное SLD-резолютивное вычислениеcomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . .
. , (Djk , θn , Gn )называетсяIуспешным вычислением (SLD-резолютивнымопровержением), если Gn = ;Iбесконечным вычислением, если comp — это бесконечнаяпоследовательность;Iтупиковым вычислением, если comp — это конечнаяпоследовательность, и при этом для запроса Gnневозможно построить ни одной SLD-резольвенты.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯОпределение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , .
. . , Cm — целевое утверждение с целевымипеременными Y1 , Y2 , . . . , Yk ,IP = {D1 , D2 , . . . , DN } — хорновская логическая программа,Icomp = (Dj1 , θ1 , G1 ), (Dj2 , θ2 , G2 ), . . . , (Djn , θn , ) —успешное SLD-резолютивное вычисление, порожденноезапросом G к программе P.Тогда подстановкаθ = (θ1 θ2 .
. . θn )|Y1 ,Y2 ,...,Yk ,представляющая собой композицию всех вычисленныхунификаторов θ1 , θ2 , . . . , θn , ограниченную целевымипеременными Y1 , Y2 , . . . , Yk ,называется вычисленным ответом на запрос G0 к программе P.SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)...G0 =?elem(X , a b c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..G1 =?elem(X1 , b c nil)...? elem(X , a b c nil)..
θ1 = {X /X1 , Y1 /a, L1 /b c nil}?SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );.. θ1 = {X /X1 , Y1 /a, L1 /b c nil}?...G1 =?elem(X1 , b c nil)elem(X2 ,Y2 L2 ) ← elem(X2 ,L2 );?.θ2 = {X1 /X2 , Y2 /b, L2 /c nil}.G2 =?elem(X2 , c nil)SLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯПример 4.Логическая программа P:.elem(X , Y .L) ← elem(X , L);elem(X , X L);Запрос G0 :...? elem(X , a b c nil)....G0 =?elem(X , a b c nil)elem(X1 ,Y1 L1 ) ← elem(X1 ,L1 );..
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
