λx.Px→_\eta P

定義

ラムダ抽象の集合\Lambda上の「二項関係\eta」を以下のように定義する

\eta=\{(\lambda x.Px,P)|P\in\Lambda, x\notin \mathrm{Var}(P)\}

ここで\mathrm{Var}(M)はMの自由変数全体を表す

関係\etaより誘導される1ステップη簡約\to_\etaを\etaを満たす最小の両立関係と定義する

\to_\etaの反射推移閉包を\xrightarrow{\ast}_\etaと書く

これがη簡約

参考

『(理論)12 計算モデルの基礎理論』 p.120