Previous  Next  Contents
 

 

РЕШАВАНЕ НА СИСТЕМИ ОТ УРАВНЕНИЯ МЕЖДУ ТЕРМОВЕ

    В предходния въпрос видяхме как търсенето на унификатор на две атомарни формули в по-трудните случаи се свежда до решаване на система уравнения от вида
(1) T1=U1, T2=U2, ..., Tn=Un,
където T1, T2, ..., Tn, U1, U2, ..., Un са термове (видяхме, че и търсенето на унификатор на два терма се свежда до такава система, но с n=1). Сега ще опишем един начин за решаване на такива системи. Начинът се състои в извършването на подходящи замени на системата от уравнения с еквивалентна на нея, докато евентуално се получи система, която е в решен вид, или система, която съдържа явно нерешимо уравнение. Ясно е, че ако се получи такава система, то задачата за решаването на първоначалната система ще бъде решена - за всяка система в решен вид знаем, че има решение, и ни е известно нейно най-общо решение, а ако една система съдържа явно нерешимо уравнение, тя няма решение.

    Заменянето на система от вида (1) с еквивалентна на нея  ще бъде разрешено да се извършва чрез някое от четири специални преобразувания на системата, които сега ще опишем последователно.

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

    2. Разпадане. То може да се извърши, когато на дадено уравнение в (1) никоя от двете страни не е нито променлива, нито константа и двете му страни са еднотипни термове. А именно, нека въпросното уравнение има вида

f(V1,V2...,Vm)=f(W1,W2...,Wm),
където m е положително цяло число, f е m-местен функционален символ и V1, V2, ...,Vm, W1, W2,...,Wm са термове. Тогава то може да се замени с m-те уравнения
V1=W1,  V2=W2,  ...,  Vm=Wm.
Получената по този начин система ще бъде еквивалентна на (1), защото едни и същи са субституциите, които удовлетворяват разглежданото уравнение, и субституциите, които удовлетворяват едновременно всяко едно от m-те заменили го уравнения. Действително, една субституция s удовлетворява разглежданото уравнение точно тогава, когато е изпълнено равенството
f(s(V1),s(V2)...,s(Vm))=f(s(W1),s(W2)...,s(Wm)),
 а за да бъде изпълнено то, необходимо и достатъчно е да бъдат изпълнени m-те равенства
s(V1)=s(W1), s(V2)=s(W2), ..., s(Vm)=s(Wm).

    3. Обръщане. Нека дадено уравнение в (1) има вида T=X, където T е терм, различен от променлива, а X е променлива. Тогава то може да се замени с уравнението X=T. Очевидно двете уравнения имат едни и същи решения, следователно системата, получена чрез такова преобразуване, ще бъде еквивалентна на (1).

    4. Заместване. Нека някое уравнение в (1), да речем i-тото, има вида X=U, където X е променлива, U е терм, X не е променлива на U и X участва в някое друго от уравненията на (1). Тогава системата (1) може да се преобразува като се запази споменатото нейно i-то уравнение, а във всяко друго от нейните уравнения двете му страни се заменят с резултатите от прилагането към тях на субституцията [U=:X]. Така получената система от уравнения също ще бъде еквивалентна на (1). И наистина, наличието на уравнението X=U и в двете системи гарантира, че за всяка субституция s, която удовлетворява някоя от тях, ще бъде в сила равенството s(X)=s(U). От друга страна, всяка субституция s, за която е изпълнено последното равенство, съвпада със съответната субституция s[U=:X] (показва се, че двете субституции съвпадат за всяка променлива, като се разглеждат поотделно случаят на променлива X и случаят на друга променлива). Да разгледаме сега j-тото уравнение Тj =Uj  на (1), където j№i. След преобразуването, което разглеждаме, въпросното уравнение ще се превърне в уравнението [U=:X](Тj )=[U=:X](Uj ). От казаното преди малко обаче е ясно, че последното уравнение ще се удовлетворява от една субституция s, имаща свойството, че s(X)=s(U), точно тогава, когато тази субституция удовлетворява уравнението Тj =Uj.

    Пример 1. В пример 7 от предходния въпрос сведохме два въпроса за унифицируемост (от предходни примери) към двете системи

