Нека s е дадена субституция. Като използваме еднозначното прочитане на термовете, можем да дефинираме индуктивно едно изображение d на Hў в Hў по следния начин:
        а) d(X)=s(X)за всяка променлива X;
        б) d(c)=c за всяка константа c;
        в) d(f(T₁,T₂...,T_n))=f(d(T₁),d(T₂)...,d(T_n)) при n>0, fОF_n,T₁,T₂,..., T_n О Hў.
За произволен терм T съответния му терм d(T) ще наричаме резултат от прилагане на s към T (интуитивно въпросният резултат може да се схваща като получен чрез заместване на променливите в T със съответните им стойности на s). Благодарение на точка а) от дефиницията на изображението d то е продължение на изображението s. Това позволява без опасност от недоразумение в бъдеще да означаваме терма d(T) със s(T). При такъв начин на означаване равенствата от точки б) и в) от същата дефиниция добиват съответно вида s(c)=c и вида

    След като вече дефинирахме какво разбираме под резултат от прилагане на дадена субституция s към произволен терм, лесно се дефинира и резултат от прилагане на s към произволна атомарна формула, като този резултат е пак атомарна формула. Дефиницията е следната: когато pОP₀, приемаме, че резултатът от прилагането на s към p е p, а когато n е положително цяло число, pОP_n и T₁, Т₂,..., Т_n са термове, за  резултат от прилагането на s към p(T₁,Т₂...,Т_n) считаме атомарната формула p(s(T₁),s(T₂)...,s(T_n)) (дефиницията е коректна благодарение на еднозначното прочитане на атомарните формули). Да отбележим, че ако се случи една атомарна формула да бъде същевременно и терм (вж. забележка 3 от въпроса "Сигнатури, структури, термове, атомарни формули"), то току-що дадената дефиниция ще даде същия резултат, какъвто би дала в случая и дефиницията за прилагане на субституция към терм. Благодарение на това ние без опасност от недоразумение ще означаваме резултата от прилагането на s към произволна атомарна формула A със s(A). Като използваме това означение, можем да запишем, че s(p)=p за всеки нулместен предикатен символ p и имаме равенството

    Нека s е субституция, а G е дадена цел. Резултат от прилагането на s към G ще наричаме целта, която се получава от G чрез прилагане на s поотделно към членовете на G. Ще означаваме този резултат със s(G). Най-сетне, ако е дадена една клауза C с глава H и тяло B, то резултат от прилагането на s към C ще наричаме клаузата с глава s(H) и тяло s(B); ще я означаваме със s(C).

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

     Твърдение 1. Ако E е терм, атомарна формула, цел или клауза и две субституции съвпадат върху множеството на променливите на E, то резултатите от прилагането на тези субституции към E също съвпадат.

     Твърдение 2. Ако E е терм, атомарна формула, цел или клауза, то е в сила равенството [=:](E)=E.

     Следствие от твърдения 1 и 2. Ако E е затворен терм, затворена атомарна формула, затворена цел или затворена клауза, то за всяка субституция s е в сила равенството s(E)=E.

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

     Твърдение 3. Ако E е терм, атомарна формула, цел или клауза, то за всяка субституция s е изпълнено равенството

    Следствие. Ако E е терм, атомарна формула, цел или клауза, а s е субституция, то резултатът s(E) е затворен точно тогава, когато термът s(X) е затворен за всяка  променлива X на E.

     Ще изложим само доказателството на твърдение 3 за случая на термове. Ако E е дадена променлива X₀, то VAR(E)={X₀}, тъй че дясната страна на доказваното равенство се равнява на VAR(s(X₀)), което е и лявата страна. Ако EОF₀, равенството пак е вярно, защото двете му страни са празни. Нека сега E е терм от вида f(T₁,T₂...,T_n), където n>0,  fОF_n и T₁, T₂, ...,T_n са такива термове, че са верни равенствата

    Да предположим сега, че са дадени една субституция s и една структура S. Ще дефинираме едно преобразование s_S, което преобразува всяка оценка в S на променливите пак в такава оценка. Дефиницията на това преобразование е следната: ако v е произволна оценка в S на променливите, то s_S(v)=vў, където оценката vў се дефинира с условието, че

     Пример. Нека субституцията s има вида [T₀=:X₀], където T₀ и X₀ са съответно даден терм и дадена променлива. Ако приложим преобразованието s_S към дадена оценка v в S на променливите, ще получим нова оценка vў, такава, че  vў(X₀)=T₀^S,v и vў(X)=v(X) за всяка променлива X, различна от X₀. Това показва, че ако в някой език за програмиране могат да се пишат програми с променливи, приемащи стойности в S, и в този език е допустим операторът за присвояване X₀:=T₀, то преобразованието s_S действа върху  оценките на променливите по същия начин както въпросния оператор.

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

     Теорема за стойността на резултата от прилагане на субституция към терм. Нека са дадени една субституция s,  една структура  S и една оценка v в S. Нека s_S(v)=vў. Тогава за всеки терм T е в сила равенството s(T)^S,v=T^S,vў.

     Доказателство. Ще използваме индукция, съобразена с дефиницията на понятието терм. Първо проверяваме верността на равенството в случая, когато T е променлива или нулместен функционален символ. Ако T е някоя променлива X, то равенството, което имаме да докажем, добива вида s(X)^S,v=vў(X) и е вярно благодарение на равенството s_S(v)=vў и дефиницията на преобразованието  s_S.  Ако T е някой нулместен функционален символ c, то доказваното равенство пак е вярно, защото и двете му страни са равни на стойността в S на затворения терм c. Нека сега да имаме T=f(T₁,T₂...,T_n), където n>0, fОF_n,T₁,T₂,..., T_n  са термове и са изпълнени равенствата s(T_i)^S,v=T_i^S,vў,i=1,...,n. Тогава, означавайки с f^S n-местната операция, чрез която се интерпретира f в S, ще имаме веригата от равенства

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

    Необходимо и достатъчно условие за вярност на резултата от прилагане на субституция към атомарна формула. Нека са дадени една субституция s,  една структура S и една оценка v в S. Нека s_S(v)=vў. Тогава за всяка атомарна формула A условието S,vs(A) е равносилно с условието S,vўA.

    Доказателство. Ако A е нулместен предикатен символ, то и двете написани условия са равносилни с верността в S на затворената формула A, следователно те са равносилни и помежду си. Нека сега  A=p(T₁,Т₂...,Т_n), където n>0, pОP_n и T₁, Т₂,..., Т_n са термове. Тогава, означавайки с p^S n-местния предикат, чрез който се интерпретира p в S, ще имаме веригата от равносилности

S,vs(A) Ы S,vp(s(T₁),s(T₂)...,s(T_n)) Ы p^S(s(T₁)^S,v,s(T₂)^S,v,...,s(T_n)^S,v)=1 Ы p^S(T₁^S,vў,T₂^S,vў,...,T_n^S,vў)=1Ы S,vўA.  _ї

    Следствие. При предположенията и означенията от горната теорема, ако G е произволна цел, то за да бъде изпълнена целта s(G) в S при оценката v, необходимо и достатъчно е целта G да бъде изпълнена в S при оценката vў.

    Забележка 2. В случая, когато субституцията s има вида от разгледания преди малко пример, установеното необходимо и достатъчно условие за вярност на резултата от прилагане на s към атомарна формула може да се разглежда като  възможна формулировка на едно известно твърдение на Антъни Хоар (Charles Antony Richard Hoare). Въпросното твърдение е полезно при доказване на коректност на програми, съдържащи оператори за присвояване. Според него, за да бъде удовлетворено дадено условие след изпълнението на оператора за присвояване X₀:=T₀, необходимо и достатъчно е преди изпълнението на този оператор да е удовлетворено същото условие с X₀, заместено с T₀.
 

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

Previous  Next  Contents