Previous  Next  Contents
 

 

ПЪЛНОТА НА РЕЗОЛЮЦИЯТА
МЕЖДУ ХОРНОВИ ЦЕЛИ И ХОРНОВИ КЛАУЗИ

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

    Нека P е произволна хорнова програма. Ще казваме, че една хорнова цел Gў е резолвентно достижима въз основа на P от дадена хорнова цел G, ако съществува основана на P крайна резолвентна верига с начален член G и последен член Gў (приемайки тази дефиниция, можем да твърдим въз основа на следствие 2 от предходния въпрос, че винаги, когато P е хорнова програма и празната цел е резолвентно достижима въз основа на P от дадена хорнова цел G, целта G е изпълнима при P). Лесно се съобразява, че така дефинираното отношение на резолвентна достижимост между хорнови цели е рефлексивно и транзитивно. Ще наричаме една атомарна формула A резолвентно отстранима въз основа на P, ако всяка хорнова цел R е резолвентно достижима въз основа на P от съответната цел [A|R]. Така въведените понятия ще ни послужат благодарение на следните две леми.

    Лема 1. Ако всички членове на една хорнова цел G са резолвентно отстраними въз основа на P, то всяка хорнова цел R е резолвентно достижима въз основа на P от съответната цел GR.

    Доказателство. Използваме индукция относно броя на членовете на G.  ї

    Лема 2. Всяка атомарна формула, изводима от P, е резолвентно отстранима въз основа на P.

    Доказателство. Ще използваме индукция, съобразена с дефиницията за изводимост от P. Ако А е атомарната формула от някой частен случай на факт от P, то A е резолвентно отстранима въз основа на P, защото тогава всяка хорнова цел R е резолвента на съответната цел [A|R] с въпросния факт. Нека сега имаме такъв частен случай
        A :- B.
на правило от P, че всички членове на целта B са резолвентно отстраними въз основа на P. Тогава и атомарната формула A е резолвентно отстранима въз основа на P, защото при произволен избор на хорнова цел R целта  [A|R] има резолвента BR със споменатото правило от P, а съгласно лема 1 целта R е резолвентно достижима въз основа на P от целта BR.  ї

    Вече сме готови да докажем това, което казахме в началото.

    Пълнота на резолюцията между хорнови цели и хорнови клаузи. Нека P е произволна хорнова програма, а G е произволна хорнова цел, изпълнима при P. Тогава празната цел е резолвентно достижима от G въз основа на P.

    Доказателство. От синтактичната характеризация на изпълнимите цели посредством изводимост следва, че целта G има частен случай G°, на който всички членове са изводими от P. По лема 2, приложена при R=[], получаваме, че празната цел е резолвентно достижима от G° въз основа на P. Оттук лесно следва желаното заключение. Действително, да разгледаме една основана на P резолвентна верига с начален член G° и последен член празната цел. Ако заменим началния член на тази верига с G, получаваме основана на P резолвентна верига с начален член G и последен член празната цел (това е очевидно, когато веригата, в която правим замяната, е само от един член, защото тогава G°=[] и следователно G=[], а в останалите случаи можем да използваме, че всяка резолвента на G° с клауза от P е резолвента и на G със същата клауза).  ї

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

    Ще усилим чувствително доказания резултат за пълнота, като покажем, че от всяка изпълнима цел може да се стигне до празната цел и посредством един специален вид резолюция. С оглед на дефинирането на този вид резолюция най-напред ще отбележим следното: винаги, когато са дадени една хорнова цел G и една хорнова клауза C, може да се намери такъв вариант C# на C, че G и C# да нямат общи променливи (това е възможно съгласно следствие 1 от въпроса "Варианти и преименуване на променливи", защото множеството на променливите на G е крайно). Ще отбележим още очевидния факт, че когато първият член на една непразна хорнова цел и главата на една хорнова клауза са унифицируеми и s е техен унификатор, то при прилагането на s към тях се получават цел и клауза, които имат непосредствена резолвента.

    Нека са дадени една хорнова цел G и една хорнова клауза C. Нека C# е вариант на C, нямащ общи променливи с G. Една хорнова цел Gў ще наричаме канонична резолвента на G с C, построена с помощта на C#, ако съществува такава субституция s, че s е най-общ унификатор на първия член на G и на главата на C#, а Gў е непосредствената резолвента на s(G) и s(C#) (намирането на канонична резолвента ще наричаме канонична резолюция). Скоро ще покажем, че така дефинираното съотношение между G, C, C# и Gў всъщност не зависи от избора на варианта C# на C. Това ще ни позволи винаги да пропускаме във въведения термин думите "построена с помощта на C#", засега обаче ние ще ги пропускаме само в случая, когато C# съвпада с C (разбира се такъв избор на C# е допустим само тогава, когато G и C нямат общи променливи).

    Пример 1 (ср. с пример 4 от предходния въпрос). Целта [p(f(Y),f(Z)),p(Y,Z)] е канонична резолвента на целта [p(U,U)] с клаузата
        p(X,f(Y)) :- p(X,f(Z)), p(Y,Z).
