簡約グラフ
ラムダ抽象のβ簡約過程を表したもの
Church-Rosserの定理がなりたつので、β正規形を持つラムダ式の場合は、分岐があろうと最終的に同一のβ正規形に辿り着く
I(IΩ)の簡約グラフ
https://gyazo.com/a78636b88d5b882f0c6524f4a86b99c4
節に当たる部分が簡約過程
これはβ正規形を持たない
矢印上の文字は、そのラムダ抽象を簡約したよ、という意味
例えば
$ I(I\Omega)\xrightarrow{I\Omega}I\Omegaは、IにΩを適用している
つまりIΩを簡約してΩにしている
$ I(I\Omega)\xrightarrow{I(I\Omega)}I\OmegaはIにIΩを適用している
M=(λx.Ix)(IΩ)の簡約グラフ
これはβ正規形を持たない
https://gyazo.com/38a82d97c796eb416bbf0ccb8f4c7fd5