Нека A и B са две атомарни формули или два терма. Унификатор на A и B ще наричаме всяка субституция, която преобразува A и B в една и съща дума. Ще казваме, че A и B са унифицируеми, ако те имат поне един унификатор.

    Пример 1. Нека A=p(a,Y),B=p(X,b), където p е двуместен предикатен символ, a и b са константи, X и Y са променливи. Тогава субституцията [a,b=:X,Y] е унификатор на атомарните формули A и B, защото преобразува и двете в атомарната формула p(a,b). Унификатори на A и B са и всички други субституции, които съвпадат с посочената върху променливите X и Y.

    Пример 2. Да направим малко изменение в пример 1, като в качеството на A вземем атомарната формула p(a,X) вместо p(a,Y). Тогава A и B се оказват неунифицируеми. И наистина, ако допуснем, че някоя субституция s е техен унификатор, то ще имаме равенството s(A)=s(B), което дава, че p(a,s(X))=p(s(X),b), а последното равенство не е възможно, защото от него следва, че s(X) трябва да е равно както на a, така и на b.

    Пример 3. Нека A е променливата X, а B е термът f(X), където f е едноместен функционален символ. Ако допуснем, че някоя субституция s е унификатор на A и B, ще получим невъзможното равенство s(X)=f(s(X)) (то е невъзможно, защото дължината на дясната страна е с 3 по-голяма от дължината на лявата). Това показва, че споменатите два терма не са унифицируеми.

    Пример 4. Нека A=p(X,X),B=p(Y,f(Y)), където p е двуместен предикатен символ, f е едноместен функционален символ, X и Y са променливи. И в този случай A и B се оказват неунифицируеми. И наистина, да допуснем, че някоя субституция s е техен унификатор. Тогава ще имаме равенството s(A)=s(B), което дава, че p(s(X),s(X))=p(s(Y),f(s(Y))). От това равенство следват равенствата s(X)=s(Y),s(X)=f(s(Y)), от които пак се получава невъзможното равенство от предходния пример.

    Забележка 1. Да предположим, че са дадени два терма A и B. Да вземем някакъв двуместен предикатен символ e и някаква променлива Z и да разгледаме хорнова програма P, имаща за своя единствена клауза факта
       e(Z,Z).
Лесно се съобразява, че една субституция s е унификатор на A и B точно тогава, когато тя преобразува атомарната формула e(A,B) в атомарна формула, изводима от P (използваме, че една атомарна формула е изводима от P точно тогава, когато има вида e(Т,Т) за някой терм T). Като вземем пред вид, че атомарните формули, изводими от P, са точно атомарните формули, тъждествено верни във всеки модел за P, можем да направим още заключението, че една субституция s е унификатор на A и B точно тогава, когато тя преобразува целта
        ?- e(A,B).
в цел, изпълнена тъждествено при програмата P. По теоремата за характеризация на изпълнимите цели с помощта на минималния разширен ербранов модел това дава още, че A и B са унифицируеми точно тогава, когато горната цел е изпълнима при програмата P. Тъй като при използването на Пролог всяка атомарна формула може да се разглежда и като терм, току-що казаното позволява заключенията за унифицируемост и неунифицируемост във всеки от горните четири примера да бъдат направени и с помощта на Strawberry Prolog като се изпълни хорнова програма P от горния прост вид съответно върху целите
        ?- e(p(a,Y),p(X,b)).
        ?- e(p(a,X),p(X,b)).
        ?- e(X,f(X)).
        ?- e(p(X,X),p(Y,f(Y))).
Ще споменем обаче, че някои други софтуерни реализации на Пролог при изпълнение на споменатата програма P върху третата и четвъртата от горните цели биха дали положителен отговор в противоречие с действителното положение на нещата (ср. с казаното в забележка 4 от въпроса "Минимални разширени ербранови модели").

    Забележка 2. Когато работим със софтуерна реализация на Пролог, бихме могли да избегнем използването на програма P от вида, посочен в горния пример. Това е така, защото сред вградените предикати на Пролог се включва и двуместен предикат, означаван с обичайния знак за равенство, и този предикат фактически се характеризира само чрез равенството
        X=X.
