与えられたラムダ抽象が、正規形を持つならば、正規順序で簡約を繰り返すと正規形が得られる

効率の良し悪しはわからないが、とりあえず必ず正規形に辿り着ける

例

正規形を持たないもの: \Omega\Omega

正規形を持たないので、正規化定理はそもそも適用できない

ref Ω-コンビネータ

適切な順序で簡約しないとループするもの

(\lambda uw.w)\Omega I

これを最左最外簡約で簡約すれば正規形に辿り着ける