簡約順番の標準化定理
standardization theorem
定理
$ 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に至る、というのが定理の主張
証明
参考