generated at
最左簡約定理

定理
Mβ正規形を持つならば、M最左最外簡約のみを複数回施せば、必ずβ正規形に至る


証明
Mβ正規形を持つ」と「簡約順番の標準化定理」を用いると、
M_1\xrightarrow{n_1}_\beta M_2\xrightarrow{n_2}_\beta\cdots\xrightarrow{n_k}_\beta Nとなる
ここで、Nは正規形なので、n_k=1となるはずである
N\lambdaを一つしか持っていないので。
すると、n_1=n_2=\cdots=n_k=1であることになり、これは最左簡約だけからなる簡約過程である


何が嬉しい?
β正規形を持つなら、この順番で簡約すれば、絶対に正規形に到達できる
逆に言えば、最左最外簡約を何度やっても正規形に到達できないようなラムダ項は、他のどんな順番で簡約しても絶対に正規形に到達できない

デメリットは、必ずしも効率の良い簡約手順ではないということ