Решаване на системи от уравнения между термове

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

Вече видяхме, че търсенето на унификатор на две атомарни формули в по-трудните случаи се свежда до решаване на нетъждествена система уравнения от вида

(1)

τ₁ = θ₁, …, τ_n = θ_n,

където n е положително цяло число, а τ₁, …, τ_n, θ₁, …, θ_n са термове.

Две системи от вида (1) ще наричаме еквивалентни, ако те имат едни и същи решения. Ще опишем един начин за решаване на такива системи, който се състои в извършването на подходящи замени на системата от уравнения с еквивалентна на нея, докато се получи система, която е явно нерешима или е в решен вид. Предварително ще отбележим, че когато две системи от споменатищ вид са еквивалентни и едната от тях не е тъждествена, то и другата не е тъждествена (това следва от забележката в края на текста „Унификация на атомарни формули и нейното свеждане до решаване на системи от уравнения между термове“).

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

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

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

ω(α₁,…,α_m) = ω(β₁,…,β_m), където m е положително цяло число, ω е m-местен функционален символ и α₁, …, α_m, β₁, …, β_m са термове. Тогава то може да се замени с m-те уравнения α₁ = β₁, …, α_m = β_m. Получената по този начин система ще бъде еквивалентна на (1), защото едни и същи са субституциите, които удовлетворяват разглежданото уравнение, и субституциите, които удовлетворяват едновременно всяко едно от m-те заменили го уравнения. Действително, една субституция σ удовлетворява разглежданото уравнение точно тогава, когато е изпълнено равенството ω(α₁σ,…,α_mσ) = ω(β₁σ,…,β_mσ), а за да бъде изпълнено то, необходимо и достатъчно е да бъдат изпълнени m-те равенства α₁σ = β₁σ, …, α_mσ = β_mσ.

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

4. Заместване. Нека някое уравнение в (1), да речем i-тото, има вида ξ = θ , където ξ е променлива, θ е терм, ξ не е променлива на θ, но е променлива на лява или дясна страна в някое друго от уравненията на (1). Тогава системата (1) може да се преобразува като се запази споменатото нейно i-то уравнение, а във всяко друго от нейните уравнения двете му страни се заменят с резултатите от прилагането към тях на субституцията [ξ/θ] . Да означим така получената система от уравнения с (1)′. Тя е еквивалентна на (1). И наистина, наличието на уравнението ξ = θ и в двете системи гарантира, че всяка субституция, която е решение на някоя от двете, ще бъде решение и на системата, състояща се само от това уравнение. Понеже последната е в решен вид, известното ни от предходния въпрос за системи от такъв вид позволява да твърдим, че за всяка субституция σ, която е решение на някоя от системите (1) и (1)′, ще бъде в сила равенството σ = [ξ/θ] σ . Да разгледаме сега j-тото уравнение на системата (1) и j-тото уравнение на системата (1)′, където j е различно от i. Тези уравнения са съответно τ_j = θ_j и τ_j [ξ/θ] = θ_j [ξ/θ] . Второто от тях ще се удовлетворява от дадена субституция σ точно тогава, когато субституцията [ξ/θ] σ удовлетворява първото. Следователно ако една субституция е решение на някоя от системите (1) и (1)′, тя ще удовлетворява j-тото уравнение на (1)′ точно тогава, когато удовлетворява j-тото уравнение на (1), и значи всъщност ще удовлетворява и двете j-ти уравнения. Оттук, понеже i-тото уравнение на системите (1) и (1)′ е едно и също, виждаме, че (1) и (1)′ имат едни и същи решения.

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

Пример 1. При сигнатура с константи a и b да рагледаме двете системи

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

Пример 2. При сигнатура с едноместен функционален символ f ще разгледаме системата

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

Пример 3. Да променим малко горния пример като разгледаме системата

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

Пример 4. При сигнатура с константа a и едноместен функционален символ f да рагледаме системата

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

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