Програма на Пролог за една универсална просто изчислима функция

    Ще разгледаме един случай, в който множеството B се състои от затворени термове, допустими за Пролог, като множеството B* ще бъде реализирано също чрез изрази, допустими за Пролог. Нека B={a, s(a), s(s(a)), s(s(s(a))),  . . . }, а B* е най-малкото множество от изрази, което съдържа множеството B∪{o} и заедно със всеки два свои елемента E1 и E2 съдържа още и израза [E1,E2] (изразите от последния вид ще наричаме наредени двойки в Пролог или за краткост двойки). Като първични просто изчислими функции ще вземем функцията ν в B, преобразуваща всеки терм T от B в съответния терм s(Т), нейната обратна функция, която ще означим с π, и функцията ζ от B към B*, преобразуваща терма a в двойката [o,o], а всички останали термове от B - в елемента o. Ще използваме кодирането от преди това направените общи разглеждания, като използваната при тях редица α0, α1, α2, . . . , αs в случая ще изберем, полагайки s=6, α0=I, α1=L, α2=R, α3=D, α4=ν, α5=π, α6=ζ.

    Нека P е следната програма на Пролог:

e(X,c(Y),Y).
e(X,i,X).
e([X1,X2],l,X1).
e([X1,X2],r,X2).
e(a,d,[o,o]).
e(s(X),d,[o,o]).
e(o,d,o).
e(a,n,s(a)).
e(s(X),n,s(s(X))).
e(s(X),p,X).
e(a,z,[o,o]).
e(s(X),z,o).
e(X,cp(A,B),Y) :–  e(X,A,U),  e(U,B,Y).
e(X,cb(A,B),[Y,Z]) :–  e(X,A,Y),  e(X,B,Z).
e(X,br(A,B,C),Y) :–  e(X,A,U),  e1(U,X,B,C,Y).
e(X,it(A,B),Y) :–  e(X,br(A,cp(B,it(A,B)),i),Y).
e1([U1,U2],X,B,C,Y) :–  e(X,B,Y).
e1(a,X,B,C,Y) :–  e(X,C,Y).
e1(s(Z),X,B,C,Y) :–  e(X,C,Y).
e1(o,X,B,C,Y) :–  e(X,C,Y).     Да означим с H най-малкото множество от изрази, което съдържа множеството {a, o}, заедно със всеки свой елемент E съдържа и израза s(E), а заедно със всеки два свои елемента E1 и E2 съдържа още и израза [E1,E2]. Нека H′ е ербрановият универсум за програмата P (образуването на израз от вида [E1,E2] го третираме като образуване на съставен терм с помощта на някакъв подразбиращ се двуместен функционален символ). Очевидно B* е същинско подмножество на множеството H, което пък от своя страна е същинско подмножество на H′. Сега ще дефинираме една структура S с носител множеството H, която е модел за P. Като интерпретация в S на константите a и o, на едноместния функционален символ s и на споменатия по-горе подразбиращ се двуместен функционален символ вземаме тяхната ербранова интерпретация при носител H на структурата - това ще осигури, че стойността в S на всеки израз от H е равна на самия него. На останалите функционални символи (вкл. константи), участващи в P, ще дадем интерпретация в S както следва (приемайки, че 0=o и k+1=[o,k] за k=0,1,2,3,4,5): cS(E)=[0,E],
iS=[1,0], lS=[1,1], rS=[1,2], dS=[1,3], nS=[1,4], pS=[1,5], zS=[1,6],
cpS(E1,E2)=[2,[E1,E2],
cbS(E1,E2)=[3,[E1,E2],
brS(E0,E1,E2)=[4,[E0,[E1,E2]],
itS(E1,E2)=[5,[E1,E2]. Така дадената интерпретация на гореспоменатите функционални символи осигурява, че за всеки елемент E на B* елементът cS(E) е код на навсякъде дефинираната константна функция със стойност E, че iS, lS, rS, dS, nS, pS, zS са кодове съответно на функциите I, L, R, D, ν, π, ζ, че всеки път, когато K1 и K2 са кодове на дадени частични функции в B*, елементите cpS(K1,K2), cbS(K1,K2), itS(K1,K2) са кодове съответно на композицията и съчетанието на тези функции и на итерацията на втората от тях, управлявана от първата, и че всеки път, когато K0, K1 и K2 са кодове на дадени частични функции в B*, елементът brS(K0,K1,K2) е код на разклонението към функциите с кодове K1 и K2, управлявано от функцията с код K0. Интерпретация на предикатния синвол e даваме, като приемаме, че eS(E1,E2,E3)=1 за дадена тройка E1, E2, E3 от елементи на H точно тогава, когато за нея е вярна следната импликация: ako E1∈B*, а E2 е код на някоя частична функция в B*, то нейното прилагане към E1 дава резултат E3. Най-сетне, приемаме, че e1S(E1,E2,E3,E4,E5)=1 за дадена петорка E1, E2, E3, E4, E5 от елементи на H точно тогава, когато за нея е вярна следната импликация: ako E1 и E2 принадлежат на B*, а E3 и E4 са кодове на някои две частични функции в B*, то е в сила едно от двете: а) E1 е двойка и прилагането на функцията с код E3 към E2 дава резултат E5 или б) E1 не е двойка и прилагането на функцията с код E4 към E2 дава резултат E5.     Определен вид изрази ще наречем формални кодове. Дефиницията е индуктивна: за всеки израз E от B* изразът c(E) е формален код, константите i, l, r, d, n, p, z също са формални кодове, за всеки два формални кода C1 и C2 изразите cp(C1,C2), cb(C1,C2), it(C1,C2) също са формални кодове, за всеки три формални кода C0, C1 и C2 изразът br(C0,C1,C2) също е формален код. Ясно е, че стойността в S на всеки формален код е код на някоя частична функция в B* и че всеки елемент на B*, който е код на частична функция в B*, представлява стойност в S на точно един формален код. Когато C е формален код, ние ще означаваме с fC частичната функция в B* с код CS. Ясно е, че за всеки елемент E на B* fc(E) е навсякъде дефинираната константна функция със стойност E, че fi, fl, fr, fd, fn, fp, fz са съответно функциите I, L, R, D, ν, π, ζ, че за всеки два формални кода C1 и C2 функциите fcp(C1,C2), fcb(C1,C2) и fit(C1,C2) са съответно композицията на функциите fC1 и fC2, тяхното съчетание и итерацията на fC2, управлявана от fC1, и че за всеки три формални кода C0, C1 и C2 функцията fbr(C0,C1,C2) е разклонението към функциите fC1 и fC2, управлявано от fC0.

    Твърдение за коректност на програмата P. Нека E е елемент на B*, C е формален код, а G е целта

?-  e(E,C,Y). Нека целта G успява при програмата P. Тогава E принадлежи на дефиниционната област на функцията fC, съществува единствен частен случай на формулата e(E,C,Y), който е тъждествено верен във всички модели за P, и той може да се получи чрез субституцията [Y/E′], където E′ е резултатът от прилагането към E на функцията fC.

    Доказателство. Щом целта G успява при програмата P, формулата e(E,C,Y), има частен случай e(E,C,E′), който е тъждествено верен във всички модели за P. Да означим с S′ структурата с носител H′, в която интерпретацията на всички функционални символи, участващи в P, е ербранова, а интерпретацията на двата предикатни символа e и e1 се определя по следния начин: предикатът eS′ приема стойност 1 точно за онези тройки от елементи на H′, за които е вярна импликацията

ако първият член на тройката принадлежи на B*, а вторият е формален код, то третият принадлежи на B*; предикатът e1S′ приема стойност 1 точно за онези петорки от елементи на H′, за които е вярна импликацията ако първите два члена на петорката принадлежат на B*, а следващите два са формални кодове, то последният принадлежи на B*. Така дефинираната структура S′ е модел за програмата P, следователно формулата e(E,C,E′) е тъждествено вярна в S′, а значи затворените частни случаи на тази формула са верни в S′. Тъй като всеки от изразите E и C, а също всеки затворен частен случай на израза E′ съвпада със стойността си в S′, това показва, че затворените частни случаи на E′ принадлежат на множеството B*. Разбира се затворените частни случаи на формулата e(E,C,E′) са верни и в структурата S и това заедно с току-що казаното позволява да твърдим, че частичната функция в B* с код CS е дефинирана за елемента E на B* и стойността й за него представлява единственият затворен частен случай на E′. Очевидно последното е възможно само ако въпросната стойност е равна на самия израз E′.

    Твърдение за пълнота на програмата P. Нека C е формален код, E е елемент на дефиниционната област на функцията fC и G е целта

?-  e(E,C,Y). Тогава G успява при програмата P.

    Доказателство. С индукция относно построението на формалния код C се показва, че при направените предположения във всеки модел за P е вярна затворената формула e(E,C,E′), където E′ е резултатът от прилагането към E на функцията fC. Ще разгледаме само най-сложната част от разсъжденията - доказателството, че ако два формални кода C1 u C2 имат разглежданото свойство, то формалният код it(C1,C2) също притежава разглежданото свойство. И така, нека формалните кодове C1 u C2 имат разглежданото свойство, а функцита fit(C1,C2) дава резултат E′ при прилагане към един елемент E от нейната дефиниционна област. Това позволява да твърдим, че за някоя крайна редица E0, E1, E2, . . . , En от елементи на B* са изпълнени равенствата E0=E и En=E′, като при k=0,1,2,...,n-1 прилагането на функциите fC1 и fC2 към елемента Ek дава съответно резултат Ek, който е двойка, и резултат Ek+1, а прилагането на първата от тези две функции към елемента En дава резултат En, който не е двойка. Като използваме направеното предположение за формалните кодове C1 u C2, заключаваме, че във всеки модел за P са верни формулите e(Ek,C1,Ek), k=0,1,2,...,n, и формулите e(Ek,C2,Ek+1), k=0,1,2,...,n-1. Трябва да покажем, че във всеки модел за P е вярна и формулата e(E,it(C1,C2),E′). Това ще направим като чрез индукция отгоре надолу покажем, че при k=0,1,2,...,n формулата e(Ek,it(C1,C2),E′) е вярна във всеки модел за P. Имайки пред вид обстоятелството, че клаузата от P, съдържаща функционалния символ it, е тъждествено вярна във всеки модел за P, за да покажем, че за дадено k горната формула е вярна във всеки модел за P, достатъчно е да направим това за формулата
        e(Ek,br(C1,cp(C2,it(C1,C2)),i),E′).
Но и клаузата от P, съдържаща функционалния символ br в заключението си, също е тъждествено вярна във всеки модел за P. Поради това и поради тъждествената вярност във всеки модел за P на формулата e(Ek,C1,Ek) достатъчно е да покажем същото и за формулата
        e1(Ek,Ek,cp(C2,it(C1,C2)),i,E′).
При k=n тази формула е частен случай на заключението на някоя от последните три клаузи на P, тъй че в този случай е достаъчно да се убедим, че във всеки модел за P е вярна формулата
        e(Ek,i,E′),
а това е така, защото тя пък е частен случай на формулата от клаузата, съдържаща константата i. Да предположим сега, че k<n и формулата e(Ek+1,it(C1,C2),E′) е вярна във всеки модел за P. Ще покажем, че в такъв случай и формулата e(Ek,it(C1,C2),E′) е вярна във всеки модел за P. Това ще го извършим отново, като направим същото за написаната преди малко формула с предикатен символ e1. Този път обаче тя е частен случай на заключението на първата от последните четири клаузи nа P и поради това е достатъчно да установим, че във всеки модел за P е вярна формулата
        e(Ek,cp(C2,it(C1,C2)),E′).
Последното обаче следва от факта, че клаузата, съдържаща в заключението си функционалния символ cp, е тъждествено вярна във всички модели за P, и от обстоятелството, че в тях са верни формулите e(Ek,C2,Ek+1) и  e(Ek+1,it(C1,C2),E′).
    Щом формулата от целта G има затворен частен случай, който е верен във всички модели за P, можем да сме сигурни, че в дървото на търсене за G при P има път, който води до успех. Този път е достижим при обичйната операционна семантика на Пролог, защото споменатото дърво всъщност е линейно, т.е. от кой да е негов връх излиза най-много едно ребро. За да се убедим в това, най-напред отбелязваме, че ако в първата формула на дадена цел всички аргументи без последния са затворени изрази, то целта има резолвента най-много с една клауза на P. Оттук следва споменатата линейност, като се докаже по индукция, че при стандартното извършване на резолюция с клаузи на P може от целта G да се стигне само до такива цели, които удовлетворяват следните условия:

    1. Последните аргументи на членовете на целта са две по две различни променливи.
    2. Всяка променлива, която участва в първи аргумент на някой член на целта, представлява последен аргумент на някой предходен неин член.
    3. Аргументите без първия и последния на всеки член на целта са затворени изрази.     Забележка. Може да се случи някой пръв аргумент на член на цел, получена по току-що разглеждания начин, да съдържа повече от една променлива. Нека например G е целта ?-  e(s(a),br(cb(n,p),z,d),Y). Тогава от G се достига до празната цел, като се минава последователно през следните цели (с точност до преименуване на променливите): ?-  e(s(a),cb(n,p),U),  e1(U,s(a),z,d,Y).
?-  e(s(a),n,U1),  e(s(a),p,U2),  e1([U1,U2],s(a),z,d,Y).
?-  e(s(a),p,U2),  e1([s(s(a)),U2],s(a),z,d,Y).
?-  e1([s(s(a)),a],s(a),z,d,Y).
?-  e(s(a),z,Y). Виждаме, че третият член на втората от тези цели съдържа двете различни променливи U1 и U2.

Последно изменение на съдържанието: 11.06.2002 г. На 29.04.2020 г. елиминирано използването на шрифт Symbol.