Пример 1. Нека p е двуместен предикатен символ. Тогава атомарната формула p(Y,Z) е вариант на атомарната формула p(X,Y), а атомарната формула p(X,X) не е вариант на p(X,Y).

    Лесно се съобразява, че всеки вариант на A има същите частни случаи както A.

    Нека a е субституция, а X₀ е някое множество от променливи. Ще казваме, че a е преименуваща върху X₀, ако a преобразува всяка променлива от множеството X₀ пак в променлива (не непременно принадлежаща на X₀) и преобразува различните променливи от X₀  пак в различни.

    Пример 2. Субституцията [Y,Z=:X,Y] е преименуваща върху множеството {X,Y}, но не е преименуваща върху множеството {X,Y,Z}. Ако T е терм, който не е променлива, то субституцията [T,X=:X,Y] не е преименуваща въху множеството {X,Y}, но е преименуваща върху всяко множество от променливи, което не съдържа променливата X.

    Сега ще установим връзка между варианти и субституции, преименуващи върху дадено множество.

    Твърдение 1. Нека A е терм, атомарна формула, хорнова цел или хорнова клауза, а a е субституция, която е преименуваща върху множеството VAR(A). Тогава a(A) е вариант на A.

    Доказателство. Множеството от променливи VAR(A) е крайно. Тогава и неговият образ посредством a е краен. Да означим въпросния образ чрез X₁ и да дефинираме изображение aў на X в X, като положим aў(a(X))=X при XОVAR(A) и aў(Y)=Y при YПX₁. Ясно е, че изображението aў е субституция и че субституцията aўa съвпада с тъждествената субституция за всички променливи на A. Това позволява да се твърди, че е в сила равенството aў(a(A))=A и следователно A е частен случай на своя частен случай a(A).  _ї

    Следствие 1. Нека A е терм, атомарна формула, хорнова цел или хорнова клауза и нека е дадено някое крайно множество от променливи. Тогава A притежава вариант, на който никоя от променливите не принадлежи на въпросното множество.

    Доказателство. Преобразуваме A чрез субституция, която замества променливите от VAR(A) с различни променливи, непринадлежащи на даденото множество.  _ї

    Следствие 2. За всеки две атомарни формули съществува вариант на първата, който няма общи променливи с втората.

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

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

    Лема 1. Ако една субституция преобразува даден терм в променлива, той също е променлива.

    Доказателство. Ако един терм не е променлива, той е константа или има вида f(T₁,T₂...,T_n), където n е положително цяло число, f е n-местен функционален символ и T₁, ...,T_nса термове. И в двата случая резултатът от прилагане на субституция към въпросния терм е терм, който не е променлива.  _ї

    Лема 2. Нека  A е терм, атомарна формула, хорнова цел или хорнова клауза, а s е такава субституция, че s(A)=А. Тогава s(X)=X за всяка променлива X на A.

    Доказателство. За случая, когато A е терм, твърдението се доказва чрез индукция, съобразена с дефиницията за терм, като се използва и дефиницията за множество на променливите на един терм. Веднаж доказано за този случай, твърдението лесно се разпространява за останалите.  _ї

    Твърдение 2. Нека A е терм, атомарна формула, хорнова цел или хорнова клауза. Тогава всеки вариант на A има вида a(A), където a е субституция, преименуваща върху множеството VAR(A).

    Доказателство. Нека Aў е произволен вариант на A. Тогава за някои субституции a и aў са в сила равенствата Aў=a(A) и A=aў(Aў). От тези равенства следва равенството aў(a(A))=A, което може да се напише и във вида aўa(A)=A. Оттук с помощта на лема 2 заключаваме, че за всяка променлива X на A имаме равенството aўa(X)=X, а значи и равенството aў(a(X))=X. Това в съчетание с лема 1 показва, че за всяка променлива X на A съответният й терм a(X) е пак променлива. Освен това ако X₁ и X₂ са две различни променливи на A, то от равенствата aў(a(X₁))=X₁ и aў(a(X₂))=X₂ виждаме, че a(X₁) и a(X₂) също са различни.  _ї

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

    Пример 3. Тъждествената субституция, субституцията [Y,X=:X,Y] и субституцията [Z,X,Y=:X,Y,Z] са преименуващи.

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

    Твърдение 3. Една субституция е преименуваща точно тогава, когато тя е естествено продължение на някоя пермутация на променливи.

    Доказателство. Ако една субституция е естествено продължение на пермутация на променливи, то тази субституция очевидно е преименуваща. По-нетривиално е обратното. За да го докажем, да предположим, че d е произволна преименуваща субституция. Нека D е множеството на онези променливи X, за които d(X)№X. Това множество е крайно според дефиницията за субституция. Понеже субституцията d преобразува променливите в променливи и различните променливи в различни, ясно е, че за всяка променлива X от D ще бъде в сила неравенството d(d(X))№d(X) и следователно d(X) ще бъде пак елемент на D. Да означим с q рестрикцията на d върху множеството D. Тогава q е пермутация на променливи, а d е естествено продължение на q.  _ї

    Следствие 3. Всяка преименуваща субституция е взаимно еднозначно изображение на множеството X върху себе си.

    За следващите разглеждания ще имаме нужда от още една лема. Да наречем заместване всяко изображение на крайно множество от променливи в множеството на термовете. Преименуващо заместване ще наричаме такова заместване, при което на променливите от дефиниционната му област съответстват пак променливи (не непременно от нея) и на различните променливи от нея съответстват пак различни. Ясно е, че пермутациите на променливи са специален вид преименуващи замествания.

    Лема 3. Нека r е преименуващо заместване. Тогава съществува такава преименуваща субституция d, че d(X)=r(X) за всяка променлива X от дефиниционната област на r и d(X)=X за всяка променлива X, която не принадлежи нито на дефиниционната област, нито на множеството на стойностите на r.

    Доказателство. Ясно е, че дефиниционната област dom(r) на r и множеството на стойностите  range(r) на r са крайни множества с равен брой елементи. Като използваме равенствата

    Ще илюстрираме конструкцията от горното доказателство с един пример.

    Пример 4. Нека dom(r)={X,Y,Z}, r(X)=U, r(Y)=V, r(Z)=X. Тогава

    С помощта на лема 3 ще дадем следното усилване на твърдение 2.

    Твърдение 2ў.Нека A е терм, атомарна формула, хорнова цел или хорнова клауза. Тогава всеки вариант на A има вида d(A), където d е преименуваща субституция.

    Доказателство. Нека  Aў е произволен вариант на A. Според твърдение 2 Aў има вида a(A), където a е някоя субституция, преименуваща върху множеството VAR(A). Да означим с r рестрикцията на a върху множеството VAR(A). Така полученото изпбражение r е преименуващо заместване и според лема 3 съществува преименуваща субституция d, която съвпада с r за променливите от dom(r). Тъй като въпросната субституция d ще съвпада с a за променливите на A, ще имаме равенството d(A)=a(A).  _ї

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

    Твърдение 4. Нека a е субституция, която е преименуваща върху дадено множество от променливи X₀. Тогава съществува преименуваща субституция, съвпадаща с a върху множеството X₀.

    Доказателство. Да означим с r рестрикцията на a върху множеството на онези променливи X от X₀, за които a(X)№X. Така дефинираното изображение r представлява едно преименуващо заместване, следователно можем да приложим лема 3 и да получим преименуваща субституция d с изказаните в лемата свойства. Ще покажем, че d съвпада с a върху множеството  X₀. Тъй като d е продължение на r, всъщност трябва само да покажем, че и за онези променливи X от X₀, които не принадлежат на dom(r), имаме равенството d(X)=a(X). Нека X е променлива от X₀, която не принадлежи на dom(r). Тогава ще имаме равенството a(X)=X и значи ще трябва да покажем, че имаме и равенството d(X)=X. Това ще направим, като установим, че X не принадлежи и на range(r). Да допуснем противното - че X принадлежи на range(r). Това дава, че X=r(Xў)=a(Xў) за някоя променлива Xў, която принадлежи на dom(r). Но в такъв случай се получава, че за двете различни променливи X и Xў, принадлежащи на X₀, стойностите на a съвпадат в противоречие с обстоятелството, че субституцията a е преименуваща върху X₀.  _ї

    Ако s е субституция, ще наричаме вариант на s такъв неин частен случай sў, че и s да бъде частен случай на sў.

    Пример 5. Ако A и B са две унифицируеми атомарни формули, а s и sў са два най-общи унификатора на A и B, то sў е вариант на s.

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

    Твърдение 5. Нека s е произволна субституция. Тогава варианти на s са точно субституциите от вида ds, където d е преименуваща субституция.

    Доказателство. Ако d е преименуваща субституция, то следствие 3 позволява да образуваме обратната й субституция d^-1 и да твърдим, че произведението d^-1d е тъждествената субституция, а това дава равенствата d^-1(ds)=(d^-1d)s=s, от които се вижда, че s е частен случай на своя частен случай ds, т.е.ds е вариант на s. За разсъждението в обратната посока да предположим, че sў е произволен вариант на s. Тогава ще имаме равенствата sў=as и s=aўsў за някои две субституции a и aў. Да означим с X₀ обединението на множествата VAR(s(Z)), съответстващи на всевъзможните променливи Z. Ще покажем, че за всяка променлива X от X₀ е изпълнено равенството aў(a(X))=X. И наистина, нека X е произволна променлива от множеството X₀. Тогава XОVAR(s(Z)) за някоя променлива Z. Ще имаме равенствата

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

Previous  Next  Contents