α同値 - oupoの日記

次の(本には証明の書かれていない)定理の証明が存外手間がかかったので記しておきます。

補助定理1.2.32(2) (の⇒の部分)
V(λxy.MN)に属さない任意の変数zに対してλx.M ≡α λy.N ⇒ [z/x]M ≡α [z/y]N

この定理は次の定理と同値であることがすぐわかるのでそれを証明します

V(λxy.MN)に属さない任意の変数v,uに対して[v/x]M ≡α [v/y]N ⇒ [u/x]M ≡α [u/y]N

既知とする定理

以下の定理を既知とします。

補助定理1.2.29(4): y, zがV(M)に属さない ⇒ [z/y][y/x]M ≡ [z/x]M
補助定理1.2.34(1): M ≡α N ⇒ FV(M) = FV(N)
代入操作の交換可能性: [y'/y][x'/x]M ≡ [x'/x][y'/y]M (ただしx ≠ yであり、x', y'はV(λxy.M)に属さない変数)

補助定理1.2.34(1)を使うのは循環論法なのではないかと思うかもしれませんが、大丈夫です。
この定理の証明には今回の目的の定理は必要なく
　　λx.M ≡α λy.N ⇒ あるV(λxy.MN)に属さない変数zが存在して[z/x]M ≡α [z/y]N
さえあれば十分で、これはすぐに証明できます。（目的の定理との違いは、任意ではなく存在になっているところ）

代入操作の交換可能性はMの長さに関する帰納法でなんのひねりもなく証明できます。

証明

V(λxy.MN)に属さない任意の変数v,uに対して[v/x]M ≡α [v/y]N ⇒ [u/x]M ≡α [u/y]N

を証明する。

[v/x]M ≡α [v/y]N を示す証明図の長さに関する帰納法で証明する。

証明図の長さが1のとき:

このとき[v/x]M ≡ [v/y]Nである。
よって[u/v][v/x]M ≡ [u/v][v/y]Nである。
ここで補助定理1.2.29(4)より[u/x]M ≡ [u/y]N となり成立する。

証明図の最後の推論がτのとき:

M ≡ (M_1 M_2), N ≡ (N_1 N_2) と表せる。
証明図は以下の形をしている。

$\frac{[v/x]M_1 = [v/y]N_1 \qquad [v/x]M_2 = [v/y]N_2}{[v/x]M = [v/y]N} (\tau)$

ここで帰納法の仮定から
　　[u/x]M_1 ≡α [u/y]N_1, [u/x]M_2 ≡α [u/y]N_2
となり、推論規則τより
　　[u/x]M ≡ [u/y]N
が得られる。

証明図の最後の推論がαのとき:

M ≡ λs.Q, N ≡ λt.Rと表せる。
Mにxが自由に出現しない場合を考える。このとき[v/x]Mにvは自由に出現しないから、「補助定理1.2.34(1): M ≡α N ⇒ FV(M) = FV(N)」より[v/y]Nにもvは自由に出現しない。よってNにyは自由に出現しない。すると[v/x]M ≡ M ≡ [u/x]M, [v/y]N ≡ N ≡ [u/y]N となるから、[u/x]M ≡α [u/y]N が成立する。

次にMにxが自由に出現する場合を考える。このとき先ほどと同様の議論からNにyが自由に出現する。
s ≡ xと仮定すると明らかにMにxが自由に出現しなくなるからs ≠ x。同様にt ≠ y。

証明図は以下の形をしている。

$\frac{[w/s][v/x]Q = [w/t][v/y]R}{\lambda s. [v/x] Q = \lambda t. [v/y]R}(\alpha)$

帰納法の仮定からwはV(λvustxy.QR)に属さないものにできる。
ここで代入操作の交換可能性より[w/s][v/x]Q ≡ [v/x][w/s]Q, [w/t][v/y]R ≡ [v/y][w/t]Rであるから、
　　[v/x][w/s]Q ≡α [v/y][w/t]R
となる。
さらに帰納法の仮定から
　　[u/x][w/s]Q ≡α [u/y][w/t]R
となり、再び代入操作の交換可能性より
　　[w/s][u/x]Q ≡α [w/t][u/y]R
となる。
よって推論規則αより λs.[u/x]Q ≡α λt.[u/y]R すなわち [u/x]M ≡α [u/y]M となる。

□