代入 (Substitution)

代入/置換 (substitution)

[定義] 代入 (substitution) 代入とは次のような形式の有限集合である．

{t₁/v₁, ・・・, t_n/v_n}

ただし，v_i は変数, t_i は v_i と異なる項で，各要素の "/" の右側に現れる変数は全て異なる．
代入が空集合であるとき，空の代入 (empty substitution)とよび，ε と表記する．

[定義] 例 (instance) 代入 θ = {t₁/v₁, ・・・, t_n/v_n} と基本論理式 E に対して，E における変数 v_i (1 ≦ i ≦ n)の各出現を t_i で置き換えたものを Eθ と表記し，E の例 (instance) とよぶ．

(例)
θ = {f(a)/x, g(b)/y}, E = P(x, y, f(y)) のとき，Eθを求めよ．

θ = {f(y)/x, g(b)/y}, E = P(x, y, f(y)) のとき，Eθを求めよ．

[定義] 代入の合成(composition) 代入

θ = {t₁/x₁, ・・・, t_n/x_n}

と，代入

λ = {u₁/y₁, ・・・, u_m/y_m}

に対して，θ と λ の合成(composition) θ○λ を次のように定義する．

{t₁λ/x₁, ・・・, t_nλ/x_n, ・・・, u₁/y₁, ・・・, u_m/y_m} から t_jλ = x_j なる t_jλ/x_j と y_i ∈ {x₁, ・・・, x_n} なる u_i/y_i を除いたもの．

(例)
θ = {y/x, f(y)/z}, λ = {a/x, b/y} のとき θ○λ を求めよ．