Нека P е една хорнова програма. Някои атомарни формули ще наречем затворено изводими от P. Дефиницията е индуктивна и се състои от следните две точки:
        а) винаги, когато клаузата
           A°.
е затворен частен случай на факт от P, атомарната формула A° е затворено изводима от P;
        б) винаги, когато клаузата
           A°:- B₁°, B₂°, ..., B_m°.
е затворен частен случай на правило от P и всяка от атомарните формули B₁°, B₂°,...,B_m° е затворено изводима от P, атомарната формула A° също е затворено изводима от P.

    От горната дефиниция следва веднага, че всички атомарни формули, затворено изводими от P, са затворени. Обратното в общия случай не е вярно. Например, ако P не съдържа нито един факт, то никоя атомарна формула не ще бъде затворено изводима от P. Могат разбира се да се дадат и по-интересни примери за хорнови програми, от които са затворено изводими не всички затворени атомарни формули.

    Пример 1. Нека единствените функционални символи от сигнатурата са седем константи c1, c2, c3, c4, c5, c6, c7, а единствените предикатни символи са два двуместни предикатни символа d и p. Нека P е следната хорнова програма, съответстваща на пример 2 от встъпителните бележки:
        d(X,Y) :- p(Y,X).
        d(X,Z) :- p(Y,X), d(Y,Z).
        p(c1,c3).
        p(c2,c5).
        p(c3,c5).
        p(c4,c6).
        p(c5,c7).
В този случай всички възможни затворени атомарни формули са краен брой (49 с предикатен символ d и 49 с предикатен символ p). Ще намерим кои измежду тях са затворено изводимите от P. Очевидно атомарните формули в петте факта на P са единствените атомарни формули, за които точка а) от дефиницията дава, че са затворено изводими от P. Те са и единствените атомарни формули с предикатен символ p, които са затворено изводими от P, тъй като по точка б) от дефиницията би могло да се установява, че са затворено изводими от P, само за атомарни формули с предикатен символ d. Тогава единствените затворени частни случаи на първата клауза от програмата, в които атомарната формула от тялото е затворено изводима от P, са следните:
        d(c3,c1) :- p(c1,c3).
        d(c5,c2) :- p(c2,c5).
        d(c5,c3) :- p(c3,c5).
        d(c6,c4) :- p(c4,c6).
        d(c7,c5) :- p(c5,c7).
Освен това затворените частни случаи на втората клауза от програмата, в които двете атомарни формули от тялото са затворено изводими от P, могат да бъдат само от следващите пет вида, където T е някоя от седемте константи:
        d(c3,T) :- p(c1,c3), d(c1,T).
        d(c5,T) :- p(c2,c5), d(c2,T).
        d(c5,T) :- p(c3,c5), d(c3,T).
        d(c6,T) :- p(c4,c6), d(c4,T).
        d(c7,T) :- p(c5,c7), d(c5,T).
Като вземем пред вид първите пет от изброените частни случаи и използваме точка б) от дефиницията, установяваме, че са затворено изводими атомарните формули d(c3,c1), d(c5,c2),d(c5,c3),d(c6,c4),d(c7,c5). Като използваме това и избираме по подходящ начин константата T, спомената преди малко, пак по точка б) от дефиницията получаваме, че са затворено изводими от P още и атомарните формули d(c5,c1),d(c7,c2),d(c7,c3). Оттук, работейки по същия начин, виждаме, че е затворено изводима от P и атомарната формула d(c7,c1). С това се изчерпват всички атомарни формули, затворено изводими от P.

    Забележка 1. Атомарните формули, затворено изводими от програмата P от горния пример, биха могли да бъдат намерени и с помощта на компютър. Това можем да направим като, грубо казано, изпълним програмата поотделно върху двете цели
        ?- p(U,V).
        ?- d(U,V).
