マクロとラムダ計算

マクロ（あるいはテンプレート）は、アルファ変換ができないラムダ計算だと思えばいい。

単純置換を定義する。M, N, Lを式（項）だとして、x, y, zなどを変数だとする。単純置換をするオペレータを{L/x}のように書く。とりあえずは1個の変数だけを置換。

1. x{L/x} ⇒ L
2. y{L/x} ⇒ y （x≠y）
3. (M・N){L/x} ⇒ (M{L/x}・N{L/x})
4. (λx.M){y/x} ⇒ λy.(M{y/x})
5. (λx.M){L/x} ⇒ 未定義 （Lは変数ではない）
6. (λy.M){L/x} ⇒ λy.(M{L/x}) （x≠y）

これでいいと思う。

この単純置換は束縛変数さえも無条件で置換する。よって具合が悪い。束縛変数を考慮する置換を[L/x]とすると。

1. x[L/x] ⇒ L
2. y[L/x] ⇒ y （x≠y）
3. (M・N)[L/x] ⇒ (M[L/x]・N[L/x])
4. (λx.M)[L/x] ⇒ (λx.M)
5. (λy.M)[L/x] ⇒ λy.(M[L/x]) （x≠y）