ラムダ計算
$ f(x)から，名前を無くす，数値などの値を無くすなどをする
した結果がこちら
純粋ラムダ計算の構文の定義
1. 変数$ vはラムダ式
2. $ M, Nをラムダ式としたとき，$ MNはラムダ式 (ラムダ簡約)
3. $ xを変数，$ Mをラムダ式としたとき，$ \lambda{x.M}はラムダ式 (ラムダ抽象)
色んなラムダ計算
純粋ラムダ計算
型付きラムダ
束縛変数と自由変数
$ \lambda{x.y\lambda{y.xy}}というラムダ式において，1番目に出てくる$ yは自由変数として現れるという．それ以外の変数は，束縛変数として現れる
厳密には以下のように定義される
ラムダ式$ M中の自由変数の全体を$ FV(M)で表す．
$ FV(x) = \{x\},
$ FV(MN) = P(M) \cup P(N),
$ FV(\lambda{x.M}) = P(M) - \{x\}.