с намиране на всички резултати. Например при използване на Strawberry Prolog би могло да се осигури показване на резултатите чрез добавяне на втори член write(p(U,V)) в първата от двете цели и на втори член write(d(U,V)) във втората (намирането на първия от резултатите при изпълнението на P върху дадена от целите може да стане чрез еднократно натискане на клавиша F5, а на останалите резултати - чрез натискане след това на клавиша F8 до получаване на съобщение "No.").

    Забележка 2. Не трябва да се мисли, че при всяка хорнова програма положението ще бъде напълно аналогично на описаното в пример 1 и забележка 1. Например има случаи, когато затворено изводимите от дадена хорнова програма атомарни формули са безбройно много (вж. пример 2 по-долу). Освен това при търсенето на затворено изводимите атомарни формули по начин, подобен на горния, Пролог може да даде резултати, които съдържат променливи и тези променливи трябва допълнително да се заместват със затворени термове, за да се получават затворено изводимите атомарни формули (вж. пример 3 по-долу). Най-сетне има и хорнови програми (вж. пример 4 по-долу), при които някои затворено изводими атомарни формули не биха могли да се получат дори и по такъв начин (това се дължи на непълнотата на търсенето при реализациите на Пролог, допусната за постигане на по-голяма ефективност).

    Пример 2. Нека единствените функционални символи от сигнатурата са константата a и едноместният функционален символ f, а единственият предикатен символ - едноместният предикатен символp. Нека P е следната хорнова програма:
        p(a).
        p(f(f(X))) :- p(X).
Тогава затворено изводими от P са точно онези атомарни формули, които са от вида p(f(...f(a)...)) с четен (евентуално нулев) брой участия на символа f. При изпълнение на тази програма чрез Strawberry Prolog върху целта
        ?- p(U), write(p(U)).
еднократното натискане на клавиша F5 ще покаже атомарната формула p(a), а натискането след това на клавиша F8 ще показва последователно атомарните формули p(f(f(a))), p(f(f(f(f(a))))) и т.н. без някога да се получи съобщение "No.".

    Пример 3. Нека пак единствените функционални символи от сигнатурата са константата a и едноместният функционален символ f, но единствен предикатен символ да бъде двуместният предикатен символ p. Нека P е следната хорнова програма:
        p(X,a).
        p(f(X),f(Y)) :- p(X,Y).
Да се условим за произволен терм T да означаваме с f⁰(T),f¹(T),f²(T) и т.н. съответно термовете T, f(T),f(f(T)) и пр. Тогава атомарните формули, които са затворено изводими от P, могат да бъдат охарактеризирани по следния начин: те са атомарните формули от вида p(f^m(a),fⁿ(a)), където m и n са неотрицателни цели числа, удовлетворяващи неравенството mіn. Резултатите пък от изпълнението на тази програма чрез Strawberry Prolog върху целта
        ?- p(U,V), write(p(U,V)).
са атомарни формули от вида p(fⁿ(X),fⁿ(a)), където X е променлива, започваща със знак за подчертаване, а n е неотрицателно цяло число.

    Пример 4. При същата сигнатура както в пример 2 нека P е програмата
        p(a).
        p(f(f(X))) :- p(X).
        p(f(f(f(X)))) :- p(X).
Описание на затворено изводимите от P атомарни формули можем да получим, като използваме лесно доказуемото твърдение, че всяко цяло число, по-голямо от 1, допуска представяне във вида 2k+3l, където k и l са неотрицателни цели числа. С помощта на това твърдение можем да се убедим, че въпросните атомарни формули са точно онези, които са от вида p(f(...f(a)...)) с различен от 1 (евентуално нулев) брой участия на символа f. При изпълнение на тази програма върху целта
        ?- p(U), write(p(U)).
