СЕМАНТИЧЕН ЕФЕКТ НА ЗАМЕСТВАНЕТО НА ПРОМЕНЛИВА В ТЕРМ
Нека са дадени една променлива x0, един терм t0 и една структура S. Да разгледаме следното преобразуване на оценки в S на променливите: ако v е произволна такава оценка, тя се преобразува в оценката v[x0:t0S,v], т.е. в онази оценка, която на променливата x0 съпоставя t0S,v, а за всички останали променливи съвпада с v. Това преобразуване ще наричаме остойностяване на x0 в S чрез t0 или още оператор за присвояване в S, съответен на заместването на x0 с t0. Въпросното преобразуване на оценки ще означаваме с [x0:=t0]S. Резултата v[x0:t0S,v] от прилагането му към дадена оценка v ще означаваме с v[x0:=t0]S.
Забележка 1. Току-що разгледаното преобразоване на оценки е аналогично на действието на оператор за присвояване в смисъл на програмирането. Програма, в която се използват такива оператори, има определен брой променливи и кое да е текущо състояние на нейното изпълнение може да бъде сравнено с оценка на променливите, защото се характеризира чрез стойностите им при това състояние. Когато при дадено текущо състояние на изпълнението бъде изпълнен някой оператор за присвояване x0:=t0 (където x0 е променлива на програмата, а t0 е някакъв израз), резултатът е преобразуване на текущото състояние по начин, аналогичен на разгледания по-горе. А именно всички променливи с изключение на променливата x0 запазват стойностите си, докато тя пък придобива като нова стойност стойността, която е имал изразът t0 при даденото текущо състояние.
Следното твърдение посочва една съществена връзка на въведеното преобразуване със заместването на променлива в терм.
Теорема за семантичния ефект на заместването на променлива в терм. Нека са дадени една променлива x0, един терм t0 и една структура S. Тогава за всеки терм t и всяка оценка v в S на променливите е в сила равенството
([x0/t0]t)S,v = tS,v[x0:=t0]S.
Доказателство. Използуваме индукция относно построението на терма t. Ако той е някоя константа a, равенството от заключението на теоремата е вярно, защото и двете му страни са равни на aS. Ako t е променливата x0, те и двете са равни на t0S,v, а ако е някоя друга променлива x, и двете страни са равни на v(x). От друга страна не е трудно да се провери, че равенството ще бъде вярно и ако t има вида f(t1,...,tn) за някой n-местен функционален символ f и някои термове t1, ..., tn, за които са в сила равенствата
([x0/t0]ti)S,v = tiS,v[x0:=t0]S, i = 1, ..., n.
Забележка 2. Ако при предположенията на доказаната теорема наречем термовете t и
[x0/t0]t и оценките v и v[x0:=t0]S съответно стария терм, новия терм, старата оценка и новата оценка, то, пропускайки споменаването на структурата S, можем да изкажем равенството от заключението на теоремата по следния начин: стойността на новия терм при старата оценка е равна на стойността на стария терм при новата оценка.
Последно изменение: 6.11.2002 г.