Ако се опитаме да уточним математически кои са целите, за които по подобен начин би могло да се установи, че не са изпълними при дадена програма, стигаме до понятието за цел, пропадаща при тази програма. Всъщност това ще бъде и описание на целите, за които Пролог би дал съобщение "No" при изпълнението на програмата, стига да не бъде възпрепятстван от недостиг на памет или от прекалена продължителност на процеса на изпълнението. За опростяване на дефиницията първо дефинираме едно спомагателно понятие. А именно, ако е дадена една хорнова програма P, то една хорнова цел G ще наричаме директно пропадаща при P, ако G не е празна и няма резолвента с никоя от клаузите на P.

    Пример 2. Ако P е програмата от пример 1, то измежду целите, дадени в явен вид там, директно пропадащи при P са следните: [q(X,X)], [q(a50,a26)], [q(a26,a26v)], [q(a78,a46)], [q(a46,a47)], [q(a64,a65a)], [q(a47,a78)], [q(a81,a78)], [q(a47,a79)] и [q(Z,a26v),q(U,Z)].

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

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

    Пример 3. Всички цели, дадени в явен вид в пример 1, са пропадащи при програната P от въпросния пример. За повечето от тях това се получава с непосредствено прилагане на горната дефиниция и на пример 2. Малко допълнителни разсъждения са нужни само за целите [q(X,a50),q(Y,X),q(Z,Y),q(U,Z)] и [q(Y,a26),q(Z,Y),q(U,Z)]. Разсъжденията биха могли да бъдат следните. За първата от тези две цели е ясно, че всяка нейна канонична резолвента с клауза от P е вариант на втората, а пък за всеки такъв вариант е ясно, че всяка негова канонична резолвента с клауза от P е вариант на директно пропадащата при P цел [q(Z,a26v),q(U,Z)] (използваме следствие 3 от предходния въпрос). Като използваме казаното в забележка 1 по-горе, заключаваме, че всички варианти на целта [q(Z,a26v),q(U,Z)] са пропадащи при P. Оттук и от казаното преди малко получаваме, че и всички варианти на целта [q(Y,a26),q(Z,Y),q(U,Z)] са пропадащи при P. Това пък позволява да заключим, че и целта [q(X,a50),q(Y,X),q(Z,Y),q(U,Z)] е пропадаща при P.

    Дадената преди малко индуктивна дефиниция за хорнова цел, пропадаща при P, може да се трансформира в стандартна математическа дефиниция така: една хорнова цел G се нарича пропадаща при P, ако G принадлежи на всяко множество, състоящо се от хорнови цели и удовлетворяващо условията а) всички хорнови цели, директно пропадащи при P, принадлежат на множеството и б) всеки път, когато една хорнова цел има резолвента с някоя от клаузите на P и всички канонични резолвенти на целта с клаузи на P принадлежат на множеството, самата цел също принадлежи на множеството. Очевидно сечението на всички такива множества е също едно от тях, поради което то всъщност ще бъде точно множеството на пропадащите при P хорнови цели. При такова трансформиране на дефиницията става очевиден следният индуктивен принцип за установяване на общи свойства на пропадащите цели: ако едно свойство е налице както за всички хорнови цели, директно пропадащи при P, тaка и за онези хорнови цели, които имат резолвенти с клаузи на P и всичките им канонични резолвенти с клаузи на P имат това свойство, то въпросното свойство е налице за всички хорнови цели, пропадащи при P.

    Забележка 2. При направеното преди малко трансформиране на дефиницията за хорнова цел, пропадаща при дадена хорнова програма P, стана дума за множества, състоящи се от хорнови цели и удовлетвояващи формулираните две условия а) и б). Ако една цел няма резолвента с никоя клауза на P, то изискването всички канонични резолвенти на тази цел с клаузи от P да принадлежат на разглежданото множество е изпълнено по тривиални съображения. Поради това лесно е да се види, че двете условия а) и б) могат да се заменят с едно, което се получава от б) като вместо думите "има резолвента с някоя от клаузите на P" се поставят думите "не е празна".

    Лема 1. Ако една хорнова цел G е пропадаща при дадена хорнова програма P, то всички варианти на G също са пропадащи при P.

    Доказателство. Ще използваме изказания преди малко индуктивен принцип, като ще го приложим за свойството всичли варианти на разглежданата хорнова цел да са пропадащи при P. От забележка 1 следва, че това свойство е налице за хорновите цели, директно пропадащи при P. Да предположим сега, че G е хорнова цел, която има резолвента с поне една клауза на P и всички канонични резолвенти на G с клаузи на P имат разглежданото свойство. Оттук следва, че всички тези канонични резолвенти са пропадащи при P (защото всяка от тях е вариант на себе си). Ще покажем, че и целта G има разглежданото свойство, т.е. всеки неин вариант е пропадащ при P. И наистина, ако вземем произволен вариант на G, той също ще има резолвента с някоя клауза на P, a според следствие 3 от предходния въпрос каноничните резолвенти на този вариант с клаузите на P ще бъдат същите както на G и значи всички те ще бъдат пропадащи при P, поради което този вариант също ще бъде пропадащ при P.  _ї

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

    Доказателство. Използваме следствие 3 от предходния въпрос.  _ї

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

    Пример 3ў. С помощта на горното следствие могат да се опростят допълнителните разсъждения от пример 3. А именно, вместо да се грижим да показваме, че всички канонични резолвенти на целта [q(Y,a26),q(Z,Y),q(U,Z)] с клаузи от P са пропадащи при P, достатъчно е да направим това само за целта [q(Z,a26v),q(U,Z)], а пък вместо да доказваме. че всички канонични резолвенти на целта [q(X,a50),q(Y,X),q(Z,Y),q(U,Z)] с клаузи от P са пропадащи при P, достатъчно е да направим това само за целта [q(Y,a26),q(Z,Y),q(U,Z)].

    Пример 4. Нека отново P да бъде програмата от пример 1. На схемата по-долу е показано, че е пропадаща при P следната цел:
        ?- q(X,Y), q(Y,U), q(U,V), q(V,X).
