最近TaPLを読んでいるのだけれど、いかんせん構造的帰納法に不慣れなもので、導出に関する帰納法による証明を読んだり書いたりしているうちに
- 自分が何をしているのか
- 何を示すことで命題を証明しようとしているのか
- そもそも項に関する帰納法と導出に関する帰納法って何が違うんだっけ???
が分からなくなることがあった。
分かってしまった今となっては何でこんなことが分からなかったのか分からないけど、恥をしのんで自分の理解をメモしておく。メモしておかないとどうせ後でまた混乱し始めると思う。
項に関する構造的帰納法
これはTaPL3章の定理3.3.4にある通り
各項 s に対して、s の任意の直接の部分項 r に対して P (r) が成り立つとき、P (s) が証明できる
ならば、すべての s に対して P (s) が成り立つ。
つまり項 $t_1$ ... $t_n$ があって、それらの各項について $P(t_1)$ ... $ P(t_n) $ が成り立つとき、$t_1$ ... $t_n$ を直接の部分項として持つ項 $s$ について $P(s)$ が成り立つ。
例えば、TaPL 第8章の、定理8.2.4の型の一意性 (t: R1 かつ t: R2 ならば R1 = R2)
ある項のsの任意の直接の部分項rに対して、型の一意性が成り立つことを帰納法の仮定と置いて、そのとき項sについて型の一意性が成り立つことを(inversion lemmaを使いつつ)示し、それにより定理を証明している。
一方、定理8.3.2の進行定理の証明では、項に関する帰納法ではなく、t: T の導出に関する帰納法により定理を証明する。
項に関する帰納法が直接の部分項に着目するのに対し、導出に関する帰納法では導出木の直接の部分木(に現れる項と型の2つ組)に着目する。
各項と型の関係 s: S に対して、s: S の任意の直接の(導出木の)部分木に現れる2つ組 r: R に対して P(r: R) が成り立つとき、P(s: S) が証明できる
ならば、すべての s: S に対して P(s: S)が成り立つ
こういう感じか???
進行定理の証明では、導出木の根を導出するのに直接使われた導出規則について場合分けを行い、それぞれの場合について導出に関する帰納法を用いて定理を証明する。
例えば T-IF の場合、つまり t = if t1 then t2 else t3 (で t: T) の場合、まずinversion lemma より
がわかる。ここで帰納法の仮定より、t1 は値である。もしくは t1' が存在して t1 -> t1' となる。
ここで何を示すべきかを思い出してみると、上に書いた帰納法の仮定の下で、命題: t = it t1 then t2 else t3 自体に t が値である or t' が存在して t -> t' であることを示せればよいのであった。
あとはt1が値である場合と、t1が評価される、どちらの場合でも t について命題が成り立つことを示せれば良い。
- t1 が値ならば canonical formよりt1はtrue か false
- true なら E-IFTRUE により
if true then t2 else t3 -> t2 だし
- false なら E-IFFALSE にょり
if false then t2 else t3 -> t3
t1 -> t1'なら E-IF より if t1 then t2 else t3 -> if t1' then t2 else t3
よって、どちらの場合でも t' が存在して t -> t' となることが分かる。
といった具合である。
分かってしまえば何てことはないのだけれど、ここを分かったフリしたまま進んでしまうと多分何も分からないで死んでたので分かってよかったですね。
