η簡約
$ λ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と書く 参考