Имат се пред вид разсъждения с помощта на следствие 1. За краткост целите са записани без заграждащите ги квадратни скоби. Числата в малките правоъгълничета под даден правоъгълник, съдържащ запис на цел, са номерата на клаузите от P, с които може да се извърши резолюция на въпросната цел, а в правоъгълниците под споменатите малки правоъгълничета са записани съответни канонични резолвенти. Когато под даден правоъгълник, съдържащ запис на цел, няма нито едно малко правоъгълниче с число, това означава, че целта от този правоъгълник няма резолвента с никоя от клаузите на P.
 

    Между пропадане на една цел и нейната изпълнимост имаме връзката, която можеше да се очаква, а именно - че двете неща се изключват взаимно.

    Несъвместимост на пропадането и изпълнимостта. Нека P е произволна хорнова програма. Ако една хорнова цел е пропадаща при P, тази цел не е изпълнима при P.

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

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

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

    Доказателство. Пак ще използваме индуктивния принцип за установяване на общи свойства на пропадащите цели. Дирекно пропадащите при P цели очевидно имат това свойство - основана на P канонична резолвентна верига, започваща с такава цел, не може да има никакъв друг член. От друга страна, ако една хорнова цел G има резолвента с някоя клауза от P и всички канонични резолвенти на G с клаузи на P имат доказваното свойство, то и целта G го притежава, защото, ако от една основана на P канонична резолвентна верига, започваща с G и имаща повече от един член, махнем нейния начален член, получаваме основана на P канонична резолвентна верига, започваща с канонична резолвента на G и на някоя клауза на P.  _ї

    Пример 5. Нека към програмата от пример 1 да добавим още следните две клаузи, където p е двуместен предикатен символ:

p(X,Y) :- q(X,Y).	%   9
p(X,Y) :- p(Y,X).	% 10

Да означим получената по този начин програма с P₁. Целта
        ?- p(X,X).
