СУБСТИТУЦИИ. ПРИЛАГАНЕ НА СУБСТИТУЦИЯ
КЪМ ТЕРМ, КЪМ БЕЗКВАНТОРНА ФОРМУЛА И КЪМ КОНФИГУРАЦИЯ

    Нека s е дадена субституция. Индуктивно дефинираме кога един терм е резултат от прилагане на s към даден терм (интуитивно въпросният резултат може да се схваща като получен чрез заместване на променливите в терма със съответните им стойности на s). Дефиницията се състои от следните точки:

    РПТ1. Ако x е променлива, то s(x) е резултат от прилагане на s към x.
    РПТ2. Ако w е 0-местен функционален символ, то w е резултат от прилагане на s към w.
    РПТ3. Ако n е положително цяло число, w е n-местен функционален символ, t₁, ..., t_n са термове и термовете t₁ў, ..., t_nў са резултати от прилагане на s съответно към t₁, ..., t_n, то термът w(t₁ў,...,t_nў) е резултат от прилагане на s към терма w(t₁,...,t_n).

    Като се използва еднозначността на синтактичния анализ на термовете, индуктивно се показва, че за всеки терм t съществува точно един терм, който е резултат от прилагане на субстицията s към t. Резултата от прилагането на s към терма t ние ще означаваме с s(t). Точка РПТ1 показва, че в случая, когато t е променлива, това означение не влиза в конфликт с досегашния смисъл на означението s(x). От точки РПТ2 и РПТ3 виждаме съответно, че за всеки 0-местен функционален символ w е в сила равенството s(w)=w и всеки път, когато n е положително цяло число, w е n-местен функционален символ и t₁, ..., t_n са термове, имаме равенството

    РПБФ1. Ако p е 0-местен предикатен символ, p е резултат от прилагане на s към p.
    РПБФ2. Ако n е положително цяло число, p е n-местен предикатен символ, t₁, ..., t_n са термове и термовете t₁ў, ..., t_nў са резултати от прилагане на s съответно към t₁, ..., t_n, то атомарната формула w(t₁ў,...,t_nў) е резултат от прилагане на s към атомарната формула w(t₁,...,t_n).
    РПБФ3. Ако j е безкванторна формула и безкванторната формула jў е резултат от прилагане на s към j, то безкванторната формула Шjў е резултат от прилагане на s към Шj.
    РПБФ4,5. Ако j₁ и j₂ са безкванторни формули, а безкванторните формули j₁ў и j₂ў са резултати от прилагане на s съответно към j₁ и j₂, то безкванторната формула (j₁ў&j₂ў) е резултат от прилагане на s към (j₁&j₂), а безкванторната формула (j₁ўЪj₂ў) е резултат от прилагане на s към (j₁Ъj₂).

    Като се използва еднозначността на синтактичния анализ на формулите, индуктивно се показва, че за всяка безкванторна формула j съществува точно една безкванторна формула, която е резултат от прилагане на s към j. Резултата от прилагането на s към безкванторната формула j ние ще означаваме с s(j) (евентуално ще пропускаме скобите в началото и края на j, ако има такива). Ясно е, че за всеки 0-местен предикатен символ p имаме равенството s(p)=p, при всеки избор на n-местен предикатен символ p, където n>0, и на термове t₁, ..., t_n е в сила равенството

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

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

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

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

    Ще изложим само доказателството на твърдение 3 за случая на термове. Ако q е дадена променлива x₀, то СВО(q)={x₀}, тъй че дясната страна на доказваното равенство се равнява на СВО(s(x₀)), което е и лявата страна. Ако qОW₀, равенствотопак е вярно, защото двете му страни са празни. Нека сега q е терм от вида w(t₁,...,t_n), където n>0, wОW_n и t₁, ..., t_n са такива термове, че са верни равенствата

    Сега ще дефинираме понятие за резултат от прилагане на субституция към конфигурация. Нека са дадени една субституция s и една конфигурация (S,v). Резултат от прилагането на s към (S,v) ще наричаме конфигурацията (S,vў), където оценката vў се дефинира с условието, че