Strawberry Prolog (както и другите реализации на Пролог) дава обаче само онези атомарни формули от горния вид, в които f участва четен брой пъти (третата клауза от програмата просто остава неизползвана).

    Да се върнем отново към общия случай, когато P е произволна хорнова програма. От втората основна лема за ербрановите структури следва съществуване на точно една ербранова структура със свойството, че в нея са верни онези и само онези затворени атомарни формули, които са затворено изводими от P. Ербрановата структура с това свойство ще наричаме ербранова структура, породена от P, и ще я означаваме с S_P. Ще установим някои други нейни свойства, като за целта най-напред ще докажем едно помощно твърдение. В него ще става дума както за оценки в S_P на променливите, така и за субституции. Във връзка с това отбелязваме, че и оценките в S_P, и субституциите са изображения на множеството на променливите в множеството на термовете, но никоя оценка в S_P не е субституция, понеже, преобразувайки всички променливи в затворени термове, тя не може да преобразува никоя променлива в себе си, докато една субституция преобразува в себе си всички променливи с изключение най-много на краен брой. От друга страна обаче върху кое да е крайно множество от променливи всяка оценка в S_P съвпада с някоя субституция и всяка субституция съвпада с някоя оценка в S_P.

    Лема за свеждане на оценките в породената ербранова структура към субституции. Нека A е дадена атомарна формула, v е някоя оценка в S_P на променливите и s е такава субституция, че s(X)=v(X) за всяка променлива X от множеството VAR(A). Тогава атомарната формула s(A) е затворена, а условието S_P,vA е равносилно с това s(A) да е затворено изводима от P.

    Доказателство. Тъй като всички стойности на v принадлежат на носителя H на S_P, субституцията s преобразува всички променливи от множеството VAR(A) в елементи на H, т.е. в затворени термове. Това, както знаем, е достатъчно, за да можем да твърдим, че формулата s(A) е затворена. Нека сега X е произволна променлива от множеството VAR(A). Тъй като S_P е ербранова структура, първата основна лема за ербрановите структури дава, че стойността на затворения терм s(X) в тази структура е равна на самия него и значи е равна на v(X). Това показва, че операторът за присвояване в S_P, съответен на s, преобразува всяка оценка в S_P на променливите в такава, която съвпада с v върху множеството VAR(A). Оттук (по необходимото и достатъчно условие за вярност на резултата от прилагане на субституция към атомарна формула и лемата за базисна роля на променливите на една атомарна формула) получаваме, че условието S_Ps(A) е равносилно с условието S_P,vA. От друга страна обаче S_Ps(A) е равносилно и с това s(A) да е затворено изводима от P.  _ї

    Сега ще докажем едно много съществено твърдение за ербрановата структура, породена от P.

    Теорема за минималния ербранов модел. Структурата S_P е модел за P и при всеки избор на затворената атомарна формула A следните три условия са равносилни помежду си: 1) A е вярна в S_P; 2) A е затворено изводима от P; 3) A е вярна във всеки модел за P.

    Доказателство. За да докажем, че S_P е модел за P, да разгледаме произволна клауза C от P. Ще покажем, че C е тъждествено вярна в структурата S_P. Да разгледаме първо случая, когато C е някой факт
           A.
Нека v е произволна оценка в S_P на променливите. Разглеждаме такава субституция s, че s(X)=v(X) за всяка променлива X от VAR(A) (субституция с това свойство съществува, понеже множеството VAR(A) е крайно). По лемата за свеждане на оценките в породената ербранова структура към субституции може да се твърди, че атомарната формула s(A) е затворена, а условието S_P,vA е равносилно с това s(A) да е затворено изводима от P. Последното обаче е изпълнено благодарение на точка а) от дефиницията за атомарна формула, затворено изводима от P, защото s(A) е затворен частен случай на A. Следователно изпълнено е и условието S_P,vA. С това показахме, че ако клаузата C е факт, тя е тъждествено вярна в S_P. Сега ще се занимаем със случая, когато C е някое правило
           A :- B₁, B₂, ..., B_m.
Нека v е оценка в S_P на променливите, при която в S_P е изпълнено тялото на C, т.е. S_P,vB_i при i=1,2,...,m. Разглеждаме такава субституция s, че s(X)=v(X) за всяка променлива X от VAR(C) (субституция с това свойство съществува, понеже множеството VAR(C) е крайно). По лемата за свеждане на оценките в породената ербранова структура към субституции може да се твърди, че при i=1,2,...,m атомарната формула s(B_i) е затворена и е затворено изводима от P, а също, че   атомарната формула s(A) е затворена и условието S_P,vA е равносилно с това s(A) да е затворено изводима от P. Да разгледаме сега клаузата s(C), т.е. клаузата
           s(A):- s(B₁),s(B₂), ...,s(B_m).
