john7rv

ラムダ計算とはラムダ関数に３つの変換規則を適用して
数学の計算を表現することです

λx.xy

とあったときλと共に定義されている引数xは束縛変数となります
束縛変数は一度代入されれば変更できません
引数でないyは自由変数となります

束縛変数の名前を変える操作をα変換と言います

λx.xy

をxをzに変数名を変えても

λz.zy

同じ内容になります

実際にラムダ関数に渡された数や変数を代入して書き換えることβ簡約と言います
（β変換ということもあります）

(λx.xy) f

(λx.xy)にfが渡されたとしたら代入してλx.が消え

fy

と書き換えることです

(λx.x+3) 2

をβ簡約すれば
xに2を代入して

2+3

となり答えは

5

となります

ラムダ式の中でまだβ変換されておらずこれからβ変換できるものを
β基と呼びます

2つの関数が全ての引数において同じ値を返すならば
2つの関数は同値であるとみなせる(外延性)
そのため書き換えることができる

λx.fx -> f