a=X,  Y=b,
a=X,  X=b.
Към всяка от тях е приложимо преобразуването обръщане и то заменя двете системи съответно със системите
X=a,  Y=b,
X=a,  X=b.
Първата от тях е в решен вид, а към втората е приложимо преобразуването заместване и то даже по два различни начина. Като приложим към втората система заместване по единия от двата възможни начина, получаваме системата
X=a,  a=b,
която съдържа явно нерешимото уравнение a=b (по другия начин се получава система, съдържаща явно нерешимото уравнение b=a). Да отбележим, че към втората от двете разглеждани системи можеше и направо да приложим замествана - по такъв начин щяхме веднага да получим системата
a=b,  X=b,
съдържаща явно нерешимото уравнение a=b.

    Пример 2. Нека се интересуваме дали са унифицируеми атомарните формули p(X,f(X)) и p(f(Y),Z), където p е двуместен предикатен символ, f е едноместен функционален символ и X, Y, Z са променливи. Съответната система от вида (1) е следната:

X=f(Y),   f(X)=Z.
Чрез последователно заместване и обръщане (няма значение в какъв ред) получаваме системата
X=f(Y),   Z=f(f(Y)),
която е в решен вид. Това показва, че разглежданите две атомарни формули са унифицируеми и имат най-общ унификатор [f(Y),f(f(Y))=:X,Z].

    Пример 3. Да променим малко горния пример като заменим втората от двете атомарни формули с p(f(Y),Y), Тогава съответната система от вида (1) ще бъде следната:

X=f(Y),   f(X)=Y.
Ако извършим заместване и след това обръщане, от нея получаваме системата
X=f(Y),   Y=f(f(Y)),
на която второто уравнение е явно нерешимо. Това показва, че атомарните формули p(X,f(X)) и p(f(Y),Y) не са унифицируеми.

    Пример 4. Нека се интересуваме дали са унифицируеми атомарните формули p(X,f(Y)) и p(f(a),X), където p, f, X, Y са както в предходните два примера, а пък a е константа. Съответната система от вида (1) е следната:

X=f(a),   f(Y)=X..
От нея чрез заместване получаваме системата
X=f(a),   f(Y)=f(a),
а оттук чрез разпадане се получава системата
X=f(a),   Y=a.
По този начин виждаме, че разглежданите две атомарни формули са унифицируеми и имат най-общ унификатор [f(a),a=:X,Y].

    В разгледаните няколко примера имахме системи от вида (1), от които с извършване на известен брой преобразувания от изброените четири вида винаги се стига до система в решен вид или система, съдържаща явно нерешимо уравнение. Нещо повече - почти винаги имаше различни възможности за извършване на преобразуванията, но едно изчерпателно изследване на вариантите лесно би показало, че така би станало при всеки от тях. Възниква въпросът дали при всяка система от уравнения от вида (1) положението е непременно такова. Отговорът на този въпрос е положителен и предстои сега да докажем, че е така. За краткост поставения въпрос ще наречем въпрос за резултатност.

    Най-напред ще се убедим, че ако една система от вида (1) не е в решен вид и не съдържа явно нерешимо уравнение, то към нея е приложимо поне едно преобразуване, имащо някой от изброените четири вида. И наистина, нека системата (1) не е в решен вид и не съдържа явно нерешимо уравнение. Ще разгледаме два случая: а) лявата страна на всяко от уравненията в (1) е някоя променлива; б) в (1) има уравнение, на което лявата страна не е променлива. В случая а) ще разгледаме два подслучая: а1) лявата страна на някое от уравненията е променлива на дясната му страна; а2) лявата страна на никое от уравненията не е променлива на дясната му страна. В подслучая а1), като използваме, че системата не съдържа явно нерешимо уравнение, заключаваме, че системата съдържа уравнение, на което лявата и дясната страна са една и съща променлива - следователно в този подслучай може да се извърши премахване на тъждество. В подслучая а2), като използваме, че системата не е в решен вид, заключаваме, че лявата страна на някое от уравненията участва и в друго измежду тях - следователно в този подслучай може да се извърши заместване. Да предположим сега, че е налице случаят б) и да разгледаме уравнение от (1), на което лявата страна не е променлива. Ако дясната страна на това уравнение е променлива, то ще може да се извърши обръщане. Остава да разгледаме възможността и дясната страна на това уравнение да не е променлива. Понеже системата не съдържа явно нерешимо уравнение, двете страни на разглежданото уравнение трябва да бъдат еднотипни. Едната възможност за това е двете страни да представляват една и съща константа - тогава ще може да се извърши премахване на тъждество. Другата възможност е уравнението да има вида

