β-簡約

β-簡約(β-reduction)

ラムダ式の簡約ルールの一つ

仮引数を実引数に置き換える操作

代入操作について

$ (λx.M) N \Rightarrow [N / x] M

M中の自由変数xをすべてNで置き換えて得られるラムダ式

$ (\lambda x.f(x))(a)\ \dot{=}\ f(a):Y

単純型付きラムダ計算の場合

例:

(λx.x + 1) 3

→ 3 + 1

→ 4

確認用

Q. β-簡約

関連

参考

メモ

調査用

Wikipedia.icon

Wikipedia.icon