Пример 1. Нека в дадената сигнатура да има само един функционален символ a и нека той е константа. Нека p е едноместен предикатен символ от сигнатурата и нека P да бъде хорновата програма, състояща се само от факта
           p(a).
Тогава Ербрановият универсум се състои само от константата a и предикатът, който интерпретира символа p в минималния ербранов модел за P, приема стойност 1 за въпросната константа. Поради тази причина атомарната формула p(X) е тъждествено вярна в минималния ербранов модел за P. От друга страна очевидно съществуват други модели за P (например с носител от два елемента), в които атомарната формула p(X) не е тъждествено вярна.

    Разглежданията от предходния въпрос имат още и един, макар и малък недостатък - те изискват предположението, че в дадената сигнатура има поне една константа. Сега ще направим някои подобни разглеждания, които няма да изискват подобно предположение, защото ще се занимаваме с разширени ербранови структури, и, което е по-важно, ще доведат до построяване на такъв модел за коя да е дадена логическа програма, че атомарните формули, тъждествено верни в него, са тъждествено верни и във всеки модел за програмата.

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

    Разбира се, ако P не съдържа нито един факт, то никоя атомарна формула не ще бъде изводима от P. В по-интересните случаи някои атомарни формули ще бъдат изводими от P, а други няма да бъдат.

    Пример 2. Нека единствените функционални символи от сигнатурата са два едноместни функционални символа f и m, а единственият предикатен символ е един двуместен предикатен символа d (интуитивно можем да си представяме, че допустими стойности на променливите са всевъзможните хора, и да четем f(X),m(X),d(X,Y) съответно като "бащата на X", "майката на X", "X е потомък на Y". Нека P е следната хорнова програма (ср. с първите две клаузи на програмата от пример 1 в предходния въпрос):
        d(X,f(X)).
        d(X,m(X)).
        d(X,Z) :- d(f(X),Z).
        d(X,Z) :- d(m(X),Z).
Атомарните формули, изводими от P, могат да бъдат охарактеризирани по следния начин: това са думите от вида d(T,Тў), където T е произволен терм, а Тў е някой от термовете
        f(T), m(T),
        f(f(T)), m(f(T)), f(m(T)), m(m(T)),
        f(f(f(T))), m(f(f(T))), f(m(f(T))), m(m(f(T))), f(f(m(T))), m(f(m(T))), f(m(m(T))), m(m(m(T))),
        . . . . . . . . . . . . . .

    Забележка 1. В Strawberry Prolog при изпълнение на програмата от горния пример върху целта
        ?- d(U,V), write(d(U,V)).
получаваме атомарните формули d(T,Тў), където в качеството на T участва променливата _0, а в качеството на Tў - някой от първите два терма от кой да е от редовете в края на примера (същото пренебрегване на останалите термове от тези редове би се получило и ако в програмата пропуснем последната клауза - тя фактически остава неизползвана при изпълнението на програмата).

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

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

    Доказателство. Да означим с h Ербрановата оценка на променливите. Нека X е произволна променлива от множеството VAR(A). Тъй като S_Pў е разширена ербранова структура, първата основна лема за разширените ербранови структури дава, че стойността на терма s(X) в тази структура при оценката h е равна на самия него и значи е равна на v(X). Това показва, че операторът за присвояване в S_Pў, съответен на s, преобразува оценката h на променливите в такава, която съвпада с v върху множеството VAR(A). Оттук (по необходимото и достатъчно условие за вярност на резултата от прилагане на субституция към атомарна формула и лемата за базисна роля на променливите на една атомарна формула) получаваме, че условието S_Pў,hs(A) е равносилно с условието S_Pў,vA. От друга страна обаче условието S_Pў,hs(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_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_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.

    Уславяме се да казваме, че една хорнова цел е изпълнена тъждествено в дадена структура S, ако тази цел е изпълнена в S при всяка оценка в S на променливите (очевидно това е равносилно с изискването всички членове на целта да са тъждествено верни в S). От направеното доту е ясно, че  за всяка хорнова цел G следните три условия са равносилни помежду си: 1) G е изпълнена тъждествено в S_Pў; 2) всеки член на G е изводим от P; 3) G е изпълнена тъждествено във всеки модел за P. За целите, които са изпълнени тъждествено във всеки модел за P, ще казваме, че са изпълнени тъждествено при 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_Pў, т.е. s(G) е частен случай на G, който е изпълнен тъждествено в S_Pў.  _ї

    Забележка 2. Ако сравним горната теорема с аналогичната теорема от предходния въпрос, виждаме, че условията а) в двете теореми са едни и същи, а останалите едноименни условия се различават. Разбира се, след като са доказани двете теореми, ясно е, че всичките седем различни условия, за които става дума в теоремите, са равносилни помежду си при допълнителното предположение за съществуване на константа, направено в предходния въпрос. Ще отбележим все пак, че при въпросното предположение равносилността на двете условия г) лесно се вижда и директно. Действително от условието г) от предходния въпрос направо следва тукашното условие г), тъй като всяка затворена цел, изпълнима при P, очевидно е изпълнена тъждествено при P. От друга страна, ако е удовлетворено тукашното условие г), то ще съществува частен случай на G, който е изпълнен тъждествено при P, и (прилагайки подходяща субституция към него) можем да си образуваме негов затворен частен случай - той ще бъде затворен частен случай на G, изпълним при P.

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

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

    Забележка 3. Когато с помощта на Strawberry Prolog изпълним една хорнова програма P върху дадена хорнова цел G и получим отговор "Yes", всъщност компютърът ще е намерил субституция, преобразуваща целта G в някой неин частен случай, на който членовете са изводими от G. Ако VAR(G)={X₁,...,X_m}, можем да накараме компютъра да ни даде информация и за тази субституция, като добавим в края на целта G например допълнителния член write([X₁,...,X_m]). Ако да речем P е програмата от пример 2, това би означавало да я изпълним върху целта
        ?- d(U,V), write([U,V]).
