ある項が与えられたときに、どのように書き換えたとしてもいつかは正規形に到達するという性質

強正規化する場合は、弱正規化する

項書き換えが必ず停止するって意味やな

単純型付きラムダ計算で言えば、 ref p.181

型を付けられるラムダ抽象から型付けを始めれば、どんな順番でβ簡約を施していっても必ずβ正規形に至る、という性質のこと

逆に言えば、無限のβ簡約を引き起こすラムダ抽象には型を付けることができない

e.g. Ω-コンビネータは自己適用しているので、型を付けられない

定義