置換

定義 2.2（「型なしラムダ計算」§2）

$M[x:=N]$ を、 $M$ の自由な $x$ をすべて $N$ で置き換えた項とする。帰納的には

x[x:=N]\equiv N,\quad y[x:=N]\equiv y\ (y\ne x),\quad (PQ)[x:=N]\equiv P[x:=N]\,Q[x:=N],

(\lambda y.P)[x:=N]\equiv\lambda y.P[x:=N]\quad(y\ne x,\ y\notin\mathrm{FV}(N))

と定める。最後の条件は変数の規約により（束縛変数を付け替えて）いつでも満たせる。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。