не е пропадаща при P₁ поради наличието на основаната на P₁ безкрайна канонична резолвентна верига

    Лема 2 допуска следното чувствително усилване:

    Лема 2ў. Нека P е произволна хорнова програма. Ако една хорнова цел е пропадаща при P, то  съществува горна граница за дължините на основаните на P крайни канонични резолвентни вериги, на които тази цел е начален член.

    Доказателство. Отново ще използваме индуктивния принцип за установяване на общи свойства на пропадащите цели. Ако една хорнова цел е директно пропадаща при P, то единствената основана на P канонична резолвентна верига, започваща с дадената цел, е тази, която се състои само от нея, следователно твърдението е вярно в този случай. Сега да предположим, че е дадена една хорнова цел G, която има резолвента с някоя клауза от P и на която всички канонични резолвенти с клаузи от P имат доказваното свойство. Ще покажем, че и тя има това свойство. За целта за всяка клауза от P, с която G има резолвента, да си изберем по една канонична резолвента на G с нея. Нека така избраните канонични резолвенти да бъдат G₁, G₂, ..., G_m. Съгласно направеното предположение за всяка от тях съществува горна граница за дължините на започващите с нея крайни канонични резолвентни вериги, основани на P. Нека h₁, h₂, ..., h_m са такива горни граници. Да означим с h най-голямата от тях. Тогава дължината на коя да е основана на P канонична резолвентна верига, започваща с G, не надминава h+1. Това е очевидно за веригите с единствен член G. От друга страна във всяка от останалите разглеждани вериги членът след началния е вариант на някоя от целите G₁, G₂, ..., G_m. Ако го заменим с нея и махнем началния член на веригата, то ще получим основана на P канонична резолвентна верига, започваща с някоя от въпросните цели и следователно имаща дължина, не по-голяма от h.  _ї

    Ще използваме току-що доказаната лема, за да получим една характеризация на пропадащите цели.

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

    Доказателство. Необходимостта е ясна от горната лема и от несъвместимостта на пропадането и изпълнимостта (лесно е да се даде и директно индуктивно доказателство, че никоя от разглежданите вериги не завършва с празната цел). За да докажем достатъчността, ще си послужим с индукция относно горната граница на дължините на основаните на P крайни канонични резолвентни вериги, на които дадената хорнова цел е начален член. Ако споменатата горна граница е 1, ясно е, че дадената цел няма резолвента с никоя от клаузите на P и не е празна, следователно тя е директно пропадаща, а значи и пропадаща при P. Да предположим сега, че това, което доказваме, е в сила при стойност h на разглежданата граница, където h е дадено естествено число, и да разгледаме цел G, такава, че всички основани на P крайни канонични резолвентни вериги, започващи с G, имат дължини, не по-големи от h+1, а освен това никоя от основаните на P крайни канонични резолвентни вериги, започващи с G, не завършва с празната цел. Ще покажем, че целта G е пропадаща при P. Без ограничение на общността можем да считаме, че поне една от споменатите вериги има дължина h+1. Тогава G сигурно ще има резолвента с поне една от клаузите на P и лесно се съобразява, че ако Gў е канонична резолвента на G с някоя клауза от P, то никоя от основаните на P канонични резолвентни вериги, започващи с Gў, не може да има дължина, по-голяма от h, също, че никоя от тези вериги не може да завършва с празната цел. По индуктивното предположение това гарантира, че всички канонични резолвенти на G с клаузи на P са пропадащи при P, а оттук по дефиницията за пропадаща цел следва, че и целта G е пропадаща.  _ї

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

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

    Пример 6. Нека p и q са нулместни предикатни символи. Да означим с P₁ програмата с единствена клауза
        p :- q, p.
Целта [p] е пропадаща при P₁, защото нейната канонична резолвента с единствената клауза на P₁ е целта [q,p], а тя е директно пропадаща при P₁. Да разглeдаме обаче програмата P₂, която има единствена клауза
        p :- p, q.
При P₂ целта [p] не е пропадаща, защото е начален член на безкрайната канонична резолвентна верига

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

Previous  Next  Contents