(получава се, ако в качеството на s се вземе субституцията [f(Y),f(Y)=:U,X]). От своя страна [p(f(Y),f(Z)),p(Y,Z)] има с клаузата
        p(f(f(X)),f(X)).
канонична резолвента [p(f(Z),Z)] (получава се при s=[Z,f(Z)=:X,Y]). Най-сетне, целта [p(f(Z),Z)] има празна канонична резолвента със същата клауза (за получаването й може в качеството на s да се използва кой да е от най-общите унификатори на атомарните формули p(f(Z),Z) и p(f(f(X)),f(X)), но най-прост измежду тях е [f(X)=:Z]).

    Пример 2 (ср. с пример 2 от предходния въпрос). Целта [p(X,b),q(X,Z)] и клаузата
        p(a,X) :- q(X,Z), r(Z).
имат канонична резолвента [q(b,W),r(W),q(a,Z)], построена с помощта на варианта
        p(a,Y) :- q(Y,W), r(W).
на клаузата (в качеството на s е взета субституцията [a,b=:X,Y]).

    Лема за каноничната резолвента. Нека са дадени една хорнова цел G, една хорнова клауза C и един вариант C# на C, нямащ общи променливи с G. Тогава, ако една хорнова цел е канонична резолвента на G с C, построена с помощта на C#, тя е резолвента на G с C. Освен това следните три условия са равносилни:
        а) съществува резолвента на G с C;
        б) първият член на G и главата на C# са унифицируеми;
        в) съществува канонична резолвента на G с C, построена с помощта на C#.

    Доказателство. Ако една хорнова цел Gў е канонична резолвента на G с C, построена с помощта на C#, тя според дефиницията за канонична резолвента е непосредствена резолвента на частен случай на G с частен случай на C# и тъй като C# и C имат едни и същи частни случаи, това гарантира, че Gў е резолвента на G с C. Дефиницията за канонична резолвента осигурява също, че винаги, когато е изпълнено условието б), ще бъде изпълнено и условието в). Разбира се от условието в) следва условието а) според вече доказаното. Остава да се убедим, че от условието а) следва условието б). Това може да се направи по следния начин. Нека G и C имат резолвента. Тогава съществува атомарна формула, която е частен случай както на първия член на G, така и на главата на C. От обстоятелството, че C# е вариант на C, следва, че и главата на C# е вариант на главата на C. Освен това главата на C# няма общи променливи с първия член на G. Тогава според едни разглеждания, които направихме във въпроса "Варианти и преименуване на променливи", може да се твърди, че първият член на G и главата на C# са унифицируеми.  ї

    Забележка за вида на каноничните резолвенти. Нека са дадени една непразна хорнова цел [A|R], където A е атомарна формула и R е хорнова цел, а също една хорнова клауза C и един неин вариант C#, нямащ общи променливи с целта [A|R], като главата и тялото на C# са съответно H и B. Тогава общият вид на каноничните резолвенти на [A|R] с C, построени с помощта на C#, е s(BR), където s е най-общ унификатор на A и H. Това следва от обстоятелството, че когато s е унификатор на A и H, непосредствената резолвента на целта s([A|R]) с клаузата s(C#) е s(B)s(R), която цел съвпада с целта s(BR).

    Ако са дадени една хорнова цел G и една хорнова клауза C, то най-обща резолвента на G с C ще наричаме такава резолвента на G с C, че всяка тяхна резолвента да бъде неин частен случай (да припомним, че в пример 2 от предходния въпрос, намирайки всички резолвенти на целта и клаузата, споменати в пример 2 по-горе, видяхме, че в този случай те се оказват безбройно много, но измежду тях има най-обща). Ще покажем, че винаги, когато една хорнова цел и една хорнова клауза имат резолвента, те имат и най-обща резолвента. Това ще направим чрез следното твърдение, съдържащо основните факти във връзка с най-общи резолвенти и фактически установяващо еквивалентност на понятията канонична резолвента и най-обща резолвента.

    Лема за най-общата резолвента. Нека са дадени една непразна хорнова цел G и две хорнови клаузи C и C#, като C# е вариант на C и няма общи променливи с G. При тези предположения една хорнова цел е най-обща резолвента на G и C точно тогава, когато тя е тяхна канонична резолвента, построена с помощта на варианта C# на C.

    Доказателство. Нека G=[A|R], където A е атомарна формула, а R е хорнова цел, и нека H и B са съответно главата и тялото на клаузата C#. Да предположим най-напред, че една хорнова цел Gў е канонична резолвента на G и C, построена с помощта на варианта C# на C. Според лемата за каноничната резолвента Gў е резолвента на G и C. Ще покажем, че всяка резолвента на G и C е частен случай на Gў. Според забележката за вида на каноничните резолвенти имаме равенството Gў=s(BR), където s е някой най-общ унификатор на A и H. Да разгледаме сега произволна резолвента на G и C. Тя ще бъде резолвента също така на G и C#, защото C е частен случай на C#. Следователно въпросната резолвента ще има вида s2(B)s1(R), където s1 и s2 са такива субституции, че s1(A)=s2(H). Благодарение на това, че G и C# нямат общи променливи, съществува субституция s0, която върху VAR(G) съвпада със s1, а върху VAR(C#) - със s2 (една такава субституция е например онази, която върху VAR(G) съвпада със s1, а върху X \ VAR(G) - със s2). Ясно е тогава, че разглежданата резолвента на G и C може да се напише и във вида s0(B)s0(R), а значи и във вида s0(BR), като освен това имаме равенството s0(A)=s0(H). Понеже s е най-общ унификатор на A и H, от последното равенство следва, че  s0=ds за някоя субституция d. Но тогава ще имаме равенството s0(BR)=d(s(BR)),т.е.s0(BR)=d(Gў) и значи разглежданата произволно избрана резолвента на G и C се оказа частен случай на Gў.  Остана да покажем, че всяка най-обща резолвента на G и C е тяхна канонична резолвента, построена с помощта на C#. Това ще направим като използваме, че при наличието на две най-общи резолвенти на G и C всяка от тях е вариант на другата. Да предположим, че е дадена някоя най-обща резолвента на G и C. Тогава, по лемата за каноничната резолвента, G и C имат канонична резолвента, построена с помощта на C#. Според вече доказаното, тя също е най-обща резолвента на G и C, следователно (по твърдение 2ў от въпроса "Варианти и преименуване на променливи") дадената преди това тяхна най-обща резолвента може да се получи от нея чрез прилагане на някоя преименуваща субституция d. От забележката за вида на каноничните резолвенти знаем, че каноничната резолвента, за която стана дума, ще има вида s(BR), където s е някой най-общ унификатор на A и H. Но тогава разглежданата произволна най-обща резолвента на G и C ще има вида ds(BR), където d е преименуваща субституция. Лесно обаче се вижда, че ds също е най-общ унификатор на A и H, тъй че ds(BR) също е канонична резолвента на G и C, построена с помощта на C# (използваме още веднаж забележката за вида на каноничните резолвенти).  ї

    Следствие 2. Ако G е хорнова цел, C е хорнова клауза и Gў е канонична резолвента на G с C, построена с помощта на един вариант на C, нямащ общи променливи с G, то Gў е канонична резолвента на G с C, построена с помощта на всеки друг вариант на C, нямащ общи променливи с G.

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

    Следствие 3. Ако G е хорнова цел, C е хорнова клауза и Gў е канонична резолвента на G с C, то Gў е канонична резолвента също на кой да е вариант на G с кой да е вариант на C. Освен това всяка канонична резолвента на G с C е вариант на Gў.

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

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

    Пример 3. От пример 1 по-горе е ясно, че резолвентната верига, намерена в пример 4 от предходния въпрос, е канонична резолвентна верига.

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

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

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

