Стойност на резултат от прилагане на субституция

СТОЙНОСТ НА РЕЗУЛТАТ ОТ ПРИЛАГАНЕ НА СУБСТИТУЦИЯ

Нека σ е субституция при сигнатура Σ, a S е структура със сигнатура Σ. В множеството на всички оценки в S ще дефинираме едно преобразование, което ще наричаме оператор за присвояване, съответен на σ в S и ще означаваме със σ^S. А именно, ще приемем, че резултатът σ^S(v) от прилагането на това преобразование към произволна оценка v в S е оценката v', за която v'(ξ)=σ(ξ)^S,v при всеки избор на променливата ξ.

Забележка 1. Ако σ = [ξ₁/θ₁], където ξ₁ е дадена променлива, а θ₁ е даден терм, то, както лесно се проверява, σ^S(v) съвпада с модификацията на v върху ξ₁ чрез θ₁^S,v. По-общо, ако σ = [ξ₁/θ₁,…,ξ_k/θ_k], където ξ₁, …, ξ_k са две по две различни променливи, а θ₁, …, θ_k са термове, то е в сила равенството σ^S(v) = v[ξ₁→θ₁^S,v]…[ξ_k→θ_k^S,v].

Забележка 2. Ако един език за програмиране работи с променливи и допуска оператор за присвояване ξ₁:=θ₁, който на дадена променлива ξ₁ приписва стойността на даден израз θ₁ и запазва стойностите на останалите променливи, то действието на този оператор за присвояване би било аналогично на действието на преобразованието σ^S от първото изречение на забележка 1.

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

Теорема за стойността на резултат от прилагане на субституция към терм. Ako S е структура със сигнатура Σ, то за всяка субституция σ и всеки терм τ при тази сигнатура е в сила равенството

(στ)^S,v = τ^{S,σ^S(v)}.

Доказателство. Нека са дадени структура S, оценка v в нея и субституция σ. Да означим с v' оценката σ^S(v). Имаме да докажем, че за всеки терм τ е в сила равенството (στ)^S,v = τ^S,v'. Ако термът τ е променлива, верността на това равенство произтича от дефиницията на оценката v', а ако той е константа, то равенството е тривиално. Да предположим сега, че τ = ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са такива термове, че при i=1,…,n е в сила равенството (στ_i)^S,v = τ_i^S,v'. Тогава

(στ)^S,v = ω(στ₁,…,στ_n)^S,v = ω^S((στ₁)^S,v,…,(στ_n)^S,v) = ω^S(τ₁^S,v',…,τ_n^S,v') = τ^S,v'. _□

Забележка 3. За запомняне на равенството от доказаната теорема може да се използва следният мнемоничен похват: да наречем термовете τ и στ съответно „старият терм“ и „новият терм“, а оценките v и σ^S(v) – съответно „старата оценка“ и „новата оценка“, след което да изкажем равенството с думите „стойността на новия терм при старата оценка е равна на стойността на стария терм при новата оценка“.

С помощта на тази теорема се получава неин аналог за прилагане на субституция към атомарна формула:

Теорема за стойността на резултат от прилагане на субституция към атомарна формула. Ako S е структура със сигнатура Σ, то за всяка субституция σ и всяка атомарна формула φ в тази сигнатура е в сила равенството

(σφ)^S,v = φ^{S,σ^S(v)}.

Доказателство. Нека са дадени структура S, оценка v в нея и субституция σ. Да означим с v' оценката σ^S(v). Имаме да докажем, че за всяка атомарна формула φ е в сила равенството (σφ)^S,v=φ^S,v'. Ако φ е нулместен предикатен символ, то равенството е тривиално. Да предположим сега, че φ = π(τ₁,…,τ_n), където n е положително цяло число, π е n-местен предикатен символ и τ₁, …, τ_n са термове. Тогава

(σφ)^S,v = π(στ₁,…,στ_n)^S,v = π^S((στ₁)^S,v,…,(στ_n)^S,v) = π^S(τ₁^S,v',…,τ_n^S,v') = φ^S,v'. _□

Разбира се, мнемоничният похват, описан в забележка 3, може да бъде разпространен и за случая, разглеждан в горната теорема, както и за по-общия случаи, който предстои да разгледаме. Въпросният по-общ случай е следният.

Теорема за стойността на резултат от прилагане на субституция към формула. Нека S е дадена структура. За всяка формула φ, всяка субституция σ, приложима към φ, и всяка оценка v в S на променливите имаме равенството

(σφ)^S,v = φ^{S,σ^S(v)}. Доказателство. Ще използваме индукция по построението на формулата φ. Твърдението е вярно в случаите, когато φ е атомарна формула, и разсъжденията за случаите на отрицание, конюнкция и дизюнкция от индуктивната стъпка са прости. Ще разгледаме подробно само случая на поставяне на квантор. Ще се ограничим с разглеждането за квантор за общност, защото за квантор за съществуване то е аналогично. Нека χ е σ∀ξφ за дадена субституция σ, дадена променлива ξ и дадена формула φ, притежаваща доказваното свойство, и нека v е оценка в S. Да означим с v' оценката σ^S(v). Ще покажем, че χ^S,v = (∀ξφ)^S,v', т.е. че χ^S,v е най-малката от стойностите на φ^S,v'[ξ→d] при изменението на d в носителя на S. Това, че χ е σ∀ξφ, означава, че субституцията σ_ξ/ξ е приложима към формулата φ и имаме равенството χ = ∀ξσ_ξ/ξφ, като при това ξ не принадлежи на VAR(ση) за никоя свободна променлива η на φ, различна от ξ. При това положение χ^S,v е най-малката от стойностите на (σ_ξ/ξφ)^S,v[ξ→d] при изменението на d в носителя на S. От направеното индуктивно предположение за φ получаваме, че (σ_ξ/ξφ)^S,v[ξ→d] = φ^{S,σ^S(v[ξ→d])}, където σ = σ_ξ/ξ. Нашата цел ще бъде постигната, ако се убедим, че за всяко d от носителя на S оценките σ^S(v[ξ→d]) и v'[ξ→d] съвпадат в множеството FVAR(φ). Нека d е произволен елемент на носителя на S. Двете оценки съвпадат за променливата ξ, защото стойността на първата от оценките за ξ е (σξ)^S,v[ξ→d] = d, колкото е и стойността на втората. Ако пък η е произволна свободна променлива на φ, различна от ξ, то стойността на първата от оценките за η е (ση)^S,v[ξ→d] = (ση)^S,v[ξ→d], докато стойността на втората за η е v'(η) = (ση)^S,v. Имаме обаче равенството (ση)^S,v[ξ→d] = (ση)^S,v, понеже оценките v[ξ→d] и v съвпадат върху множеството VAR(ση). _□

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