Сводка определений - 2 (1158088), страница 4
Текст из файла (страница 4)
Ответ η на запрос к логической программе Р называется правильным, еслирезультат подстановки (C1 , C2 ,..., Cm )η является логическим следствием Р.Определение. Эрбрановская интерпретация I для логической программы Р называется еемоделью, если она является моделью для любого хорновского дизъюнкта, входящего в нее.Утверждение. I – модель для логической программы Р тогда и только тогда, когда длялюбого основного примера D0 = A '0 ← A '1 & A '2 &...& A 'n , если любое A 'i принадлежит I, тои A '0 также принадлежит I.Лемма (о пересечении моделей): Пусть Р – хорновская логическая программа, а М' и М'' - еемодели.
Тогда эрбрановская интерпретация М, являющаяся пересечением М' и М'' такжебудет моделью для Р.Следствие 1: пересечение произвольного числа моделей для Р также будет моделью.Следствие 2: пересечение всех моделей для Р также будет ее моделью. Такая модель будетназываться наименьшей Н-моделью (ННМ) и обозначаться как M PТеорема: Пусть Р – хорновская логическая программа, С - основной терм.
С являетсяследствием Р тогда и только тогда, когда он принадлежит ННМ Р.Определение. Пусть Р – хорновская логическая программа, D = A0 ← A1 & A2 &...& An некоторое ее программное утверждение, G : ? C1 ,..., Cm - запрос, а пересечение формальныхпараметров ( VarD ) с фактическими ( VarG ) пусто. Пусть Ci - подцель запроса G, аθ = НОУ (Сi , A0 ) . Тогда запрос G ' : ?(C1 ,..., Ci −1 , A1 , A2 ,..., An , Ci +1 ,..., Cm )θ , полученный из Gзаменой Ci на A1 , A2 ,..., An и последующей унификацией, называется SLD-резольвентойзапроса G и программного утверждения D с НОУ θ . При этом Ci называется выделеннойподцелью, а D – активизированным программным утверждением.15Математическая логика, сводка определений.
(с) 2006 GrGr (grgr@later.ru)Определение. SLD-резолютивным вычислением запроса G к хорновской логическойпрограмме Р называется последовательность пар (Gi ,θi ) , конечная или бесконечная, такая,что1) G0 = G2) Запрос Gi +1 - SLD-резольвента запроса Gi и варианта D' программного утверждения D,такого VarGi ∩ VarD ' = ∅ , а θi +1 - НОУ для этой резольвенты.3) Возможно три варианта вычисления:А) Gl = ? - успешное вычисление (SLD-резолютивное опровержение)Б) бесконечная последовательность – бесконечное вычислениеВ) обнаруживается, что очередную SLD-резольвенту построить нельзя – тупиковоевычисление.Определение.
Пусть (G1 ,θ1 ),..., (Gl −1 , θl −1 ), ( ,θl ) - успешное завершение запроса G кхорновской логической программе Р. Тогда подстановка θ = θ1θ 2 ...θ l | y1 , y2 ,..., yn называетсявычислимым ответом на запрос G к логической программе Р.Определение. Пусть Р – хорновская логическая программа. Тогда множеством успехов Рбудет называться следующее множество SuccP - это множество всех атомарных запросов,имеющих успешное SLD-резолютивное вычисление ( A ∈ BP - эрбрановскому базису Р).Определение. Пусть 2BP - множество всех подмножеств BP (множество всех эрбрановскихинтерпретаций). Оператором непосредственного следования для логической программы Рназывается функция TP : 2 BP → 2 BP , такая, что для любого подмножества BP (обозначим егоI) TP ( I ) = { A : A ∈ BP ; A ← A1 , A2 ,..., An } , где Аi принадлежит I – т.е.
все то, что следует изинтерпретации I по правилам логической программы Р.Утверждение. Для оператора непосредственного следования выполняются свойства:I1 ⊆ I 2 ⇒ TP ( I1 ) ⊆ TP ( I 2 )TP ( I1 ∪ I 2 ) ⊇ TP ( I1 ) ∪ TP ( I 2 )I ∈ BP ; I |= P ⇔ TP ( I ) ⊆ IОпределение. Интерпретация I называется неподвижной точкой операторанепосредственного следования, если выполняется равенство TP ( I ) = I . Множество всехнеподвижных точек оператора непосредственного следования обозначим как f pPОпределение.
I 0 называется наименьшей неподвижной точкой оператора TP , есливыполняются 2 свойства:1) I 0 - неподвижная точка оператора TP ;2) для любой другой неподвижной точки I выполняется свойство I 0 ⊆ I .Наименьшая неподвижная точка обозначается как lf pP .Теорема (о неподвижных точках).
В хорновской логической программе Р всегда∞существует наименьшая неподвижная точка, и lf pP = ∪ TPi (∅ ) = M P (т.е. наименьшаяi =016Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)неподвижная точка равна объединению всех следствий конечной кратности и являетсянаименьшей эрбрановской моделью для логической программы Р).Теорема (корректности операционной семантики): Пусть Р – хорновская логическаяпрограмма, G – запрос к ней, θ - вычисленный ответ на запрос G к Р.
Тогда вычисленныйответ θ - это правильный ответ.Следствие. SuccP ⊆ M P (т.е. множество успехов является подмножеством наименьшейэрбрановской модели).Определение. Пусть Р – хорновская логическая программа, G0 - запрос к Р. Тогда квазиSLD-резолютивным вычислением запроса G0 к Р называется последовательность пар(G '1 , θ '1 ),..., (G 'n , θ 'n ), (G 'n +1 , θ 'n +1 ) , которая удовлетворяет требованию: еслиG 'n −1 = ? C1 ,..., Ci −1 , Ci , Ci +1 ,..., Cm , D : A0 ← A1 ,..., Ak ∈ P и θ 'n - произвольный унификатор Ci иA0 , то G 'n = ?(C1 ,..., Ci −1 , A1 ,..., Ak , Ci +1 ,..., Cm )θ 'n .Заметим, что SLD-резолютивное вычисление – частный случай квази-SLD-резолютивноговычисления, поэтому корректность квази-SLD-резолютивного вычисления представляетсобой отдельную теорему.Теорема (о квази-SLD-резолютивных вычислениях): Если атом С входит в наименьшуюэрбрановскую интерпретацию ( C ∈ M P ), то запрос G0 : ? C имеет успешное квази-SLDрезолютивное вычисление.Следствие.
Если C1 , C2 ,..., Cn ∈ M P , то запрос G : ? C1 , C2 ,..., Cn имеет успешное квази-SLDрезолютивное вычисление.Лемма (о подъеме для SLD-резолюций): Пусть G – запрос к хорновской логическойпрограмме Р, η - конечная подстановка, а запрос Gη имеет успешное квази-SLD-резолютивное вычисление Gη ,(G '1 ,θ '1 ),..., ( ,θ 'n ) . Тогда запрос G имеет успешное SLDрезолютивное вычисление G, (G1 ,θ1 ),..., ( , θ n ) , причем существует такая конечнаяподстановка ρ , что ηθ '1 θ '2 ...θ 'n = θ1θ 2 ...θ n ρ .
Иначе говоря, результат частного случаязапроса для квази-SLD-резолютивного вычисления – это результат частного случая запросадля SLD-резолютивного вычисления.Теорема (о полноте; ван Эмдена): Если атом C ∈ M P , то C ∈ SuccP .Теорема (о полноте; Кларка): Пусть G – запрос к хорновской логической программе Р, θ правильный ответ на G. Тогда существует вычисленный ответ η , такой, что для некоторойконечной подстановки ρ выполняется равенство θ = ηρ (т.е. любой правильный ответявляется частным случаем некоторого вычисленного ответа).Машина Тьюринга:Определение. Ленточный алфавит A = {a0 ,..., an } - это множество допустимых значенийячеек памяти (символ a0 называется пустым). Слово в алфавите А называется ленточнымсловом.Определение.
Алфавит состояний Q = {q 0 , q1 ,..., qm ,...} - это множество состояний, причемсостояние q0 называется заключительным, а состояние q1 - начальным.17Математическая логика, сводка определений. (с) 2006 GrGr (grgr@later.ru)Определение. Ленточная конфигурация – это тройка d =< w1 , q, w2 > , где w1 - ленточноеслово, которое является содержимым ленты слева от обозреваемой ячейки, q - текущеесостояние машины Тьюринга, w2 - слово, состоящее из самой ячейки и содержимого лентысправа от нее.Определение. Команда машины Тьюринга – это пятерка < q, a, b, q ', D > , где q и q' –состояния, a, b – символы из алфавита А, D ∈ {L, R} .Определение. Машиной Тьюринга называется тройка T =< A, QT , ΠT > , где А – ленточныйалфавит, QT – конечное подмножество множества состояний, ПТ – множество команд.Важное ограничение: для любого состояния, отличного от заключительного, и символа изленточного алфавита существует единственная команда.Определение.
Отношением непосредственного перехода называется отношение T : α → β ,*где α , β - состояния машины Тьюринга. Обозначим a ⎯⎯→ β транзитивное замыканиеTотношения непосредственного перехода.Для каждой машины Тьюринга определим функцию FT : q1 → q0 , причем если α - начальнаяконфигурация, то FT (α ) = β тогда и только тогда, когда β - заключительная конфигурация,*и a ⎯⎯→β .TТезис Чёрча: Для любой функции ϕ : q1 → q0 существует алгоритм вычисления этойфункции тогда и только тогда, когда ϕ = FT для некоторой машины Тьюринга.Введем дополнительные обозначения: nil – 0-местный функциональный символ (константа),• - 2-местный функциональный символ, и введем отображение множества машин Тьюрингана множество логических программ: Compile : T → PТеорема. Пусто Т – машина Тьюринга, Compile(T ) = P - логическая программа.
Тогда длялюбой начальной конфигурации α 0 =< ai1 ,..., aik ; q1 ; b j1 ,..., b jn > существует заключительная*конфигурация β 0 =< a 'l1 ,..., a 'lm ; q0 ; b 'r1 ,..., b 'rt > , такая, что a ⎯⎯→ β , тогда и только тогда,Tкогда запрос Gα 0 : ? R (•( aik , •( aik −1 ,..., ( ai1 , nil )...), q1 , •(b j1 ,..., (b jn , nil )...)) имеет успешное SLDрезолютивное вычисление с ответом{}η = u •(a ' , •(...(a ' , nil )...) ; v q ; w •(b ' , •(...(b ' , nil )...)) .lml10r1rtТеорема (Чёрча; о неразрешимости проблемы общезначимости для классическойлогики предикатов): Не существует алгоритма, который для любой формулы ϕ позволялбы проверить ее общезначимость, т.е.
не существует алгоритма, который выдавал бы навыходе 1, если формула ϕ общезначима, и 0 в противном случае.Определение. Правилом выбора подцелей называется отображение R : ? C1 ,..., Cn → Ci (т.е.отображение, показывающее, какой атом должен быть выбран на текущем этапевычисления).Определение. SLD-резолютивное вычисление называется R-вычислением, если на каждомшаге вычисления очередная подцель выбирается по правилу R.18Математическая логика, сводка определений.
(с) 2006 GrGr (grgr@later.ru)Определение. Вычисленный ответ, полученный в результате R-вычисления называется Rвычисленным ответом.Лемма (переключательная): Пусть Р – хорновская логическая программа, G0 - запрос кней, пусть также имеется SLD-резолютивное вычисление G0 , (G1 ,θ1 ),..., ( , θ n ) , причем G1 иG2 - этапы SLD-резолютивного вычисления, на которых i-ая подцель была раскрыта поправилу D1 и D2 соответственно.
Тогда существует SLD-резолютивное вычислениеG0 , (G '1 ,θ '1 ), (G '2 , θ '2 ),..., ( ,θ 'n ) , такое, что на этапе G '1 раскрытие происходило по правилуD2 , а на этапе G '2 - по правилу D1 , при этом для вычисленных ответов η и η ' существуютконечные подстановки ρ и ρ ' , такие, что η = η ' ρ ' , η ' = ηρ .Теорема: Пусть Р – хорновская логическая программа, G – запрос к ней, R и R' – различныеправила выбора. Тогда если η - R-вычислимый ответ на G к Р, то существует такой R'вычислимый ответ η ' , такой, что η = η ' ρ ' и η ' = ηρ для некоторых конечных перестановок(переименований) ρ и ρ ' .Теорема (сильной полноты): Пусть G – запрос к хорновской логической программе Р, R –правило выбора, θ - правильный ответ на G к Р.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
