Subject Reductionに関する練習問題
まだこのブログでこの話をしていなかった（ような気がする）ことにふと気づいたので、ありがちなクイズ。
任意の型環境Γにおいて、任意のλ式Mに対して、任意の型Tを与えることのできるような型つけ規則∀Γ.∀M.∀T. Γ├ M : Tを考える。
- この型つけ規則の下で、Subject Reduction (├ M : T ∧ M → N ⇒├ N : T)は成り立つか？
- この型つけ規則は健全といえるか？
追記：酷い書き間違いを直した。
追記の追記：直ってなかったし。もうグダグダ。
解説のようなもの：http://d.hatena.ne.jp/yoriyuki/20060808#c1156214112
