Субституции

Субституция нарчаме изображение $$\sigma$$ от множеството на промненливите в множеството на всички термове, за което $$\sigma(X) \neq X$$ само за краен брой X. $$\sigma$$ може да се запише по следния начин: [X1/T1,..,Xn/Tn], където X1,...,Xn са всички различни променливи, за които $$\sigma(X_i) = T_i \neq X_i$$. Ако такива променливи няма, т.е $$(\forall X)(\sigma(X) = X)$$ тази субституция наричаме идентитет, бележим я с $$\iota$$ или [X/X] за някоя променлива X. Прилагане на субституция към терм T бележим с $$T\sigma$$ и дефинираме индуктивно:

  • $$c\sigma = c$$
  • $$X\sigma = \sigma(X)$$
  • $$f(T_1,...,T_n)\sigma = f(T_1\sigma,...,T_n\sigma)$$

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

Произведение на субституции

Произведение на субституциите $$\sigma_1$$ и $$\sigma_2$$ наричаме субституцията $$\sigma(X) = (X\sigma_1)\sigma_2$$ и бележим с $$\sigma_1\sigma_2$$. Очевидно $$\iota$$ играе ролята на единичен елемент: $$\sigma\iota = \iota\sigma = \sigma$$. Ако $$\sigma = \rho\tau$$, тогава казваме, че $$\rho$$ е по-обща от $$\sigma$$, а $$\sigma$$ е частен случай на $$\rho$$. Възможно две субституции да са най-общи: например [X/Y] = [X/Z].[Z/Y], [X/Z] = [X/Y].[Y/Z], т.е. са взаимно частни случаи една на друга. За тях казваме, че са варианти.

Унификатори

Казваме, че два терма или атома A1, A2 са унифицируеми (могат да се унифицират), ако има субституция $$\sigma$$, която ги изравнява, т.е. $$A_1\sigma = A_2\sigma$$. $$\sigma$$ наричаме унификатор. Два терма или атома могат да имат много унификатори, които не са варианти един на друг. Когато ПРОЛОГ проверява дали един атом се унифицира с друг в случай на успех, той намира най-икономичния или най-общия унификатор. Ако два терма или атома са унифицируеми, те винаги имат най-общ един унификатор, който не е единствен заради горната забележка (има много варианти).

Системи от равенства на термове

Алгоритъмът за намиране на най-общ унификатор на два атома или терма се свежда до намиране на най-общо решение на системи от уравнения от термове:

T1' = T1''
T2' = T2''
...
Tn' = Tn''.

Казваме, че системата е решена относно променливата X, ако за някое i X = Ti' (X е лявата страна на някое равенство) и не участва в никой друг терм в системата. Казваме, че системата е решена, ако е решена относно всички променливи от лявата страна на равенствата. Това не означава, че от дясната страна не могат да участват други променливи. Казваме, че системата е явно нерешима, ако в някое равенство (което не е тъждество) имаме някой от следните случаи:

  • X = T, където T е терм, в който участва X
  • от двете страни на равенството имаме термове с различни функционални символи
  • от двете страни на равенството имаме различни константи
  • от едната страна на равенството имаме константа, а от другата - функционален символ
  • от двете страни на равенство имаме еднакви функционални символи с различен брой аргументи.

Следните действия запазват еквивалентността на системата от термове:

  1. Премахване на тъждество. Изтриване на уравнение от вида T = T, където T е терм
  2. Обръщане. Замяна на уравнението T1 = T2 с уравнението T2 = T1.
  3. Разпадане. Замяна на уравнението f(T1',T2',...,Tk') = f(T1'',T2'',...,Tk'') с уравненията T1' = T1'', T2' = T2'', ..., Tk' = Tk''.
  4. Заместване. Ако системата не е решена относно някоя променлива X, която участва в единствено равенство от вида X = T, и X не участва в T, тогава заместваме в цялата система X със T.

Последователното прилагане на тези четири действия винаги води до решена или до нерешима система. Нещо повече, ако първоначалните атоми или термове са унифицируеми, решената система ни дава най-общ унификатор, ако те не са унифицируеми, тогава стигаме до нерешима система.

Последно модифициране: събота, 12 ноември 2011, 17:38