Субституции. Прилагане на субституция към терм

СУБСТИТУЦИИ. ПРИЛАГАНЕ НА СУБСТИТУЦИЯ КЪМ ТЕРМ

Ще предполагаме, че е дадена една сигнатура Σ. Под субституция в сигнатура Σ ще разбираме функция с дефиниционна област множеството Ξ на всички променливи и със стойности в множеството на термовете в сигнатура Σ (в съгласие с предишно уславяне обикновено ще пропускаме думите "в сигнатура Σ" и ще говорим просто за субституции и за термове). Една субституция σ ще наричаме финитарна, ако равенството σ(ξ)=ξ е нарушено най-много за краен брой променливи ξ. Ако ξ₁, …, ξ_k, където k≥1, са променливи, които при k>1 са две по две различни, а θ₁, …, θ_k са термове, то ще означаваме със знака [ξ₁/θ₁,…,ξ_k/θ_k] финитарната субституция σ, определена по следния начин: σ(ξ₁)=θ₁, …, σ(ξ_k)=θ_k и σ(ξ)=ξ за всяка променлива ξ, различна от ξ₁, …, ξ_k. Финитарната субституция, която преобразува всяка променлива в самата нея, ще наричаме тъждествена субституция и ще означаваме с ι (тя разбира се може да се представи във вида [ξ₁/ξ₁], където ξ₁ е произволно избрана променлива).

Нека σ е дадена субституция. За всеки терм τ дефинираме терм στ, който ще наричаме резултат от прилагане на σ към τ (интуитивно въпросният резултат може да се схваща като получен чрез заместване на променливите в терма τ със съответните им стойности на σ). Дефиницията е индуктивна и се състои от следните точки:
1. Ако ξ е променлива, то σξ = σ(ξ).
2. Ако ω е константа, то σω = ω.
3. Ако n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са термове, то

σω(τ₁,…,τ_n) = ω(στ₁,…,στ_n). Разбира се еднозначността на тази дефиниция се осигурява от еднозначния прочит на термовете.

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

Твърдение 1. За всеки терм τ е в сила равенството ιτ=τ.

Доказателство. Равенството ιτ=τ е очевидно, когато τ е константа или променлива. Да предположим сега, че τ=ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са термове, притежаващи доказваното свойство, т.е. термове, за които са в сила равенствата ιτ₁=τ₁, …, ιτ_n=τ_n. Тогава

ιτ = ω(ιτ₁,…,ιτ_n) = ω(τ₁,…,τ_n) = τ, т.е. термът τ също притежава доказваното свойство. _□

Твърдение 2. Нека σ и σ′ са произволни субституции. Ако τ е произволен терм, то равенството στ=σ′τ е изпълнено точно тогава, когато σ и σ′ съвпадат върху множеството VAR(τ).

Доказателство. Ако τ е променлива, то е очевидно, че равенството στ=σ′τ е равносилно със съвпадането на σ и σ′ върху множеството VAR(τ). Такава равносилност е налице по тривиални причини и в случая, когато τ е константа. Да предположим сега, че τ=ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са такива термове, че при i=1,…,n равенството στ_i=σ′τ_i е равносилно със съвпадането на σ и σ′ върху множеството VAR(τ_i). От равенствата

στ = ω(στ₁,…,στ_n), σ′τ = ω(σ′τ₁,…,σ′τ_n) е ясно, че равенството στ=σ′τ е изпълнено точно тогава, когато са изпълнени равенствата στ_i=σ′τ_i, i=1,…,n. Следователно равенството στ=σ′τ е равносилно със съвпадането на σ и σ′ върху всяко от множествата VAR(τ_i), i=1,…,n, т.е. със съвпадането на σ и σ′ върху обединението на въпросните n множества, което пък е VAR(τ). _□

Следствие. Нека σ е произволна субституция. Ако τ е произволен терм, то равенството στ=τ е изпълнено точно тогава, когато σξ=ξ за всяка променлива ξ от множеството VAR(τ). В частност στ=τ за всеки затворен терм τ.

Доказателство. Прилагаме твърдение 2 при σ′=ι. _□

Твърдение 3. Нека σ е произволна субституция. Тогава за всеки терм τ множеството VAR(στ) е обединение на множествата VAR(σξ), където ξ∈VAR(τ).

Доказателство. Твърдението е тривиално в случая, когато τ е променлива. То разбира се е вярно и в случая, когато τ е константа, защото обединението на празно семейство от множества е празно. Да предположим сега, че τ=ω(τ₁,…,τ_n), където n е положително цяло число, ω е n-местен функционален символ и τ₁, …, τ_n са такива термове, че при i=1,…,n множеството VAR(στ_i) е обединение на множествата VAR(σξ), където ξ∈VAR(τ_i). От равенството στ = ω(στ₁,…,στ_n) получаваме, че VAR(στ) е обединение на множествата VAR(στ₁), …, VAR(στ_n) и следователно VAR(στ) е обединение на множествата VAR(σξ), където ξ принадлежи на обединението на множествата VAR(τ₁), …, VAR(τ_n). Последното обединение обаче е точно VAR(τ). _□

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

Нека σ е субституция в сигнатура Σ, 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) - съответно "старата оценка" и "новата оценка", и да изкажем равенството с думите "стойността на новия терм при старата оценка е равна на стойността на стария терм при новата оценка".

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