| Съдържание |
Пример 1. Нека P е програмата от пример 1 във въпроса „Хорнови програми“, т.е. програмата
| a(o,Y,Y). |
| a(s(X),Y,s(Z)) :- a(X,Y,Z). |
| m(o,Y,o). |
| m(s(X),Y,Z) :- m(X,Y,U), a(U,Y,Z). |
Забележка 1. Можем да онагледим извършеното в горния пример с помощта на следната дървовидна схема:
| Q | ||||||
| ↙ ↘ | ||||||
| Q.1 | Q.2 | |||||
| ↙ | ↘ | |||||
| Q.2.1 | Q.2.2 | |||||
| ↓ | ↓ | |||||
| Q.2.1.4 | Q.2.2.1 | |||||
| ↓ | ↓ | |||||
| Q.2.1.4.3 | Q.2.2.1.4 | |||||
| ↓ | ||||||
| Q.2.2.1.4.4 | ||||||
| ↓ | ||||||
| Q.2.2.1.4.4.3 | ||||||
| ↓ | ||||||
| Q.2.2.1.4.4.3.1 |
Забележка 2. Заключението, че запитването от пример 1 е пропадащо при програмата от този пример, очевидно не зависи от конкретния избор на каноничните резолвенти сред най-общите. Може да се покаже, че подобна независимост е налице винаги, а именно, ако при някой конкретен избор на каноничните резолвенти сред най-общите едно хорново запитване се окаже пропадащо, то ще бъде пропадащо и при всеки друг техен избор.
Забележка 3. При софтуерните реализации на езика Пролог е предвидено изпълнението на хорнова програма върху пропадащо хорново запитване да завършва със съобщение (обикновено то е думата No), показващо, че запитването е пропадащо (по-точно, до такова съобщение се стига при допълнителното условие ресурсите на компютъра да са достатъчни за изследването на всички канонични резолвентни редици относно дадената програма, които започват с даденото запитване).
Забележка 4. От пълнотата на SLD-резолюцията е ясно, че когато едно хорново запитване е пропадащо при дадена хорнова програма, не може да съществува отговор на това запитване при тази програма в смисъла на дефиницията от въпроса „Хорнови програми“. Обратното обаче не е в сила. Например нека p и q са нулместни предикатни символи, а P е хорновата програма
| p :- q. |
| q :- p. |
Знаем, че съществуването на отговор на дадено хорново запитване при дадена хорнова програма не гарантира намирането на такъв отговор при търсенето му съобразно с операционната семантика на Пролог. Ще дадем една математическа характеризация на случаите, когато споменатият вид търсене би дал отговор след някакъв брой стъпки.
Нека P е дадена хорнова програма. На някои хорнови запитвания ще съпоставим число от двуелементното множество {0,1}, като числото, съответно на дадено хорново запитване Q, ще наричаме успех на Q при P или по-кратко успех на Q. Начинът на съпоставянето ще опишем чрез следната индуктивна дефиниция:
1. Празното запитване има успех 1.
2. Ако всички канонични резолвенти на дадено непразно хорново запитване Q с клаузи на P имат успех 0 (в частност, ако Q няма резолвента с никоя клауза на P), то Q има успех 0.
3. Ако всички канонични резолвенти на дадено непразно хорново запитване Q с клаузи на програмата P, предхождащи дадена нейна клауза C, имат успех 0 (в частност, ако Q няма резолвента с никоя клауза на P, предхождаща C), а с C запитването Q има канонична резолвента с успех 1, то
Q има успех 1.
Пример 2. Всички запитвания, за които става дума в пример 1, имат успех 0 при програмата, разглеждана там. И наистина, по точка 2 от горната дефиниция всяко от запитванията Q.1, Q.2.1.4.3 и Q.2.2.1.4.4.3.1 има успех 0. Прилагайки отново същата точка от дефиницията, заключаваме последователно, че такъв успех има също всяко от запитванията Q.2.1.4 и Q.2.1, както и всяко от запитванията Q.2.2.1.4.4.3, Q.2.2.1.4.4, Q.2.2.1.4, Q.2.2.1, Q.2.2. Като използшаме това, че всякп от запитванията Q.2.1 и Q.2.2 има успех 0, пак по точка 2 получаваме, че и запитването Q.2 има успех 0. Имайки по такъв начин информацията, че всяко от запитванията Q.1 и Q.2 има успех 0, заключаваме по същата точка, че и запитването Q има успех 0.
Пример 3. Нека P е същата програма както в пример 1, но Q да е запитването
Забележка 5. Може да се покаже, че ако при даден конкретен избор на каноничните резолвенти сред най-общите едно число се е оказало успех на дадено хорново запитване при дадена хорнова програма, то това положение на нещата ще бъде налице и при всеки друг избор на каноничните резолвенти сред най-общите.
Твърдение 1. Когато едно хорново запитване Q има успех s при дадена хорнова програма P, в сила са следните две условни твърдения:
а) ако s=0, то Q е пропадащо при P;
б) ако s=1, то съществува канонична резолвентна редица относно P, която започва с Q и завършва с празно запитване.
Доказателство. Използваме индукция, съобразена с индуктивната дефиниция за успех, и следните три твърдения, от които първото е тривиално, а останалите две са лесно проверими:
1. Едночленната редица, на която единствен член е празното запитване, е канонична резолвентна редица относно P.
2. Ако всички канонични резолвенти на дадено непразно хорново запитване Q с клаузи на P са пропадащи при P (в частност, ако Q няма резолвента с никоя клауза на P), то Q е пропадащо при P.
3. Ако дадено непразно хорново запитване Q има с някоя клауза на програмата P канонична резолвента, която е начален член на канонична резолвентна редица относно P, завършваща с празно запитване, то съществува канонична резолвентна редица относно P, която започва с Q и завършва с празно запитване. □
От твърдение 1 е ясно, че не може едно хорново запитване да има при дадена хорнова програма едновременно успех 0 и успех 1, но може да се случи то да няма нито успех 0, нито успех 1 (защото може да се случи каноничните резолвентни редици, започващи с даденото запитване, да са безбройно много, но никоя от тях да не завършва с празното запитване.
Твърдение 2. Нека P е произволна хорнова програма. Ако едно хорново запитване е пропадащо при програмата P, то това запитване има при нея успех 0.
Доказателство. Използваме индукция относно максималната измежду дължините на каноничните резолвентни редици относно P, започващи с даденото пропадащо запитване (този брой е поне 1 и запитването не е празно). Ако тази максимална дължина е 1, то запитването няма резолвента с никоя клауза на P и следователно има успех 0 (по точка 2 от дефиницията за успех). Да предположим сега, че при дадено положително цяло число n всяко пропадащо при P хорново запитване, с което не започват канонични резолвентни редици относно P с повече от n члена, има успех 0 при P. Нека Q е такова пропадащо при P хорново запитване, че най-дългата канонична резолвентна редица относно P, започваща с Q, е n+1-членна. Тогава всяка канонична резолвента на Q с клауза на P ще има успех 0 при P, тъй като от такава резолвента не започват канонични резолвентни редици относно P с повече от n члена. При това положение точка 2 от дефиницията за успех позволява да заключим, че и Q има успех 0 при P. □
Следствие. Едно хорново запитване има успех 0 при дадена хорнова програма точно тогава, когато то е пропадащо при нея.
Както видяхме в твърдение 1, ако едно хорново запитване има успех 1 при дадена хорнова програма, то съществува канонична резолвентна редица относно нея, започваща с даденото запитване и завършваща с празното запитване, Обратното не винаги е вярно. При по-прецизно описание на операционната семантика на Пролог, включващо в частност връщанията назад при невъзможност да се продължи дадена резолвентна редица, може да се покаже, че успех 1 при една хорнова програма имат точно онези хорнови запитвания, за които операционната семантика осигурява намирането на отговор при програмата (поне ако се абстрахираме от ограничеността на ресурсите на компютъра). Хорновите запитвания, които имат успех 1 при дадена хорнова програма P, ще наричаме успяващи при P. Всеки конкретен пример, показващ непълнотата на операционната семантика на Пролог относно хорнови програми и хорнови запитвания, може да послужи като пример за хорново запитване, което има отговор при дадена хорнова програма, но не е успяващо при нея.
Последно изменение: 8.05.2008 г.