ОПЕРАТОРИ ЗА ПРИСВОЯВАНЕ, СЪОТВЕТНИ НА СУБСТИТУЦИЯ
Да предположим, че са дадени една субституция s и една структура S. Ще дефинираме едно преобразование sS, което преобразува всяка оценка в S на променливите пак в такава оценка. Дефиницията на това преобразование е следната: ако v е произволна оценка в S на променливите, то sS(v)=vў, където оценката vў се дефинира с условието, че
vў(X) = (Xs)S,v
за коя да е променлива X. Преобразованието sS ще наричаме оператор за присвояване в S, съответен на s.
Пример. Нека субституцията s има вида [X0/T0], където
X0 и T0 са съответно даден терм и дадена променлива. Ако приложим преобразованието sS към дадена оценка v в S на променливите, ще получим нова оценка vў, такава, че vў(X0)=T0S,v и vў(X)=v(X) за всяка променлива X, различна от X0. Това показва, че ако в някой език за програмиране могат да се пишат програми с променливи, приемащи стойности в S, и в този език е допустим операторът за присвояване X0:=T0, то преобразованието sS действа върху оценките на променливите по същия начин както въпросният оператор.
Сега ще докажем една теорема, която установява връзка между прилагането на субституция към терм или атомарна формула от една страна и преобразуването на оценки чрез съответния оператор за присвояване от друга.
Теорема за стойността на резултата от прилагане
на субституция към терм или атомарна формула. Нека са дадени една субституция s, една структура S и една оценка v в S. Нека sS(v)=vў и нека E е терм или атомарна формула. Тогава е в сила равенството (Es)S,v=ES,vў.
Доказателство. За да докажем твърдението за случая, когато E е терм, ще използваме индукция, съобразена с дефиницията на понятието терм. Първо проверяваме верността на равенството в случая, когато E е променлива или константа. Ако E е някоя променлива X, то равенството,
което имаме да докажем, добива вида (Xs)S,v=vў(X)
и е вярно благодарение на равенството sS(v)=vў и дефиницията на преобразованието sS. Ако E е някоя константа, то доказваното равенство пак е вярно, защото и двете му страни са равни на интерпретиращия тази константа елемент на носителя на S. Нека сега да имаме E=f(E1,E2...,En),
където n>0, fОFn, E1, E2, ..., En са термове и са изпълнени равенствата
(Eis)S,v=EiS,vў, i=1,...,n. Тогава, означавайки с fS функцията, чрез която се интерпретира f в S, ще имаме веригата от равенства
(Es)S,v = f(E1s,E2s...,Ens)S,v = fS((E1s)S,v,(E2s)S,v,...,(Ens)S,v) =
fS(E1S,vў,E2S,vў,...,EnS,vў) = ES,vў.
Веднаж доказано за термове, твърдението се проверява и за атомарни формули с помощта на аналогични пресмятания. ї
Забележка. В случая, когато субституцията
s има вида от разгледания преди малко пример, изказаното в теоремата твърдение за случая на прилагане на s
към атомарна формула може да се разглежда като възможна формулировка
на едно известно твърдение на Антъни
Хоар (Charles Antony Richard Hoare). Въпросното твърдение е полезно
при доказване на коректност на програми, съдържащи оператори за присвояване.
Според него, за да бъде удовлетворено дадено условие след изпълнението
на оператора за присвояване X0:=T0,
необходимо и достатъчно е преди изпълнението на този оператор да е удовлетворено
същото условие с X0, заместено с T0.
Последно изменение: 13.02.2003 г.