(вж. например файла Standard.add на Strawberry Prolog - да речем чрез избиране на "Help" от менюто и след това на "ADD File"). Поради това бихме могли да заменим четирите цели от горния пример със следните, върху които да изпълним празна програма (програма без никакви клаузи):
        ?- p(a,Y)=p(X,b).
        ?- p(a,X)=p(X,b).
        ?- X=f(X).
        ?- p(X,X)=p(Y,f(Y)).

    Ако две атомарни формули са унифицируеми, то съществува атомарна формула, която е частен случай и на двете (достатъчно е да вземем атомарната формула, в която ги преобразува някой техен унификатор); разбира се аналогично е положението и с унифицируемите термове. С помощта на пример 2 можем да се убедим, че обратното не е вярно. Действително, въпреки че, както видяхме в този пример, атомарните формули p(a,X) и p(X,b) не са унифицируеми, атомарната формула p(a,b) е частен случай на всяка от тях (само че субституциите, които преобразуват p(a,X) и p(X,b) в нея, този път са различни). За щастие има лесен начин, чрез който може да се сведе към въпрос за унифицируемост всеки въпрос за съществуване на атомарна формула, която да е частен случай едновременно на две дадени атомарни формули (с този начин ще се занимаем в един от следващите въпроси). Засега ще покажем само, че ако за две атомарни формули с непресичащи се множества на променливите съществува атомарна формула, която е частен случай и на двете, то тези две атомарни формули са унифицируеми. И наистина, нека A и B са атомарни формули, за които сечението на множествата VAR(A) и VAR(B) е празно, и нека една атомарна формула C е частен случай както на A, така и на B. Тогава за някои две субституции a и b ще имаме равенствата C=a(A),C=b(B). Да дефинираме едно изображение s на множеството на променливите в множеството на термовете като положим s(X)=a(X) при XОVAR(A) и s(X)=b(X) при XОX \VAR(A). Лесно се вижда, че s е субституция. Тази субституция съвпада с a върху множеството VAR(A) и съвпада с b върху множеството VAR(B). Поради това s(A)=a(A)=C и s(B)=b(B)=C, следователно s(A)=s(B).

    Когато две атомарни формули са унифицируеми, те имат безбройно много унификатори. Това е очевидно, защото ако s е унификатор на две атомарни формули A и B, то всяка друга субституция, която съвпада със s върху множеството VAR(A)ИVAR(B), също е унификатор на A и B. Можем разбира се да считаме, че различните унификатори на A и B, които съвпадат върху споменатото множество, не се различават съществено един от друг. Има обаче и случаи, когато между два унификатора на дадена двойка от формули е налице по-съществено различие. Например, ако две атомарни формули съвпадат, то всяка субституция е техен унификатор, независимо от това какви термове съпоставя тя на техните променливи. С оглед на това, което предстои да направим, важно е да отбележим следното: ако една субституция s е унификатор на две дадени атомарни формули A и B, а d е произволна субституция, то субституцията ds също е унификатор на A и B. Проверката е съвсем проста: ако имаме равенството s(A)=s(B), то ще имаме и ds(A)=d(s(A))=d(s(B))=ds(B). Нека се условим да наричаме частни случаи на една субституция s субституциите от вида ds, където d е произволна субституция. Тогава можем да изкажем току-що отбелязаното свойство още и по такъв начин: ако една субституция е унификатор на две дадени атомарни формули, то и всеки неин частен случай е техен унификатор. Най-общ унификатор на две дадени атомарни формули ще наричаме такъв техен унификатор, на който всичките им унификатори са частни случаи. Ние ще докажем, че когато две атомарни формули са унифицируеми, те измежду техните унификатори има най-общ. Засега обаче ще дадем някои прости примери, в които непосредствено ще покажем съществуването на такъв унификатор.

    Пример 5. Ако две атомарни формули съвпадат, то тъждествената субституция е техен най-общ унификатор. Две затворени атомарни формули са унифицируеми точно тогава, когато съвпадат. Същите неща важат и за термове.

    Пример 6. В условията на пример 1 посочената там субституция [a,b=:X,Y] е най-общ унификатор на разглежданите в примера атомарни формули A и B. Действително, нека означим със s₀ споменатата субституция и нека s е произволен унификатор на A и B. Тогава ще имаме равенството p(a,s(Y))=p(s(X),b), от което следват равенствата s(X)=a,s(Y)=b. Като ги имаме пред вид, лесно можем да проверим, че за всяка променлива Z е изпълнено равенството s(Z)=ss₀(Z) (разглеждаме поотделно случаите, когато Z е X, когато Z е Y и когато Z е коя да е друга променлива). Резултатът от тази проверка показва, че е в сила равенството s=ss₀ и следователно s е частен случай на s₀.

    Забележка 3. Когато две атомарни формули са унифицируеми, измежду унификаторите им сигурно има такива, които не са най-общи. Действително, нека една субституция s е унификатор на две дадени атомарни формули A и B. Да си вземем две различни променливи Z₁ и Z₂, такива, че s(Z₁)=Z₁ и s(Z₂)=Z₂ (такива променливи сигурно има). След това да означим със sў субституцията [Z₁=:Z₂]s. Тогава sў пак е унификатор на A и B (защото е частен случай на техния унификатор s), но за разлика от s преобразува променливите Z₁ и Z₂ в един и същ терм (а именно в променливата Z₁). Лесно е да се убедим, че и всяка субституция, която е частен случай на sў, също ще преобразува Z₁ и Z₂ в един и същ терм. Поради това субституцията s не е частен случай на sў и значи sў не е най-общ унификатор на A и B.

    Забележка 4. За някои две унифицируеми атомарни формули A и B може да се случи всички унификатори (най-общи или не) да съвпадат върху множеството VAR(A)ИVAR(B) (разсъжденията от пример 6 показват, че в пример 1 положението е именно такова) . В такива случаи би могло да се счита, че унификаторите, които не са най-общи, са несъществено различни от най-общите.

    Една естествена и важна задача е да се познае дали две дадени атомарни формули или два дадени терма са унифицируеми и в случай, че са унифицируеми, да се намери техен унификатор. Сега ще извършим известна подготвителна работа и ще опишем някои от елементите на един метод за решаване на тази задача, като пълното описание на метода ще завършим в следващия въпрос (методът по съшество е даден от Ербран - в параграф 2.4 от гл. 5 на дисертацията му; доста е известен и друг метод, даден през 1965 г. от Джон А. Робинсън в неговата статия за резолюцията).

    Да наречем две атомарни формули еднотипни, ако те представляват един и същ нулместен предикатен символ или пък имат вида p(T₁,T₂...,T_n) и p(U₁,U₂...,U_n), където n е положително цяло число, p е n-местен предикатен символ и T₁, ..., T_n, U₁, ..., U_n са термове. По аналогичен начин се дефинира и еднотипност за два терма, никой от които не е променлива - достатъчно е в горното условие думата "предикатен" да се замени с думата "функционален" (не е зле още в този случай вместо p да се напише f). Разбира се, ако две атомарни формули или два терма, които не са променливи, съвпадат, те са еднотипни; освен това отношението еднотипност е симетрично и транзитивно. Очевидно е също, че при прилагане на произволна субституция към една атомарна формула резултатът е атомарна формула, еднотипна с дадената, и аналогично твърдение важи за резултата от прилагане на субституция към терм, който не е променлива. От казаното става ясно, че ако A и B са атомарни формули или са термове, никой от които не е променлива, и A и B не са еднотипни, то A и B не са унифицируеми. Не е вярно обаче, че при еднотипност имаме винаги унифицируемост. Това се вижда да речем от пример 2, а може да се види и по-просто - например еднотипни, но не унифицируеми са атомарните формули p(a) и p(b), където p е едноместен предикатен символ, а a и b са константи.

    Да предположим, че са дадени две произволни атомарни формули A и B и се интересуваме дали те са унифицируеми. Ако A и B не са еднотипни, отговорът на този въпрос е отрицателен. Да предположим сега, че A и B са еднотипни. Ако A и B съвпадат, те са унифицируеми и тъждествената субституция е техен най-общ унификатор, както отбелязахме в пример 5. Остава да се занимаем с подслучая, когато атомарните формули A и B са различни. Тогава със сигурност ще имаме

    За по-удобното записване на това, което ше правим по-нататък, уславяме се при произволен избор на термове T и U да наричаме решения на уравнението T=U онези субституции s, за които е изпълнено равенството s(T)=s(U) (за такива субституции ще казваме още, че удовлетворяват уравнението T=U). Разбира се, ще казваме, че дадена субституция е решение на една система от уравнения от този вид (или че удовлетворява тази система), ако тя е решение на всяко от нейните уравнения. С използване на тази терминология можем казаното преди малко да го преформулираме така: ако n е положително цяло число, p е n-местен предикатен символ и T₁,...,T_n,U₁,...,U_n са термове, то унификатори на атомарните формули p(T₁,T₂...,T_n) и p(U₁,U₂...,U_n) са точно онези субституции, които са решения на системата от уравнения

