TaPL輪講/12章
正規化
12.1.1 演習
正規化の証明をwell-typedな項の大きさに関する帰納法でしようとしたらどこでつまずくか?
→applicationで項の大きさが大きくなる場合がある
12.1.2 定義
型Tの閉じた項の集合R_T
$ R_A(t) iff tは停止する
$ R_{T_1 \rightarrow T_2}(t) iff
tは停止する かつ
$ R_{T_1}(s) ならば常に $ R_{T_2}(t\ s)
Rによって所望の強くなった帰納法の仮定が得られる
つまり全てのbase typeの閉じた項は停止する
しかしbase typeの閉じた項は関数型のsubtermを含みうる
なのでそれらについても知る必要がある
定義12.1.2は論理関係の証明技法を特徴づけている
全ての型Aの閉じた項に関する性質Pを示したいならば、型Aに関する帰納法をまわす
型によってindexedな述語の族を定義する
12.1.3 補題
$ R_T(t) ならばtは停止する
Rの定義からすぐわかるらしい
次にRに入るのが簡約しても保たれることを示そう
12.1.4 補題
t : T かつ t -> t' ならば $ R_T(t) \iff R_T(t')
(証明)
型Tの構造に関する帰納法
tが停止する iff t'が停止する は明らか(そうなの?)