От казаното преди малко е ясно, че тя е затворен частен случай на C и всички членове на нейното тяло са затворено изводими от P. При това положение точка б) от дефиницията за атомарна формула, затворено изводима от P, позволява да заключим, че и главата s(A) на C е затворено изводима от P, следователно S_P,vA. И така, клаузата C и този път се оказа тъждествено вярна в S_P. И така, доказахме, че структурата S_P е модел за P. Остана да покажем, че за всяка затворена атомарна формула A условията 1), 2) и 3) са равносилни помежду си. Това ще направим, като покажем, че са налице съотношенията

    Теоремата, която току-що доказахме, показва, че измежду всички модели за хорновата програма P ербрановата структура, породена от P, има най-малко множество на верните затворени атомарни формули. По тази причина тази структура обикновено се нарича минимален ербранов модел за P.

    Забележка 3. Носител на всяка ербранова структура е Ербрановият универсум,  а той се определя еднозначно по дадената сигнатура. За улеснение на формулировките ние сме приели, че е избрана някаква сигнатура и всички хорнови програми и цели, които разглеждаме, са построени с използване на символите от тази сигнатура. При прилагането на нещата в конкретни случаи можем обаче да постъпваме и по следния начин: когато е дадена една конкретна хорнова програма, да разглеждаме подходяща сигнатура само с краен брой функционални и предикатни символи, избрани така, че измежду тях да бъдат всички използвани в програмата, и след това на основата на тази сигнатура да строим минимален ербранов модел за тази програма.

    Нещата, които установихме, позволяват да се направят някои важни изводи и относно хорновите цели, изпълними при дадена хорнова програма. Първият от тях е непосредствено ясен от направеното дотук и гласи, че за всяка затворена хорнова цел G следните три условия са равносилни помежду си: 1) G е изпълнена в S_P; 2) всеки член на G е затворено изводим от P; 3) G е изпълнена във всеки модел за P. Преминаваме към следващия.

    Теорема за характеризация на изпълнимите цели с помощта на минималния ербранов модел. Нека G е дадена хорнова цел. Тогава следните четири условия са равносилни помежду си: а) G е изпълнима при P; б) G е изпълнима в S_P; в) някой затворен частен случай на G е изпълнен в S_P; г) някой затворен частен случай на G е изпълним при P.

    Доказателство. Това, че от условието а) следва условието б), е ясно - ако G е изпълнима при P, то G е изпълнима във всеки модел за P, а S_P е един от тези модели. Като използваме, че затворените цели, изпълнени в S_P, са изпълнени във всеки модел за P, виждаме също, че от условието в) следва условието г). Ясно е и това, че от условието г) следва условието а) - ако някой частен случай на G е изпълним при P, той е изпълним във всеки модел за P, а тогава и целта G ще бъде изпълнима във всеки модел за P (по твърдението за изпълнимост на цел, имаща изпълним частен случай). При това положение е достатъчно да покажем, че от условието б) следва условието в). Да предположим, че G е изпълнима в S_P. Това означава, че G е изпълнена в S_P при някоя оценка в S_P на променливите. Нека v е една такава оценка. Да означим със s такава субституция, че за всяка променлива X от множеството VAR(G) да е в сила равенството s(X)=v(X). Като приложим лемата за свеждане на оценки в породената ербранова структура към субституции, получаваме, че за всеки член A на G атомарната формула s(A) е затворена и е затворено изводима от P. Следователно целта s(G) е затворена и всички нейни членове са верни в S_P, т.е. тя е изпълнена в S_P.  _ї

    Четирите равносилни помежду си условия а) - г) в горната теорема са формулирани с помощта на семантични термини като "изпълнима", "изпълнен", "изпълним". Условието в) обаче е равносилно със синтактично формулираното изискване да съществува  частен случай на G, на който всички членове са затворено изводими от P. Следователно е в сила следното твърдение:

    Синтактична характеризация на изпълнимите цели посредством затворена изводимост. За да бъде една хорнова цел G изпълнима при дадена хорнова програма P, необходимо и достатъчно е да съществува частен случай на G, на който всички членове са затворено изводими от P.

    Да припомним все пак, че в горното твърдение, както и навсякъде другаде в този въпрос, предполагаме съществуване на поне един нулместен предикатен символ в сигнатурата, която е дадена.
 

Последно изменение: 10.06.2003 г.
 

Previous  Next  Contents