(вместо върху целта от забележка 1). При изпълнението ще получаваме последователно (с натискане на клавиш F5 в началото и F8 след това)

[_0,f(_0)]Yes. [_0,m(_0)]Yes. [_0,f(f(_0))]Yes. [_0,m(f(_0))]Yes. [_0,f(f(f(_0)))]Yes. [_0,m(f(f(_0)))]Yes.                           . . .

Съответните субституции разбира се са  [_0,f(_0)=:U,V], [_0,m(_0)=:U,V], [_0,f(f(_0))=:U,V], [_0,m(f(_0))=:U,V] и т.н. (за съжаление Пролог ще пропусне безбройно много други не по-сложни субституции - например няма да се получат субституции от вида  [T,f(m(T))=:U,V], [T,m(m(T))=:U,V] и пр.).

    Забележка 4. При повечето други софтуерни реализации на Пролог сведения за намерената субституция се получават без прибавяне на допълнителни членове към целта. За жалост при немалко от тези други реализации наред с непълнотата, за каквато стана дума в горната забележка, има и случаи, когато при изпълняване на дадена хорнова програма върху дадена хорнова цел се получава положителен отговор и без целта да е изпълнима при програмата (малко повече подробности относно причината за това ще дадем по-нататък) . Например споменатата неприятност може да се срещне при изпълнение на програмата от пример 2 върху целта
        ?- d(X,X).
(въпреки че никой частен случай на атомарната формула d(X,X) не е измежду изводимите от тази програма атомарни формули - те бяха изчерпателно описани в споменатия пример). Да речем Arity Prolog, версия 5.1 (една доста стара реализации на езика), показва в този случай на екрана като резултат следното:

X = f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(f(...)))))))))))  ))))))))))))))))))) ->_

(мигащ курсор накрая подканва ползователя евентуално да запита и за други решения, което става чрез натискане на клавиша за точка и запетая; при първото му натискане се получава подобен резултат, но с "m" вместо с "f", при следващото се повтаря първоначалният резултат, при по-следващото се получава израз, подобен на втория, но с по едно "f(" между последователните "m(" и по-нататък нещата се развиват в този дух, но с увеличаване на броя на вмъкваните "f(", когато не се повтаря първоначалният резултат). Поведението на Strawberry Prolog в случая също не е безупречно, но поне не се получават такива странни решения.
 

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

Previous  Next  Contents