定理

M\xrightarrow{\ast}_\beta Nならば、MからNへ至る標準的な順番による簡約過程が存在する

「標準的な順番による簡約過程」とは、

ラムダ抽象は、\lambdaが、\lambda_1\lambda_2(\lambda_3(\lambda_4)\lambda_5..のように、入れ子があったり横に並んだりしているが、

「最も左に存在する\lambdaについて簡約していく操作」のことを、こう呼ぶ

どのラムダ項を簡約するかを明示する記法を用いて定式化すれば

M_1\xrightarrow{n_1}_\beta M_2\xrightarrow{n_2}_\beta\cdots\xrightarrow{n_k}_\beta M_{k+1}のとき、

n_1\le n_2\le\cdots\le n_kになる

ということ

例: M\equiv(\lambda x.(xx))((\lambda y.y)z)について、「標準的な順番による簡約を1回行うと

「\lambda x.」を部分が適用されて、

((\lambda y,y)z)((\lambda y.y)z)になる

次は、z((\lambda y.y)z)になる

これを繰り返していくと、Nに至る、というのが定理の主張

証明

参考

『C言語による計算の理論』 p.176