肝心なことを書き忘れた。
>>170
つまり標準形のあるλ式（計算が終了する）であるならば、
λ項はβ変換適用ごとに減っていくので「簡約」なわけです。
通常､計算は終了することに意味があるとされるので、逆に
β変換が「簡約」であるようなλ式を「正しい」プログラムの表現
と見るわけです。

ついでに言えば、現実のプログラムでは評価順序も決まってるから、
その評価順序において簡約し切れるような式であれば良いわけで、
標準形のあるλ式以外にも､特定の簡約順序によって
有限回で簡約不能な式（値）になるような式も
条件付で認めるが立場あり、実はプログラムの基礎理論としては主流です。