(1)	T1=U1, T2=U2, ..., Tn=Un.

По такъв начин ние сведохме по-трудните задачи за търсене на унификатор на две атомарни формули към решаването на системи от уравнения от току-що посочения вид. Разбира се задачата за търсене на унификатор на два терма T и U директно се свежда до решаването на уравнението T=U, т.е. пак до решаването на система от вида (1), но с n=1.

    Пример 7. На двете атомарни формули от пример 1 унификатори са точно онези субституции, които удовлетворяват системата a=X,Y=b, а на двете атомарни формули от пример 2 - точно онези субституции, които удовлетворяват системата a=X,X=b (само че такива субституции няма).

    И така, задачата ни ще бъде да опишем как да работим, когато е дадена една система от вида (1), за да видим дали тя има решение и да охарактеризираме по-просто нейните решения, когато тя има такива. За пълнота няма да изключваме от нашите разглеждания и празна система от уравнения (с n=0) - ще считаме, че всяка субституция я удовлетворява.

    Забележка 5. Нека P е програмата, състояща се от един факт и разгледана в забележка 1, и нека е дадена една система от вида (1). С разсъждения, подобни на онези от забележка 1, се вижда, че дадената система ще има решение точно тогава, когато при P е изпълнима съответната цел
        ?- e(T₁,U₁), e(T₂,U₂), ..., e(T_n,U_n).
