α同値その2

補助定理1.2.34(3)
任意のラムダ項Mに対して次のようなラムダ項Nが存在する

M ≡α N かつ FN(N) ∩ BV(N) = ∅

以下の二つの命題と本の中の補助定理1.2.34(3)よりも前に登場する定理を既知とする。

• 主張A: BV([y/x]M) = BM(M) (y ∉ BV(M))
• 主張B: [z/y][y/x]M ≡ [z/x]M (y ∉ V(M), z ∉ BV(M))

証明の都合上、条件を少し強めた次の命題を証明する

任意のラムダ項Mと変数の有限集合Aに対して次のようなラムダ項Nが存在する

M ≡α N かつ BV(N) ∩ (FV(N) ∪ A) = ∅

証明

Mの長さについての帰納法で証明する。

Mの長さが1のとき

このときBV(M) = ∅だからN ≡ Mとおけばいい。

M ≡ M_1 M_2 のとき

帰納法の仮定から

M_1 ≡α N_1 かつ BV(N_1) ∩ (FV(N_1) ∪ FV(M_2) ∪ A) = ∅
M_2 ≡α N_2 かつ BV(N_2) ∩ (FV(N_2) ∪ FV(M_1) ∪ A) = ∅
となるN_1, N_2がある。
ここでN ≡ N_1 N_2とおくと上記のN_1, N_2の満たす条件と次の事実:

• BV(N) = BV(N_1) ∪ BV(N_2), FV(N) = FV(N_1) ∪ FV(N_2)
• FV(M_1) = FV(N_1), FV(M_2) = FV(N_2)

から

BV(N) ∩ (FV(N) ∪ A) = ∅
が従う。
また、M ≡α NだからNは求めている条件を満足する。

M ≡ λx.Qのとき

V(M) ∪ Aに属さない異なる二つの変数y, zをとる。
帰納法の仮定から

[z/x]Q ≡α R' かつ BV(R') ∩ (FV(R') ∪ {y,z} ∪ A) = ∅
となるR'がある。
ここでR ≡ [y/z]R'とおく。
y ∉ BV(R')よりBV(R) = BV(R')である。(主張Aから)
また、y ∉ B(R'), z ∉ BV(R')だから主張Bより[z/y][y/z]R' ≡ [z/z]R'、よってR' ≡ [z/y]Rとなる。
FV(R)はFV(R')か(FV(R') - {z})∪{y}に等しいがどちらの場合も
FV(R) ∪ {y, z} = FV(R') ∪ {y, z}
が成り立つ。

よって

BV(R') ∩ (FV(R') ∪ {y,z} ∪ A) = ∅
より
BV(R) ∩ (FV(R) ∪ {y,z} ∪ A) = ∅
したがって
BV(R) ∩ ((FV(R) - {y}) ∪ A) = ∅
これとy ∉ (FV(R) - {y}) ∪ Aより
(BV(R) ∪ {y}) ∩ ((FV(R) - {y}) ∪ A) = ∅
つまり
(BV(λy. R) ∩ ((FV(λy. R)) ∪ A) = ∅
となる。

ここで[z/x]Q ≡α R', R' ≡ [z/y]Rより

[z/x]Q ≡α [z/y]R
であり、z ∉ V((λx. Q)(λy. R))を満たすから
λx. Q ≡α λy. R
となる。
λy. Rが求める条件を満足するNである。

□

ちょっと大掛かり気味な感じがする…。