f(V1,V2...,Vm)=f(W1,W2...,Wm),
където m е положително цяло число, f е m-местен функционален символ и V1, V2, ...,Vm, W1, W2,...,Wm са термове - тогава пък ще може да се извърши разпадане.

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

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

    Нека е дадена една система от уравнения от вида (1) и нека X е едно от неизвестните й. Ще казваме, че системата е решена относно X, ako X е лява страна на някое уравнение от системата и нито е променлива на дясната му страна, нито участва в някое друго от уравненията на системата. Лесно се проверява, че ако в системата има уравнение от въпросния вид, това уравнение се запазва или преминава в уравнение от същия вид при всяко от четирите разглеждани преобразувания. Следователно ако системата е решена относно дадена променлива и извършим някое от четирите преобразувания, новополучената система също ще е решена относно тази променлива. Освен това при всяко от четирите преобразувания множеството на неизвестните на новополучената система се съдържа в множеството на неизвестните на онази, от която е получена. Значи същото ще важи и за множеството на неизвестните, относно които системата не е решена. Това показва, че при никое от четирите вида преобразувания не може да нарастне броят на неизвестните, относно които системата не е решена. От друга страна при заместване този брой намалява строго, защото лявата страна X на използваното за заместването уравнение X=U при това преобразуване отпада от множеството на неизвестните, относно които системата не е решена. Ясно е при това положение, че когато тръгнем от една система от вида (1) и последователно извършваме преобразувания от четирите вида, не е възможно заместване да се извърши повече пъти, отколкото са неизвестните в първоначалната система. Остава да се убедим, че за всяка система от вида (1) има горна граница и за това колко пъти последователно могат да се извършват преобразувания от останалите три вида, без да се извършва заместване.

    Ще дефинираме за всеки терм положително цяло число, което ще наричаме негово тегло. Дефиницията е индуктивна: считаме, че променливите имат тегло 1, константите имат тегло 2, а теглото на терм от вида f(V1,V2...,Vm) при обичайните предположения за m, f, V1,V2,...,Vm е увеличеният с 1 сбор от теглата на термовете V1,V2,...,Vm. Ясно е при тази дефиниция, че терм, който не е променлива, непременно има тегло, по-голямо от 1. Като използваме дефиницията и това следствие от нея, лесно виждаме, че ако подложим една система от вида (1) на някое преобразуване от първите три вида (без заместване), то сборът от теглата на левите страни на системата се намалява поне с 1. Това показва, че ако тръгнем от коя да е система от вида (1), не е възможно последователно да извършваме преобразувания само от първите три вида повече пъти отколкото е сборът на теглата на левите страни на системата, от която сме тръгнали.

    Забележка 2. При заместване сборът на теглата на левите страни може не само да не намалее, а даже да нарастне (да речем в системата X=a, X=b от пример 1 левите части на уравненията имат сбор 2, а за системата X=a, a=b, получена от нея чрез заместване, този сбор е 3). Това е причината, поради която в направените разсъждения си служим и с още един показател - броят на неизвестните, относно които системата не е решена. Би могло да се мине и само с един показател, но ако той се избере другояче.

    Забележка 3. Когато една система от вида (1) няма решение, това нерядко може да се види по описания начин без да има нужда да се извършват преобразувания от четирите вида до получаване на система, към която повече не са приложими такива преобразувания. Например системата

X=f(Y),   X=a ,  Y=X
допуска по три различни начина да се извърши заместване (предполагаме разбира се, че f е едноместен функционален символ, a е константа и X, Y са променливи). При единия от тях се получава системата
a=f(Y),   X=a ,  Y=a,
към която отново е приложимо заместване, но няма нужда то да се прилага, тъй като първото уравнение на тази система е явно нерешимо и значи тя няма решение.

    От нещата, които установихме, може да се направи следното заключение: ако една система от уравнения от вида (1) с множество на неизвестните X0 има решение, тя има най-общо решение от вида [W1,...,Wk=:X1,...,Xk], където

{X1,...,Xk} Н X0,    VAR(W1) И ... И VAR(Wk) Н X0 \ {X1,...,Xk}.
Следователно ако A и B са унифицируеми атомарни формули или унифицируеми термове и X0 е множеството VAR(A)ИVAR(B), то A и B имат най-общ унификатор от вида [W1,...,Wk=:X1,...,Xk], където X1, ..., Xk, W1, ..., Wk удовлетворяват горните условия.
 

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