Казаното в забележка 2 позволява при използването на Пролог вместо това да прилагаме празна програма към целта
        ?- T₁=U₁, T₂=U₂, ..., T_n=U_n.

    За една променлива ще казваме, че участва в дадено уравнение T=U, когато тя е променлива на поне един от термовете T и U, а ще казваме, че участва в една система от вида (1), ако участва в поне едно от уравненията на системата. Променливите, участващи в дадена система от уравнения, ще наричаме нейни неизвестни. За две системи от уравнения ще казваме, че са  еквивалентни, ако те имат едни и същи решения (включваме и случая, когато никоя от двете системи няма решение). Най-общо решение на дадена система от вида (1) ще наричаме такова нейно решение, че всички решения на системата да са негови частни случаи.

    Система в решен вид ще наричаме всяка система уравнения от вида

(2)	X1=U1, X2=U2, ..., Xn=Un,

където X₁, X₂,...,X_n са различни помежду си променливи, а U₁, U₂, ..., U_n са такива термове, че X_iПVAR(U_j) при i,j=1,2,...,n (за празната система също считаме, че е в решен вид). Сега ще покажем, че ако (2) е система в решен вид, a s₀ е субституцията

    Пример 8. Първата от системите, написани в пример 7, е очевидно еквивалентна на системата X=а,Y=b, която е в решен вид. Така още веднаж (ср. с пример 6) виждаме, че субституцията [a,b=:X,Y] е най-общ унификатор на двете атомарни формули от пример 1.

    Ако в една система от вида (1) някое от уравненията няма решение, то очевидно и цялата система няма решение. Сега ще отбележим изрично два случая, когато уравнение, на което страните са термове, няма решение; ще ги наричаме съответно първи и втори случай на явна нерешимост, а всяко уравнение, за което е налице някой от тези два случая, ще наричаме явно нерешимо. Първият случай е онзи, когато никоя от двете страни на уравнението не е променлива и двете страни не са еднотипни. Вторият се описва чрез следното твърдение, което сега ще докажем: ако X е променлива, а U е такъв терм, различен от X,  че XОVAR(U), то уравнението X=U няма решение. Това твърдение следва от факта, че при изказаните предположения за X и U дължината на терма s(U) ще бъде строго по-голяма от дължината на терма s(X), както и да избираме субституцията s (въпросният факт се установява като се използва обстоятелството, че винаги, когато m е положително цяло число, f е m-местен функционален символ и V₁, V₂,...,V_m са термове, резултатът от прилагането на една субституция към терма f(V₁,V₂...,V_m) има по-голяма дължина от резултата от прилагането на субституцията към кой да е от термовете V₁, V₂,...,V_m - това обстоятелство позволява първо да се докаже индуктивно, че винаги, когато U е терм и XОVAR(U), дължината на s(X) никога не надминава дължината на s(U), а след това да се покаже, че споменатото неравенство е строго при допълнителното условие термът U да е различен от X).

    Пример 9. Нека f е едноместен функционален символ, а X е променлива. От току-що доказаното следва, че уравнението X=f(X) няма решение. Всъщност това вече го установихме и с директни разсъждения в пример 3.

    Забележка 6. Всяка софтуерна реализация на Пролог използва съществено някой метод за унификация, а при коректното му използване би трябвало да се оказва, че унификацията е невъзможна, когато  при опит за нейното осъществяване възникне някой от отбелязаните два случая на явна нерешимост. За съжаление в много от реализациите на Пролог (но не и в Strawberry Prolog) съзнателно е допусната некоректност на действията при възникване на втория от тези случаи, като заради повишаване на бързодействието е спестен тъй нареченият "occurs check". Именно това става причина за некоректностите от рода на онези, които бяха посочени в забележка 1 от настоящия въпрос и в забележка 4 от въпроса "Минимални разширени ербранови модели".

    Пример 10. Нека p е двуместен предикатен символ, f е едноместен функционален символ, а X и Y са променливи. Да разгледаме хорнова програма P, състояща се само от факта
        p(X,X).
Да разгледаме и целта
        ?- p(X,f(X)).
Тази цел не е изпълнима при програмата P, защото съгласно забележка 1 това би означавало да са унифицируеми термовете X и f(X), т.е. да има решение уравнението X=f(X). Във връзка с резултатите,  които дава изпълнението на програмата P върху разглежданата цел при използване на конкретни софтуерни реализации на Пролог, ще отбележим обаче следното: ако използваме Strawberry Prolog, получаваме правилния отговор "No", но при използването на някои от другите софтуерни реализации на езика се получава положителен отговор. Например Arity Prolog, версия 5.1, показва на екрана първия от резултатите, споменати в забележка 4 от въпроса "Минимални разширени ербранови модели".
 

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

Previous  Next  Contents