Basic Proof Theory 読書記録其の一 - 曇りなき眼で見定めブログ

　Troelstra先生とSchwichtenberg先生*1の"Basic Proof Theory"もまあ必読書なのでしょうな。頑張ります。

　単純型付ラムダ計算の代入補題についてメモ。

　代入は以下のように項の複雑性によって帰納的に定義される。

　 $x[x/s] := s$ ,

　 $y[x/s] := y$ （ $y \equiv x$ でないとき*2）,

　 $(t_1t_2)[x/s] := t_1[x/s]t_2[x/s]$ ,

　 $(\lambda x.t)[x/s] := \lambda x.t$ ,

　 $(\lambda y.t)[x/s] := \lambda y.t[x/s]$ （ $y \equiv x$ でないとき。w.l.o.g.(一般性を失わず) $y \notin$ FV( $s$ )とあるけどこれはα変換すればそうなるようにできるからということだろうか。）

　で、代入補題は以下。

　 $x \equiv y$ でなく $x \notin$ FV( $t_2$ ) ならば

　　 $t[x/t_1][y/t_2] \equiv t[y/t_2][x/t_1[y/t_2]]$ .　 $\Box$

　項の深さに関する帰納法で証明しろとのことである。

　まずは $t$ が変数のときに成立していることを確認する。

　 $t \equiv x$ のときは $t[x/t_1][y/t_2] \equiv t_1[y/t_2]$ かつ $t[y/t_2][x/t_1[y/t_2]] \equiv t[x/t_1[y/t_2]] \equiv t_1[y/t_2]$ なので OK。

　 $t \equiv y$ のときも $t[x/t_1][y/t_2] \equiv t[y/t_2] \equiv t_2$ かつ $t[y/t_2][x/t_1[y/t_2]] \equiv t_2[x/t_1[y/t_2]] \equiv t_2$ なので OK。

　 $t \equiv x$ でも $t \equiv y$ でもないときは代入が起こらないので左辺も右辺も $t$ で OK。

　ということは $t \equiv t_a$ のときと $t \equiv t_b$ のときに代入補題が成り立っていると仮定して $t \equiv (t_at_b)$ のときにも成り立っていれば項が適用の形のときも OK となる。定義より $(t_at_b)[x/t_1][y/t_2] = t_a[x/t_1][y/t_2]t_b[x/t_1][y/t_2]$ で、帰納法の仮定より $t_a[x/t_1][y/t_2]t_b[x/t_1][y/t_2] \equiv t_a[y/t_2][x/t_1[y/t_2]]t_b[y/t_2][x/t_1[y/t_2]]$ だが、これも定義から $(t_at_b)[y/t_2][x/t_1[y/t_2]]$ のことといえるので OK である。