G0, G1, ..., Gm-1, Gm
е една такава резолвентна верига. За i=0,1,...,m-1,m дефинираме последователно хорнови цели Gi^, така, че Gi да бъде частен случай на Gi^, да имаме равенството G0^=G и редицата
G0^, G1^, ..., Gm-1^, Gm^
да бъде канонична резолвентна верига, основана на P. Разбира се започваме с това, че полагаме G0^=G (това дава равенството G0^=G0). Да предположим сега, че за някой номер i, по-малък от m, вече сме дефинрали хорнова цел Gi^, така, че Gi да бъде неин частен случай. Целта Gi+1 е резолвента на Gi с някоя клауза C от P (коя е тази клауза ще зависи в общия случай от i). Тогава Gi+1 е резолвента и на Gi^ с C. Съгласно лемата за каноничната резолвента целта Gi^ ще има с клаузата C и канонична резолвента. Полагаме Gi+1^ да бъде някоя канонична резолвента на Gi^ с C. По лемата за най-общата резолвента Gi+1^ ще бъде най-обща резолвента на Gi^ с C. Следователно Gi+1 ще бъде частен случай на Gi+1^. С това дефиницията на обещаната канонична резолвентна верига е завършена. Сега ще се възползваме от обстоятелството, че Gm е празната цел. Тъй като Gm е частен случай на Gm^, ясно е, че Gm^ също е празната цел.  ї

    Следствие 4. Нека P е произволна хорнова програма, а G е произволна хорнова цел. За да бъде целта G изпълнима при P, необходимо и достатъчно е празната цел да е канонично резолвентно достижима от G въз основа на P.

    Забележка относно търсенето на тъждествено изпълнени частни случаи на целите. Kаноничната резолвентна достижимост е специален вид резолвентна достижимост. Поради това можем да използваме каноничната резолвентна достижимост на празната цел от дадена цел G, за да намерим тъждествено изпълнен частен случай на G, действайки така, както беше илюстрирано със забележка 1 от предходния въпрос. При канонична резолвентна достижимост на празната цел, като имаме пред вид използването на най-общи резолвенти, изглежда естествено този метод да дава такъв тъждествено изпълнен частен случай, който е в някакъв смисъл възможно най-общ. Оказва се обаче, че не винаги се получава такъв резултат, ако не се положат известни допълнителни грижи при избора на използваните при каноничната резолюция варианти на клаузите от програмата. Грубо казано, трябва да се грижим, щото вариантът, с който ще си послужим, да няма общи променливи не само с текущата цел, на която ще образуваме канонична резолвента, но и с текущите термове, произлезли от променливите на първоначалната цел (когато се работи не с какви да е най-общи унификатори, а с такива, каквито дават стандартните методи за унификация, това може да се постигне например чрез използване на все нови и нови променливи в образуваните варианти). Ще илюстрираме гореказаното с един пример.

    Пример 4. Нека f и g са едноместни функционални символи, p е двуместен предикатен символ, q е едноместен предикатен символ, а P е следната програма:
        p(f(X),Y).
        q(g(X)).
