Унификация на атомарни формули и нейното свеждане до решаване на системи от уравнения ...

УНИФИКАЦИЯ НА АТОМАРНИ ФОРМУЛИ И НЕЙНОТО СВЕЖДАНЕ ДО РЕШАВАНЕ НА СИСТЕМИ ОТ УРАВНЕНИЯ МЕЖДУ ТЕРМОВЕ

За извършването на SLD-резолюция е важно да умеем по две дадени атомарни формули да намираме такава атомарна формула, която е частен случай и на двете. Действително, за да образуваме SLD-резолвента на едно непразно хорново запитване и една положителна хорнова клауза, налага се всъщност да намерим атомарна формула, която е едновременно частен случай на първата атомарна формула от запитването и на онази, която е заключение на клаузата. Методът на унификацията, с който предстои да се занимаем, е основното средство за търсене на атомарна формула, която е частен случай на всяка от две дадени атомарни формули.

Нека φ и ψ са две атомарни формули. Техен унификатор ще наричаме всяка субституция, която преобразува φ и ψ в една и съща атомарна формула. Ще казваме, че φ и ψ са унифицируеми, ако те имат поне един унификатор.

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

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

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

Ако две атомарни формули са унифицируеми, то съществува атомарна формула, която е частен случай и на двете (достатъчно е да вземем атомарната формула, в която ги преобразува някой техен унификатор). С помощта на пример 2 можем да се убедим, че обратното не е вярно. В този пример видяхме, че атомарните формули p(a,X) и p(X,b) не са унифицируеми. Въпреки това обаче атомарната формула p(a,b) е частен случай на всяка от тях (само че субституциите, които преобразуват p(a,X) и p(X,b) в нея, този път са различни). Ще покажем все пак следното: ако за две атомарни формули с непресичащи се множества на променливите съществува атомарна формула, която е частен случай и на двете, то тези две атомарни формули са унифицируеми. И наистина, нека φ и ψ са атомарни формули, за които сечението на множествата VAR(φ) и VAR(ψ) е празно, и нека една атомарна формула χ е частен случай както на φ, така и на ψ. Тогава за някои две субституции σ₁ и σ₂ ще имаме равенствата χ = φσ₁, χ = ψσ₂. Да дефинираме едно изображение σ на множеството на променливите в множеството на термовете, като положим σ(ξ) = σ₁(ξ) за всяка променлива ξ от множеството VAR(φ) и σ(ξ) = σ₂(ξ) за всяка променлива ξ, непринадлежаща на това множество. Лесно се вижда, че σ е субституция. Тази субституция съвпада с σ₁ върху множеството VAR(φ) и съвпада с σ₂ върху множеството VAR(ψ). Поради това φσ = φσ₁ = χ и ψσ = ψσ₂ = χ, следователно φσ = ψσ.

Когато две атомарни формули са унифицируеми, те имат безбройно много унификатори. Това е очевидно, защото ако σ е унификатор на две атомарни формули φ и ψ, то всяка субституция, която съвпада със σ върху множеството VAR(φ)∪VAR(ψ), също е унификатор на φ и ψ. Можем разбира се да считаме, че различните унификатори на φ и ψ, които съвпадат върху споменатото множество, не се различават съществено един от друг. Има обаче и случаи, когато между два унификатора на дадена двойка от формули е налице по-съществено различие. Например, ако две атомарни формули съвпадат, то всяка субституция е техен унификатор, независимо от това какви термове съпоставя тя на техните променливи. С оглед на това, което предстои да направим по-нататък, важно е да отбележим следното: ако една субституция σ е унификатор на две дадени атомарни формули φ и ψ, а δ е произволна субституция, то субституцията σδ също е унификатор на φ и ψ. Проверката е съвсем проста: ако имаме равенството φσ = ψσ, то ще имаме и

φ(σδ) = (φσ)δ = (ψσ)δ = ψ(σδ). Нека се условим да наричаме частни случаи на една субституция σ субституциите от вида σδ, където δ е произволна субституция. Тогава можем да изкажем току-що отбелязаното свойство още и по такъв начин: ако една субституция е унификатор на две дадени атомарни формули, то и всеки неин частен случай е техен унификатор.

