Лекции по семантика на езиците за програмиране
Лема (съгласуваност на заместване и стойност)
Изтегляне 3.6 Mb.
|
Лема (съгласуваност на заместване и стойност): Нека (X1, …, Xn, , , …, ) e терм. Нека 1 ( , , …, ), 2 ( , , …, ), …, n ( , , …, ) са функционални термове и F . Тогава (1 (), 2 (), …, n (), ) = (X/, F)(). Доказателство: индукция по построението на . Нека е константа, = c. Тогава (1 (), 2 (), …, n (), ) = c, (X/, F) = c и (X/, F)() = c (1 (), 2 (), …, n (), ) = (X/, F)(). Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Тогава (1 (), 2 (), …, n (), ) = i () и (X/, F) = i (F), така че (X/, F)() = i () (1 (), 2 (), …, n (), ) = (X/, F)(). Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Тогава (1 (), 2 (), …, n (), ) = = f* (1 (1 (), 2 (), …, n (), ), 2 (1 (), 2 (), …, n (), ), …, l (1 (), 2 (), …, n (), )) = f* (1 (X/, F)(), 2 (X/, F)(), …, l (X/, F)()) = f (1 (X/, F), 2 (X/, F), …, l (X/, F))() = = f (1, 2, …, l)(X/, F)() = (X/, F)(). Използвали сме индукционното предположение и дефиницията за стойност на терм. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Нека (1 (), 2 (), …, n (), ) = tt. Тогава (1 (), 2 (), …, n (), ) = 1 (1 (), 2 (), …, n (), ). От друга страна (X/, F) = if (X/, F) then 1 (X/, F) else 2 (X/, F). По индукционното предположение (X/, F)() = tt и 1 (X/, F)() = = 1 (1 (), 2 (), …, n (), ). При това положение, (X/, F)() = 1 (X/, F)() = 1 (1 (), 2 (), …, n (), ) = = (1 (), 2 (), …, n (), ). Случаят (1 (), 2 (), …, n (), ) = ff се разглежда абсолютно аналогично. Нека (1 (), 2 (), …, n (), ) = . Тогава (1 (), 2 (), …, n (), ) = . От индукционното предположение имаме (X/, F)() = (X/, F)() = (1 (), 2 (), …, n (), ) = (X/, F)(). Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (1 (), 2 (), …, n (), ) = = i (1 (1 (), 2 (), …, n (), ), 2 (1 (), 2 (), …, n (), ), …,
= (1, 2, …, )(X/, F)() (X/, F)(). Използвали сме индукционното предположение и дефиницията за стойност на терм. Твърдение (за монотонност): Нека (X, F) е терм, a, b Nn, a b и , F , . Тогава (a, ) (b, ). Доказателство: индукция по построението на . Нека е константа, = c. Тогава (a, ) = c = (b, ). Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Тогава (a, ) = ai, (b, ) = bi и ai bi, тъй като a b. Така (a, ) (b, ). Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме (a, ) = f* (1 (a, ), 2 (a, ), …, l (a, )), (b, ) = f* (1 (b, ), 2 (b, ), …, l (b, )). От индукционното предположение имаме i (a, ) i (b, ) за всяко i { 1, 2, …, l }. Имаме, че f* е точна f* е монотонна f* (1 (a, ), 2 (a, ), …, l (a, )) f* (1 (b, ), 2 (b, ), …, l (b, )), т.е. (a, ) (b, ). Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Нека (a, ) = . Тогава (a, ) (b, ). Нека (a, ) . Тогава (а, ) = tt и (a, ) = 1 (a, ) или (а, ) = ff и (a, ) = 2 (a, ). Нека (а, ) = tt и (a, ) = 1 (a, ). От индукционното предположение имаме (a, ) (b, ) (b, ) = tt. Тогава (b, ) = 1 (b, ). От индукционното предположение 1 (a, ) 1 (b, ) (a, ) (b, ). Случаят (а, ) = ff и (a, ) = 2 (a, ) се разглежда аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (a, ) = i (1 (a, ), 2 (a, ), …, (a, )), (b, ) = i (1 (b, ), 2 (b, ), …, (b, )). От индукционното предположение имаме, че j (a, ) j (b, ) за всяко j { 1, 2, …, ni }. Освен това i е непрекъснато i е монотонно (a, ) = i (1 (a, ), 2 (a, ), …, (a, )) i (1 (b, ), 2 (b, ), …, (b, )). Имаме i i i (1 (b, ), 2 (b, ), …, (b, )) i (1 (b, ), 2 (b, ), …, (b, )) = = (b, ). Така (a, ) (b, ). С всеки терм от тип Nat или условен терм (X1, …, Xn, , , …, ) свързваме изображение Г на F в множеството на тоталните функции дефинирани в Nn и приемащи стойности в N, което се дефинира по следния начин: Г () = a. (а, ) за всяко F . Твърдението за монотонност показва, че Г () е монотонна функция за всяко F . Действително, за всеки a, b Nn, a b, имаме (a, ) (b, ), т.е. Г ()(a) Г ()(b). Така Г : F F n. Освен това, твърдението за монотонност показва, че Г е монотонно изображение. Действително, нека a Nn, F , F и . Тогава (a, ) (a, ), т.е. Г ()(a) Г ()(a). Така Г () Г (). След малко ще видим, че Г е непрекъснато изображение. Да отбележим, че това не следва от неговата монотонност, както беше в случаите по-горе, тъй като множеството F съдържа монотонни редици с безброй много елементи.
{ k} е монотонно растяща редица от елементи на F , = . Toгава за всяко a N (B), a имаме (a, ) = a съществува k N, такова че (a, k) = a. Доказателство: нека съществува k N, такова че (a, k) = a . От твърдението за монотонност имаме (a, k) (a, ) (a, ) = a. Нека (a, ) = a . С индукция по построението на ще покажем, че съществува k N, такова че (a, k) = a. Нека е константа, = c. Имаме (a, ) = a a = c. Също, (a, k) = c за всяко k N. Така, например, при k = 0 имаме (a, 0) = a. Нека е обектова променлива, = Xi, i { 1, 2, …, n }. Имаме (a, ) = ai ai = a. Също, (a, k) = ai за всяко k N. Така, например, при k = 0 имаме (a, 0) = a. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме (a, ) = f* (1 (a, ), 2 (a, ), …, l (a, )) = = а i (a, ) за всяко i = 1, 2, …, l, тъй като f* е точна функция. От индукционното предположение за всяко i = 1, 2, …, l съществува ki N, такова че i (a, ) = i (a, ). Избираме k = max (k1, k2, …, kl). Естествено, k за всяко i = 1, 2, …, l и от твърдението за монотонност получаваме i (a, ) i (a, k). Имаме i (a, ) i (a, ) = i (a, k) за всяко i = 1, 2, …, l. Последователно получаваме (a, k) = f* (1 (a, k), 2 (a, k), …, l (a, k)) = f* (1 (a, ), i (a, ), …, i (a, )) = f* (1 (a, ), 2 (a, ), …, l (a, )) = а. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (a, ) = i (1 (a, ), 2 (a, ), …, (a, )) = а . Тук не можем да твърдим, че j (a, ) за всяко j { 1, 2, …, ni}, тъй като в общия случай i не е точна функция. Имаме = i = , i (1 (a, ), 2 (a, ), …, (a, )) = а (твърдение от по-горе) съществува k0 N, такова че (1 (a, ), 2 (a, ), …, (a, )) = а. Нека j { 1, 2, …, ni}. Ако j (a, ) = , полагаме kj = 0. Ако j (a, ) , то от индукционното предположение съществува kj N, такова че j (a, ) = j (a, ). Избираме k = max (k0, k1, …, ). Имаме k ki и
ki (1 (a, ), 2 (a, ), …, (a, )) = a. Нека j { 1, 2, …, ni}. Нека j (a, ) = . От монотонността имаме j (a, k) j (a, ) j (a, k) = . Нека j (a, ) . От монотонността имаме j (a, ) = j (a, ) j (a, k) j (a, k) = j (a, ). И така, j (a, k) = j (a, ) за всяко j { 1, 2, …, ni}. Окончателно, (a, k) = ki (1 (a, k), 2 (a, k), …, (a, k)) = = ki (1 (a, ), 2 (a, ), …, (a, )) = a. Следствие: Нека (X, F) е терм. Нека a Nn, { k} е монотонно растяща редица от елементи на F , = . Тогава (a, ) = . Доказателство: преди всичко от твърдението за монотонност { (a, k) } е монотонна редица, така че съществува . Нека (a, ) = . От твърдението за монотонност (a, k) (a, ) = за всяко k N (a, k) = за всяко k N = = (a, ). Нека (a, ) . От твърдението за непрекъснатост съществува k N, такова че (a, k) = (a, ). Имаме (a, k) (a, k) = (a, ) = . Следствие: За всеки терм от тип Nat или условен терм (X, F), дефинираното Г е непрекъснато изображение на F във F n. Доказателство: вече показахме, че Г е монотонно изображение. Така, достатъчно е да покажем, че Г ( ) = за всяка монотонно растяща редица { k} от елементи на F . Нека a Nn. Тогава Г ( )(a) = (a, ) = = = . Използвали сме предното следствие и характеризацията на точните горни граници на монотонни редици от непрекъснати изображения в области на Скот.
0 (X1, …, Xn, , , …, ), where (X1, …, ) = i (X1, …, , , , …, ), i = 1, 2, …, k. Нека Гi : F , Гi = , i = 1, 2, …, k. Разглеждаме системата за изображенията Г1, Г2, …, Гk: Г1 (1, 2, …, k) = 1 Г2 (1, 2, …, k) = 2 … Гk (1, 2, …, k) = k Тъй като Г1, Г2, …, Гk са непрекъснати изображения (предното следствие), то системата притежава най-малко решение = (1, 2, …, k). При това е и най-малко квазирешение. Полагаме = a. 0 (a, ) = (), F n. Функцията DN (R) : Nn N, дефинирана с DN (R)(а) (a), ако (a) , ! DN (R)(a), ако (a) = , за всяко a Nn наричаме денотационна семантика на програмата R с предаване по име. Нашата най-близка цел е да покажем, че денотационната и операционната семантика по име съвпадат за всяка програма R.
за Г1, Г2, …, Гk, което е и най-малко квазирешение на тази система. Твърдение: Нека (F) е функционален терм, c е константа от типа на и R c. Тогава () = c. Доказателство: провеждаме пълна индукция по дължината на извода R c. Нека R c с дължина на извода k и твърдението е изпълнено за изводи R c с дължини по-малки от k. Разглеждаме случаи в зависимост от вида на . Нека е константа, = d. Имаме R c. От лемата за извода получаваме d = c. Тогава () d = c. Нека е основна операция, = f (1, 2, …, l). Имаме R c с дължина на извода k. От лемата за извода съществуват константи c1, c2, …, cl, такива че R j cj, j = 1, 2, …, l с дължина на извода по-малка от k и f (c1, c2, …, cl) = c. От индукционното предположение имаме j () = cj, j = 1, 2, …, l. Тогава () = f* (1 (), 2 (), …, l ()) = f* (c1, c2, …, cl) = f (c1, c2, …, cl) = c. Използвали сме, че cj , j = 1, 2, …, l и че f* е точното продължение на f. Нека е условен терм, = if then 1 else 2. Имаме R c с дължина на извода k. От лемата за извода R tt и R 1 c или R ff и R 2 c, при това тези изводи са с дължина по-малка от k. Нека R tt и R 1 c. От индукционното предположение имаме () = tt, 1 () = c () = c. Случаят R ff и R 2 c се разглежда аналогично. Нека е обръщение към функция, = (1, 2, …, ). Имаме R c с дължина на извода k, така че от лемата за извода R i (X1/1, X2/2, …, / , F) c с дължина на извода по-малка от k. Oт индукционното предположение получаваме i (X1/1, X2/2, …, / , F)() = c. От лемата за съгласуване на заместване и стойност получаваме i (1 (), 2 (), …, (), ) = c. Имаме () = i (1 (), 2 (), …, ()) = Гi ()(1 (), 2 (), …, ()) = = i (1 (), 2 (), …, (), ) = c. Използвали сме, че е решение на системата за Г1, Г2, …, Гk.
Доказателство: нека ON (R)(a) b. Тогава R 0 (X/a, F) b. От предното твърдение получаваме 0 (X/a, F)() = b. От лемата за съгласуване на заместване и стойност получаваме 0 (a, ) = b . При това положение, DN (R)(a) b. Така ОN (R) DN (R). Нека (F) е функционален терм. Определяме елемент [] N (B) с индукция по построението на :
[] = f* ([1], [2], …, [l]), където f* е точното продължение на f.
[] = [1], ако [] = tt, [] = [2], ако [] = ff, [] = , ако [] = .
4.1. Aко съществува a N, такова че R i (X/, F) a, определяме [] = a. 4.2. Ако не съществува такова a N, че R i (X/, F) a, определяме [] = . Дефиницията е коректна, т.е. на всеки терм съпоставяме единствено [], тъй като е в сила еднозначност на опростяването по име.
Тогава R a. Доказателство: индукция по построението на . Нека е константа, = d. Имаме [] = a а = d и R a. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме [] = a съществуват a1, a2, …, al, такива че [1] = a1, [2] = a2, …, [l] = al и f* (a1, a2, …, al) = a. Имаме, че f* е точна функция и a aj за всяко j = 1, 2, …, l. От индукционното предположение R j aj, j = 1, 2, …, l. Освен това f (a1, a2, …, al) = a, тъй като f* (a1, a2, …, al) = a и f* е точното продължение на f. Така R a. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Имаме [] = a . Тогава [] = tt и [1] = a или [] = ff и [2] = a. Нека [] = tt и [1] = a. От индукционното предположение получаваме R tt и R 1 a. Тогава R a. Случаят [] = ff и [2] = a се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме [] = a . От дефиницията на [] получаваме R i (X/, F) a. От правилото за предаване по име получаваме R а. Твърдение: За всеки функционален терм (F) е изпълнено: () []. Доказателство: ще припомним конструкцията на от теоремата на Кнастер-Тарски. Имаме = , 0 = (1, 2, …, k), r+1 = (Г1 (r), Г2 (r), …, Гk (r)) за всяко r N. Тук с i сме означили най-малкият елемент на - константната функция , i = 1, 2, …, k. Ще покажем, че (r) [] с индукция по r.
индукция по построението на . Нека е константа, = c. Тогава (0) = c = [] (0) []. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме (0) = f* (1 (0), 2 (0), …, l (0)) f* ([1], [2], …, [l]) = []. Използвали сме индукционното предположение и факта, че точното продължение f* на f е монотонна функция. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Ако (0) = , то (0) []. Нека (0) . Тогава (0) = tt и 1 (0) = (0) или (0) = ff и 2 (0) = (0). Нека (0) = tt и 1 (0) = (0). Oт индукционното предположение (0) [] и 1 (0) [1]. Тъй като (0) = tt , то [] = tt [] = [1]. Така (0) = 1 (0) [1] = []. Случаят (0) = ff и 2 (0) = (0) се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (0) = i (1 (0), 2 (0), …, (0)) = []. Главно индукционно предположение: нека (r) [] за някое r 0. Стъпка: ще покажем, че (r+1) [] с индукция по построението на . Нека е константа, = c. Тогава (r+1) = c = [] (r+1) []. Нека е основна операция, = f (1, 2, …, l) и твърдението е изпълнено за термовете 1, 2, …, l. Имаме (r+1) = = f* (1 (r+1), 2 (r+1), …, l (r+1)) f* ([1], [2], …, [l]) = []. Използвали сме индукционното предположение и факта, че точното продължение f* на f е монотонна функция. Нека е условен терм, = if then 1 else 2 и твърдението е изпълнено за термовете , 1, 2. Ако (r+1) = , то (r+1) []. Нека (r+1) . Тогава (r+1) = tt и 1 (r+1) = (r+1) или (r+1) = ff и 2 (r+1) = (r+1). Нека (r+1) = tt и 1 (r+1) = (r+1). Oт индукционното предположение (r+1) [] и 1 (r+1) [1]. Тъй като (r+1) = tt , то [] = tt [] = [1]. Така (r+1) = 1 (r+1) [1] = []. Случаят (r+1) = ff и 2 (r+1) = (r+1) се разглежда абсолютно аналогично. Нека е обръщение към функция, = (1, 2, …, ) и твърдението е изпълнено за термовете 1, 2, …, . Имаме (r+1) = r+1, i (1 (r+1), 2 (r+1), …, (r+1)). От индукционното предположение j (r+1) [j], j = 1, 2, …, ni. Нека j { 1, 2, …, ni}. Ако j (r+1) = aj , то aj = [j] и от предното твърдение R j aj. За всяко j { 1, 2, …, ni} въвеждаме терм j по следния начин: j = aj, ако j (r+1) = aj , j = j, ако j (r+1) = . Ще проверим, че j (r) = j (r+1) за всяко j = 1, 2, …, ni. Действително, ако j (r+1) = aj , то j (r) = aj = j (r+1), ако j (r+1) = , то от r r+1 и от твърдението за монотонност получаваме j (r) = j (r) j (r+1) = j (r) = = j (r+1). Имаме (r+1) = r+1, i (1 (r+1), 2 (r+1), …, (r+1)) = = Гi (r) (1 (r), 2 (r), …, (r)) = i (1 (r), 2 (r), …, (r), r) = = i (X/, F)(r). Използвали сме лемата за съгласуване на заместване и стойност. Вече можем да покажем, че (r+1) []. Ако (r+1) = , то неравенството е очевидно. Нека (r+1) = а . Имаме (r+1) = = i (X/, F)(r) = a . Oт главното индукционно предположение, a = i (X/, F)(r) [i (X/, F)] [i (X/, F)] = a и от предното твърдение, R i (X/, F) a. Разбиваме множеството { 1, 2, …, ni} на две непресичащи се подмножества I1 = { p1, p2, …, pl} и I2 = { q1, q2, …, qs}, по такъв начин, че j I1 j (r+1) , j I2 j (r+1) = . Естествено, от дефиницията на термовете j получаваме, че j I1 j = aj, j I2 j = j, j = 1, 2, …, ni. Нека ( , , …, , F) = i ( / , / , …, / , F) = = i ( / , / , …, / , F). Имаме ( / , / , …, / , F) = = ( / , / , …, / , F) = i (X/, F). Вече получихме R j aj за всяко j I1 = { p1, p2, …, pl}. Също R ( / , / , …, / , F) a. От лемата за симулацията получаваме R ( / , / , …, / , F) a. Oт друга страна, ( / , / , …, / , F) = i (X/, F) R i (X/, F) a. Така [] = a = (r+1).
При това положение, () = ( ) = []. Използвали сме следствието след твърдението за непрекъснатост. Теорема (за пълнота): DN (R) ON (R). Доказателство: нека DN (R)(a) b. Тогава 0 (а, ) = b. От лемата за съгласуване на заместване и стойност, 0 (X/a, F)() = b , от предното твърдение 0 (X/a, F)() [0 (X/a, F)] [0 (X/a, F)] = b. От по-предното твърдение, R 0 (X/а, F) b ON (R)(a) b. Kaто комбинираме теоремите за коректност и пълнота получаваме ON (R) = DN (R), с което показахме еквивалентността на операционната и денотационната семантика с предаване по име на рекурсивните програми. Семантична характеризация на логическите програми. Език от първи ред се състои от следните синтактични елементи:
С всеки функционален и предикатен символ се свързва естествено число, по-голямо от 0, което означава неговата местност (арност). Ще припомним как се дефинират синтактичните понятия терм и формула. Дефинираме индуктивно понятието терм в езика :
Дефинираме индуктивно понятието формула в езика :
Ясно е как се дефинират множествата от свободните и свързаните променливи на формула. Ще считаме, че в една формула не може да има променлива, която е едновременно свързана и свободна. Естествено, това се постига чрез преименуване на свързаните променливи. Ако е терм, то с (X1, X2, …, Xn) означаваме факта, че променливите на са измежду X1, X2, …, Xn. Ако F е формула, то с F (X1, X2, …, Xn) означаваме факта, че свободните променливи на F са измежду X1, X2, …, Xn. Термове, в които не участват променливи наричаме основни. Атомарни формули, в които не участват променливи наричаме основни атоми. Ако (X1, X2, …, Xn), 1, 2, …, n са термове, то с (X1/1, X2/2, …, Xn/n) означаваме термът, получен от чрез едновременно заместване на променливите X1, X2, …, Xn съответно с термовете 1, 2, …, n. По-съкратено записваме (X/). Естествено, ако 1, 2, …, n са основни термове, то (X/) също е основен терм. Ако F (X1, X2, …, Xn) е формула, 1, 2, …, n са термове, то с F (X1/1, X2/2, …, Xn/n) означаваме формулата, получен от F чрез едновременно заместване на свободните срещания на променливите X1, X2, …, Xn съответно с термовете 1, 2, …, n. По-съкратено записваме F (X/). Естествено, ако 1, 2, …, n са основни термове, то формулата F (X/) няма свободни променливи. Алгебрична система в езика се състои от:
Нека е въведена алгебрична система = (H, (a1, a2, …, ar), (F1, F2, …, Fm), (P1, P2, …, Pk)).
Ако v е оценка в , a H и X е променлива, то v[X a] - модификация на v върху X чрез a е оценката, дефинирана с
v () = Fi (v (1), v (2), …, v (n)). Естествено, стойността на всеки терм при дадена оценка v е елемент на носителя H. Също така, стойността на основен терм е една и съща при всяка оценка v. За всяка формула F в и всяка оценка v дефинираме индуктивно стойност true или false на F при оценката v. Бележим, , v F, ако F има стойност true при оценката v и , v F, в противен случай.
Ясно е, че ако две оценки v1, v2 съвпадат върху свободните променливи на F, то , v1 F , v2 F. В частност, ако F няма свободни променливи, то , v F при всяка оценка v или , v F при всяка оценка v. Останалите логически връзки конюнкция, импликация, еквивалентност и кванторът за общност се въвеждат като подходящи съкращения:
формулата (F G). Естествено, , v F & G , v F и , v G.
Естествено, , v F G от , v F следва , v G.
((F G) (G F)). Естествено, , v F G , v F и , v G са едновременно изпълнени или не.
формулата X F. Естествено, , v X F за всяко a H, имаме , v [X a] F. Нека F е формула в , е алгебрична структура в . Казваме, че е модел на F, ако , v F за всяка оценка v. Бележим F. Естествено, ако не е модел на F, бележим F. Нека F, G са формули в . Казваме, че oт F логически следва G и бележим F G, ако при всеки избор на алгебрична система в и оценка на променливите v в имаме , v F , v G. В частност, ако F няма свободни променливи, тaзи дефиниция е еквивалентна на следната: всеки модел на F да е модел и на G. Формула C от вида X1X2…Xs (A (X1, X2, …, Xs) B1 (X1, X2, …, Xs) B2 (X1, X2, …, Xs) … Bn (X1, X2, …, Xs)) се нарича хорнова клауза. Тук A, B1, B2, …, Bn са атомарни формули. Ако n = 0 формулата C наричаме факт, ако n > 0 формулата C наричаме правило. Обикновено за формулата C се използва следният съкратен запис: A :- B1, B2, …, Bn. Логическа програма наричаме формула P от вида C1 & C2 & … & Cp, където Cj е хорнова клауза, j = 1, 2, …, p. Ако P е логическа програма, то с Output (P) бележим множеството от всички основни атоми A, такива че P A. Множеството Output (P) задава семантиката на логическата програма P. Връзката между Output (P) и изчислението в PROLOG е следната:
то А Output (P).
то А Output (P).
Третият случай показва непълнотата на езика PROLOG. При идеална реализация на логическото програмиране в третия случай имаме A Output (P). Този трети случай е съществен и не може да се избегне, тъй като логическото следване в предикатното смятане от първи ред не е алгоритмично разрешимо.
|