Да се занимаем с въпроса за изпълнимост при P на следната цел:
        ?- p(U,V), q(V).
Тази цел няма общи променливи с клаузите на P, а първият член на целта и атомарната формула от първата клауза на P имат за най-общ унификатор например субституцията [f(X),Y=:U,V]. Това дава една канонична резолвента на дадената цел с първата клауза на P, а именно следната:
        ?- q(Y).
Така получената цел няма общи променливи с втората клауза на P, а единственият член на целта и атомарната формула от споменатата клауза имат за най-общ унификатор субституцията [g(X)=:Y]. Това показва, че празната цел е канонична резолвента на горната цел с втората клауза на P. Значи редицата

[p(U,V),q(V)], [q(Y)], []
е канонична резолвентна верига, основана на P, и следователно целта, от която тръгнахме, е изпълнима при P. За да намерим частен случай на тази цел, който е тъждествено изпълнен при P, проследяваме как при последователно извършваните субституции се изменят термовете, произлизащи от променливите U и V на въпросната цел. Измененията са показани в следната таблица:
U
 f(X) f(X)
V Y g(X)
Оттук виждаме, че един тъждествено изпълнен при P частен случай на дадената цел може да се получи от нея чрез субституцията [f(X),g(X)=:U,V] - въпросният частен случай е
        ?- p(f(X),g(X)), q(g(X)).
Съществува обаче и по-общ частен случай на целта, който е тъждествено изпълнен при P. За да го намерим, ще променим начина, по който получихме празната цел като канонична резолвента на целта с единствен член q(Y) и на втората клауза от P. А именно, ще си послужим с вариант на въпросната клауза, който да не съдържа не само променливата Y на споменатата цел, но и променливата X, която е налице в произлезлия до този момент от U терм f(X). Да вземем варианта
        q(g(X1)).
Атомарните формули q(Y) и q(g(X1)) имат най-общ унификатор [g(X1)=:Y] и новата таблица за измененията на термовете, произлизащи от U и V, ще бъде следната:
U
 f(X) f(X)
V Y g(X1)
Прилагайки субституцията [f(X),g(X1)=:U,V] към първоначалната цел, получаваме нейния частен случай
        ?- p(f(X),g(X1)), q(g(X1)).
Той е пак тъждествено изпълнен при P, но е по-общ от намерения преди малко. Ще отбележим, че имахме значителна свобода за избиране на вариант на клаузата и на най-общ унификатор още на първата стъпка, която направихме. Ако пък искахме да минем с най-малък брой използвани променливи, можехме, при същата първа стъпка както по-горе, на втората стъпка да използваме вариант на втората клауза на P, в който променливата  е U или V - това би довело до някой от следните два варианта на намерения преди малко частен случай:
        ?- p(f(X),g(U)), q(g(U)).
        ?- p(f(X),g(V)), q(g(V)).
 

Последно изменение: 21.06.2000 г.
 
 Previous  Next  Contents