# Types and Programming Languages/演習 8.2.3/答案

## 演習 8.2.3.
正しく型付けされた項のすべての部分項は､正しく型付けされていることを証明せよ｡

## 【証明】

「項」は`true | false | 0 | if t then t else t | succ t | pred t | iszero t`の高々7つしか存在しないので、全ての項に対して正しく型付けした場合に部分項の型を決定できるかどうかを調べる。

(1) T-True のとき
(2) T-False のとき
(4) T-Zero のとき
(5) T-Succ のとき
(6) T-Pred のとき
(7) T-IsZero のとき
項 = 部分項なので自明(?)

(3) T-If のとき
`if t_1 then t_2 else t_3: R`のとき`t_1: Bool``t_2: R``t_3: R`に型付けすることができる