Спец часть (часть 1) (3 поток) (2015) (by Кибитова) (1161601), страница 14
Текст из файла (страница 14)
. . , CmG = C1 &C2 & . . . &CmС точки зрения декларативной семантики,Iпрограммные утверждения D и запросы G � этологические формулы,Iпрограмма P � это множество формул (база знаний),Iа правильный ответ на запрос � это такие значенияпеременных (подстановка), при которой запросоказывается логическим следствием базы знаний.n[i=0VarAiДЕКЛАРАТИВНАЯ СЕМАНТИКАОпределение (правильного ответа)Пусть P � логическая программа, G � запрос к P смножеством целевых переменных Y1 , . .
. , Yk .Тогда всякая подстановка ✓ = {Y1 /t1 , . . . , Yk /tk } называетсяответом на запрос G к программе P.Ответ ✓ = {Y1 /t1 , . . . , Yk /tk } называется правильным ответомна запрос G к программе P, еслиДЕКЛАРАТИВНАЯ СЕМАНТИКАP |= 8Z1 . . . 8ZN G ✓,где {Z1 , . . . , ZN } =k[Varti .i=1Теорема (об основном правильном ответе)Пусть G =?C1 , C2 , . . . , Cm � запрос к хорновской логическойпрограмме P. Пусть Y1 , . . .
, Yk � целевые переменные,t1 , . . . , tk � основные термы.Тогда подстановка ✓ = {Y1 /t1 , . . . , Yk /tk } являетсяправильным ответом на запрос G к программе P тогда иОПЕРАЦИОННАЯСЕМАНТИКАтолько тогда, когда P |= (C1 & . . . &Cm )✓.ЛОГИЧЕСКИХ ПРОГРАММКонцепция операционной семантикиПод операционной семантикой понимают правила построениявычислений программы. Операционная семантикаописывает, КАК достигается результат работы программы.Результат работы логической программы � это правильныйответ на запрос к программе. Значит, операционная семантикадолжна описывать метод вычисления правильных ответов.Запрос к логической программе порождает задачу ологическом следствии. Значит, вычисление ответа на запросдолжно приводить к решению этой задачи.Таким методом вычисления может быть разновидностьметода резолюций, учитывающая особенности устройствапрограммных утвержденийSLD-РЕЗОЛЮТИВНЫЕВЫЧИСЛЕНИЯОпределение (SLD-резолюции)ПустьIG = ? C1 , .
. . , Ci , . . . , Cm � целевое утверждение, вкотором выделена подцель Ci ,ID 0 = A00A01 , A02 , . . . , A0n � вариант некоторогопрограммного утверждения, в котором VarG \ VarD 0 = ;,I✓ 2 НОУ(Ci , A00 ) � наиб. общ. унификатор подцели Ci изаголовка программного утверждения A0 .Тогда запросG 0 = ?(C1 , .
. . , Ci0001 , A1 , A2 , . . . , An , Ci+1 , . . . , Cm )✓называется SLD-резольвентой программного утверждения D 0 изапроса G с выделенной подцелью C и унификатором ✓.IID 0 = A00A01 , A02 , . . . , A0n � вариант некоторогопрограммного утверждения, в котором VarG \ VarD 0 = ;,✓ 2 НОУ(Ci , A00 ) � наиб. общ.
унификатор подцели Ci изаголовка программного утверждения A0 .Тогда запросG 0 = ?(C1 , . . . , Ci0001 , A1 , A2 , . . . , An , Ci+1 , . . . , Cm )✓называется SLD-резольвентой программногоутверждения D 0 иSLD-РЕЗОЛЮТИВНЫЕВЫЧИСЛЕНИЯзапроса G с выделенной подцелью Ci и унификатором ✓.Определение (SLD-резолютивного вычисления)ПустьIG0 = ? C1 , C2 , .
. . , Cm � целевое утверждение,IP = {D1 , D2 , . . . , DN } � хорновская логическая программа.Тогда (частичным) SLD-резолютивным вычислением ,порожденным запросом G0 к логической программе Pназывается последовательность троек (конечная илибесконечная)(Dj1 , ✓1 , G1 ), (Dj2 , ✓2 , G2 ), . . . , (Djn , ✓n , Gn ), . . . ,в которой для любого i, iI1,Dji 2 P, ✓i 2 Subst, Gi � целевое утверждение (запрос);SLD-РЕЗОЛЮТИВНЫЕВЫЧИСЛЕНИЯI запрос Gi является SLD-резольвентой программногоSLD-РЕЗОЛЮТИВНЫЕВЫЧИСЛЕНИЯутверждения Dj и запроса Gi 1 с унификатором ✓i .iОпределение (SLD-резолютивного вычисления)Определение (SLD-резолютивного вычисления)Частичное SLD-резолютивное вычислениеЧастичное SLD-резолютивное вычислениеcomp = (Dj1 , ✓1 , G1 ), (Dj2 , ✓2 , G2 ), .
. . , (Djk , ✓n , Gn )comp = (Dj1 , ✓1 , G1 ), (Dj2 , ✓2 , G2 ), . . . , (Djk , ✓n , Gn )называетсяназываетсяI успешным вычислением (SLD-резолютивнымI успешнымопровержением),если G(SLD-резолютивнымвычислениемn = ⇤;если Gn = ⇤;Iопровержением),бесконечным вычислением, если comp � это бесконечнаяпоследовательность;I бесконечнымвычислением , если comp � это бесконечнаяIпоследовательность;тупиковым вычислением , если comp � это конечнаяпоследовательность,и приэтомдля�запросаGnI тупиковымвычислением, еслиcompэто конечнаяневозможнопостроитьниоднойSLD-резольвенты.SLD-РЕЗОЛЮТИВНЫЕпоследовательность, и при этом ВЫЧИСЛЕНИЯдля запроса Gnневозможно построить ни одной 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.IIP = {D1 , D2 , . . . , DN } � хорновская логическая программа,comp = (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-РЕЗОЛЮТИВНЫЕВЫЧИСЛЕНИЯSLD-РЕЗОЛЮТИВНЫЕ ВЫЧИСЛЕНИЯТеперь у нас есть два типа ответов на запросы к логическимТеперьу нас есть два типа ответов на запросы к логическимпрограммам:программам:I правильные ответы, которые логически следуют изI правильные ответы, которые логически следуют изпрограммы;программы;I вычисленные ответы, которые конструируются по ходуI вычисленные ответы, которые конструируются по ходуSLD-резолютивных вычислений.SLD-резолютивных вычислений.Правильные ответы � это то, что мы хотим получить,Правильные ответы � этото, что мы хотим получить,КОРРЕКТНОСТЬобращаясь с вопросамиОПЕРАЦИОННОЙк программе.обращаясь с вопросами к программе.СЕМАНТИКИВычисленные ответы � это то, что нам в действительностиВычисленные ответы � это то, что нам в действительностивыдает компьютер (интерпретатор программы).выдает компьютер (интерпретатор программы).Какова связь между правильными иКаковасвязь междуправильнымииТеорема(корректностиоперационнойсемантикивычисленнымиответами?вычисленнымиотносительнодекларативной ответами?семантики)ПустьIG0 = ? C1 , C2 , .
. . , Cm � целевое утверждение,ПОЛНОТАОПЕРАЦИОННОЙ СЕМАНТИКИIIP = {D1 , D2 , . . . , DN } � хорновская логическая программа,✓ � вычисленный ответ на запрос G0 к программе P.Тогда ✓ � правильный ответ на запрос G0 к программе P.Теорема полноты (главная).Пусть ✓ � правильный ответ на запрос ?G к хорновскойлогической программе P.Тогда существует такой вычисленный ответ ⌘ на запрос ?G кпрограмме P,что ✓ = ⌘⇢ длянекоторой подстановки ⇢.ПРАВИЛАВЫБОРАПОДЦЕЛЕЙПРАВИЛАВЫБОРА ПОДЦЕЛЕЙОпределение.ПРАВИЛАВЫБОРА ПОДЦЕЛЕЙОпределение.Определение.ОтображениеR, которое сопоставляет каждому непустомуОтображениеR,котороесопоставляеткаждомунепустомузапросуG:?Cодну из подцелейCi =R(G ) в этом1, C2 , .
. . , CmОтображение R,котороесопоставляеткаждомунепустомузапросуG:?C,C,...,CоднуизподцелейC=этом12miзапросе,называетсяподцелей.R(G)) вв этомзапросу G: ?C1 , C2 , .правилом. . , Cm однувыбораиз подцелейCi = R(Gзапросе, называетсяправиломвыбора подцелей.запросе,называетсяправиломвыбора подцелей.Длязаданногоправилавыбора подцелейR вычислениеДлязаданногоправилавыбораподцелейRвычислениезапросаG к логическойпрограммеP называетсяДля заданногоправила выбораподцелейR вычислениезапроса G к логическойпрограммеP называетсяR-вычислением,еслинакаждомшагевычисления очереднаязапроса G к логической программе P называетсяR-вычислениемесли на каждомшаге вычисленияочереднаяподцельв запросе,, выбираетсяпо правилуR.R-вычислениемесли на каждомшаге вычисленияочереднаяподцель в запросе выбирается по правилу R.подцельв запросе выбираетсяправилу R.Ответ,полученныйв результатепоуспешногоR-вычисления,Ответ,полученныйврезультатеуспешногоR-вычисления,называется R-вычисленным .Ответ, полученный в результате успешного R-вычисления,называется R-вычисленным .ТеоремаполнотыназываетсясильнойR-вычисленным.Теорема сильной полнотыТеоремасильнойполнотыКаковобы нибыло правиловыбора подцелей R, если ✓ �КаковобынибылоправилоподцелейлогическойR, если ✓ �правильный ответ на запрос Gвыбора0 к хорновскойКаково бы ни было правило выбораподцелей R, если ✓ �правильныйP,ответна запрос такойG0 к хорновскойлогическойпрограммето существуетR-вычисленныйответ ⌘,правильный ответ на запрос G0 к хорновской логическойпрограммеP, то существует такой R-вычисленный ответ ⌘,чторавенствоR-вычислением , если на каждом шаге вычисления очереднаяподцель в запросе выбирается по правилу R.Ответ, полученный в результате успешного R-вычисления,называется R-вычисленным .Теорема сильной полнотыКаково бы ни было правило выбора подцелей R, если ✓ �правильный ответ на запрос G0 к хорновской логическойпрограмме P, то существует такой R-вычисленный ответ ⌘,что равенство✓ = ⌘⇢ДЕРЕВЬЯЛОГИЧЕСКИХвыполняетсяВЫЧИСЛЕНИЙдля некоторой подстановки⇢.выполняется для некоторой подстановки ρ.ПРОГРАММОпределениеДеревом SLD-резолютивных вычислений запроса G0 клогической программе P называется помеченное корневоедерево TG0 ,P , удовлетворяющее следующим требованиям:1.
Корнем дерева является исходный запрос G0 ;2. Потомками каждой вершины G являются всевозможныеSLD-резольвенты запроса G (при фиксированномстандартном правиле выбора подцелей);3. Листовыми вершинами являются пустые запросы(завершающие успешные вычисления) и запросы, неимеющие SLD-резольвент (завершающие тупиковыеДЕРЕВЬЯВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХвычисления).ПРОГРАММИллюстрация⇣tP)⇣ @PP⇣qR@?'TG0 ,P?Gi⇣tP?Gi0 t⇣)⇣ @PPq t ?Gi0v?Gi00 t&$?G0qqq@@ t?G 000Ri?Gt j?t?⇤%СТРАТЕГИИ ВЫЧИСЛЕНИЙ ЛОГИЧЕСКИХПРОГРАММОпределениеСтратегией вычисления запросов к логическим программамназывается алгоритм построения (обхода) дереваSLD-резолютивных вычислений TG0 ,P всякого запроса G0 кпроизвольной логической программе PСтратегия вычислений называется вычислительно полной ,если для любого запроса G0 и любой логической программы PСТРАТЕГИИВЫЧИСЛЕНИЙЛОГИЧЕСКИХэта стратегия строит(обнаруживает) все успешныевычисления запроса G0 к программы PПРОГРАММФактически, стратегия вычисления � это одна стратегийобхода корневого дерева.
Как известно, таких стратегийсуществует много, но среди них выделяются две наиболеехарактерные:Iстратегия обхода в ширину , при которой деревостроится (обходится) поярусно � вершина i-го нестроится, до тех пор пока не будут построены все вершины(i 1)-го яруса;стратегия обхода в глубину с возвратом , при которойветви дерева обходятся поочередно � очередная ветвьдерева не обохдится, до тех пор пока не будут пройденыСТРАТЕГИИЛОГИЧЕСКИХвсе вершиныВЫЧИСЛЕНИЙтекущей ветви.IПРОГРАММСтратегия обхода в ширину является вычислительно полной,посколькуI каждый запрос имеет конечное число SLD-резольвент, ипоэтому в каждом ярусе дерева SLD-резолютивныхвычислений имеется конечное число вершин;I каждое успешное вычисление завершается на некоторомярусе;I и поэтому каждое успешное вычисление будет рано илипоздно полностью построено.Но строить интерпретатор логических программ на основестратегии обхода в ширину нецелесообразно.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
