強正規化
strong normalization
ある項が与えられたときに、どのように書き換えたとしてもいつかは正規形に到達するという性質
強正規化する場合は、弱正規化する
項書き換えが必ず停止するって意味やなmrsekut.icon
単純型付きラムダ計算で言えば、 ref 『C言語による計算の理論』.icon p.181
型を付けられるラムダ抽象から型付けを始めれば、どんな順番でβ簡約を施していっても必ずβ正規形に至る、という性質のこと
逆に言えば、無限のβ簡約を引き起こすラムダ抽象には型を付けることができない
e.g. Ω-コンビネータは自己適用しているので、型を付けられない
定義
https://ja.wikipedia.org/wiki/正規化_(項書き換え)#定義