(1)                                                       vў(x)=s(x)^S,v
за коя да е променлива x; този резултат ще означаваме с s(S,v).

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

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

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

    Доказателство. Имаме s(S,v)=(S,vў), където оценката vў се дефинира с помощта на равенството (1). Значи нашата цел ще бъде да докажем, че
(2)                                                       s(q)^S,v=q^S,vў.
Нека S=(C,I). За да докажем равенството (2) в случая, когато q е терм, ще използваме индукция, съобразена с дефиницията на понятието терм. Първо проверяваме верността на равенството в случая, когато q е променлива или нулместен функционален символ. Ако q е някоя променлива x, то равенството (2) добива вида s(x)^S,v=vў(x) и е вярно благодарение на (1), а ако q е някой нулместен функционален символ w, то (2) пак е вярно, защото и двете му страни са очевидно равни на I(w). Нека сега да имаме q=w(t₁,...,t_n), където wОW_n, n>0, t₁, ..., t_n са термове и са изпълнени равенствата s(t_i)^S,v=t_i^S,vў, i=1,...,n. Тогава

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

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

    Лема за запазване на тъждествената вярност при преход от безкванторна формула към неин частен случай. Ако една безкванторна формула j е тъждествено вярна в дадена структура S, то всички частни случаи на j са също тъждествено верни в S.

    Доказателство. Нека j е безкванторна формула, тъждествено вярна в дадена структура S, и нека s е произволна субституция. Ще покажем, че и безкванторната формула s(j) е тъждествено вярна в S. Нека v е произволна оценка в S на променливите. Тогава, използвайки теоремата за стойността на резултата от прилагане на субституция и дефиницията за прилагане на субституция към конфигурация, виждаме, че е в сила равенство от вида s(j)^S,v=j^S,vў, където vў е подходяща оценка в S на променливите. Поради тъждествената вярност на j в S дясната страна на това равенство е 1, следователно и лявата е 1.

    Особено съществена роля в нашите разглеждания ще играят затворените частни случаи. От доказаната лема е ясно, че ако дадена безкванторна формула j е тъждествено вярна в дадена структура, то всички затворени частни случаи на j са верни в тази структура. Обратното твърдение на последното не е вярно без допълнителни предположения. Причина за това, грубо казано, е обстоятелството, че понякога възможностите за образуване на затворени частни случаи са малко или даже липсват.

    Пример 2. Нека е налице само един функционален символ w и той е нулместен. Нека p е едноместен предикатен символ, x е променлива и S=(C,I) е такава структура, че I(p)(I(w))=1, но I(p) приема стойност 0 за някой елемент на C. Тогава атомарната формула p(x) не е тъждествено вярна в S, въпреки че нейният единствен затворен частен случай p(w) е верен в S.

    Ако S=(C,I) е дадена структура, един елемент на C ще наричаме явно представим в S, ако той е стойност в S на някой затворен терм.

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

    В сила е следното твърдение:

    Достатъчно условие за тъждествена вярност при вярност на затворените частни случаи. Нека S=(C,I) е такава структура, че всеки елемент на C е явно представим в S, и нека j е такава безкванторна формула, че всички затворени частни случаи на j са верни в S. Тогава j е тъждествено вярна в S.

    Доказателство. Нека v е произволна оценка в S на променливите. При направените предположения можем да разгледаме субституция s, която на всяка променлива x съпоставя някой затворен терм със стойност v(x) в S. Тогава за всяка оценка w в S на променливите ще имаме равенството s(S,w)=(S,v). Следствието от твърдение 3 показва, че безкванторната формула s(j) е затворена, а теоремата за стойността на резултата от прилагане на субституция заедно с отбелязаното преди малко равенство дава равенството s(j)^S=j^S,v. Тъй като лявата страна на това равенство е 1, дясната също ще бъде 1.

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

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