Една естествена и важна задача е тъй наречената задача за унификация. Тя се състои в това да се познае дали две дадени атомарни формули са унифицируеми и в случай, че са унифицируеми, да се намери техен унификатор. Сега ще извършим известна подготвителна работа и ще опишем някои от елементите на един метод за решаване на задачата за унификация, като пълното му описание ще завършим в следващите въпроси. Въпросният метод по същество е даден от френския логик Жак Ербран (Jacques Herbrand) през 1928 г. и е изложен в параграф 2.4 от гл. 5 на дисертацията му, но доста е известен и друг метод, даден през 1965 г. от Джон А. Робинсън (John Alan Robinson).

Да наречем две атомарни формули еднотипни, ако те представляват един и същ нулместен предикатен символ или пък имат вида π(τ₁,…,τ_n) и π(θ₁,…,θ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n, θ₁, …, θ_n са термове. По аналогичен начин се дефинира и еднотипност за два терма, никой от които не е променлива – достатъчно е в горното условие думата „предикатен“ да се замени с думата „функционален“ (не е зле още в този случай вместо π да се напише например ω). Разбира се, ако две атомарни формули или два терма, които не са променливи, съвпадат, те са еднотипни; освен това отношението еднотипност е симетрично и транзитивно. Очевидно е също, че при прилагане на произволна субституция към една атомарна формула резултатът е атомарна формула, еднотипна с дадената, и аналогично твърдение важи за резултата от прилагане на субституция към терм, който не е променлива. От казаното става ясно, че ако две атомарни формули не са еднотипни, то те не са унифицируеми. Не е вярно обаче, че при еднотипност на две атомарни формули те винаги са унифицируеми. Това се вижда да речем от пример 2, а може да се види и по-просто – например еднотипни, но не унифицируеми са атомарните формули p(a) и p(b), където p е едноместен предикатен символ, а a и b са константи.

Да предположим, че са дадени две произволни атомарни формули φ и ψ и се интересуваме дали те са унифицируеми. Ако φ и ψ не са еднотипни, отговорът на този въпрос е отрицателен. Да предположим сега, че φ и ψ са еднотипни. Една от възможностите за това е φ и ψ да са един и същ нулместен предикатен символ. Тогава те са унифицируеми и всяка субституция е техен унификатор. Другата възможност е да имаме

φ = π(τ₁,…,τ_n), ψ = π(θ₁,…,θ_n), където n е някое положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n, θ₁, …, θ_n са термове. Разбира се, ако φ и ψ са една и съща атомарна формула, те са унифицируеми и всяка субституция е техен унификатор, а в по-интересния случай, когато φ и ψ са различни, поне за едно i измежду числата 1, …, n термовете τ_i и θ_i ще бъдат различни. За произволна субституция σ ще имаме равенствата φσ = π(τ₁σ,…,τ_nσ), ψσ = π(θ₁σ,…,θ_nσ), поради което (благодарение на еднозначния прочит на атомарните формули) σ ще бъде унификатор на φ и ψ точно тогава, когато са изпълнени n-те равенства τ₁σ = θ₁σ, …, τ_nσ = θ_nσ.

За по-удобното записване на това, което ше правим по-нататък, уславяме се при произволен избор на термове τ и θ да наричаме решения на уравнението τ = θ онези субституции σ, за които е изпълнено равенството τσ = θσ (за такива субституции ще казваме още, че удовлетворяват уравнението τ = θ ). Разбира се, ще казваме, че дадена субституция е решение на една система от уравнения от този вид (или че удовлетворява тази система), ако тя е решение на всяко от нейните уравнения. С използване на тази терминология можем казаното преди малко да го преформулираме така: ако n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n, θ₁, …, θ_n са термове, то унификатори на атомарните формули π(τ₁,…,τ_n) и π(θ₁,…,θ_n), са точно онези субституции, които са решения на системата от уравнения

(1) τ₁ = θ₁, …, τ_n = θ_n.
Когато φ и ψ са една и съща атомарна формула, лявата и дясната страна на всяко от уравненията в горната система съвпадат, а разбира се е вярно и обратното. В този случай ще казваме за системата (1), че е тъждествена. И така, ние сведохме по-трудните задачи за търсене на унификатор на две атомарни формули към решаването на нетъждествени системи от уравнения между термове.

Пример 4. На двете атомарни формули от пример 1 унификатори са точно онези субституции, които удовлетворяват системата

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

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

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

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