置換ちかんとα同値どうちの基本きほん

date2026-07-14document_iddoc_9d68d494495c280adb6049e30a0c55c1description捕縛回避置換、fresh変数、α変換、α同値を厳密に定義し、β簡約の準備を行う講義である。prerequisitesdata/lecture/information/programming-languages/foundation/variable-binding-and-free-variables-basics.lecture.n.mdtype講義statusactive

informationprogramming-languageslambda-calculuslecture

1導入どうにゅう

この講義こうぎでは、変数へんすうの自由出現じゆうしゅつげんだけを項こうで置換ちかんする操作そうさを定義ていぎする。単純たんじゅんな文字列置換もじれつちかんは自由変数じゆうへんすうを意図いとせず束縛そくばくするため、束縛変数そくばくへんすうの改名かいめいによって変数捕縛へんすうほばくvariable captureを回避かいひする必要ひつようがある。この改名かいめいを形式化けいしきかするα同値どうちも定義ていぎする。

2置換ちかんと捕縛ほばく

$M [x := N]$ は、 $M$ における $x$ の自由出現じゆうしゅつげんを項こう $N$ で置換ちかんした結果けっかを表あらわす。束縛出現そくばくしゅつげんは置換ちかんの対象たいしょうではない。例たとえば

(λ x . x y) [x := N] = λ x . x y

である。一方いっぽう、 $(λ y . x) [x := y]$ を機械的きかいてきに $λ y . y$ とすると、置換前ちかんまえに自由じゆうであった右辺うへんの $y$ が $λ y$ に束縛そくばくされる。この変化へんかが変数捕縛へんすうほばくである。正ただしい結果けっかは、束縛子そくばくしを先さきに改名かいめいした $λ z . y$ である。

3fresh 変数へんすう

項こうの有限集合ゆうげんしゅうごう $S$ に対たいし、 $S$ に出現しゅつげんするどの変数名へんすうめいとも異ことなる変数へんすう $z$ を $S$ に対たいしてfreshフレッシュであるという。 $[PARSE ERROR: Undefined("Command(\"mathcal\")")] V$ は無限むげんであり、有限個ゆうげんこの項こうに出現しゅつげんする変数名へんすうめいは有限個ゆうげんこなので、fresh変数へんすうは常つねに選択せんたくできる。以下いかでは、改名かいめいによる混同こんどうを避さけるため、 $z$ を $M$ と $N$ の双方そうほうに出現しゅつげんしないように選択せんたくする。

4捕縛回避置換ほばくかいひちかん

捕縛回避置換ほばくかいひちかんを構文こうぶんに関かんして再帰的さいきてきに定義ていぎする。

x [x := N] = N, y [x := N] = y (y \neq x),

(M_{1} M_{2}) [x := N] = (M_{1} [x := N]) (M_{2} [x := N]) .

λ抽象ちゅうしょうには三みっつの場合ばあいがある。

(λ x . M) [x := N] = λ x . M,

(λ y . M) [x := N] = λ y . (M [x := N]) (y \neq x, y \notin F V (N)),

(λ y . M) [x := N] = λ z . ((M [y := z]) [x := N]) (y \neq x, y \in F V (N)),

ただし、最後さいごの場合ばあいの $z$ は $M$ と $N$ に対たいしてfreshである。より厳密げんみつには、 $x \notin F V (M)$ なら置換結果ちかんけっかは $M$ 自身じしんであり、改名かいめいも不要ふようである。上うえの最後さいごの場合ばあいは $x \in F V (M)$ のときに適用てきようすればよい。

例れいとして、 $z$ を $x, y$ と異ことなるfresh変数へんすうに選えらぶと、

(λ y . x y) [x := y] = λ z . ((x z) [x := y]) = λ z . y z .

挿入そうにゅうされた $y$ は結果けっかでも自由じゆうである。

5α変換へんかんとα同値どうち

束縛子そくばくしと、それが束縛そくばくする出現しゅつげんを一斉いっせいにfresh変数へんすうへ改名かいめいする操作そうさをα変換へんかんという。 $y \notin F V (M)$ のとき、

λ x . M =_{α} λ y . (M [x := y])

とする。ここで右辺うへんの置換ちかんは捕縛回避置換ほばくかいひちかんである。α同値どうち $=_{α}$ は、この基本的きほんてきな改名かいめいを任意にんいの部分項ぶぶんこうで許ゆるし、反射性はんしゃせい・対称性たいしょうせい・推移性すいいせいを満みたす最小さいしょうの合同関係ごうどうかんけいである。したがって

λ x . x =_{α} λ y . y,

だが、自由変数じゆうへんすうは改名かいめいできないため $λ x . x y [PARSE ERROR: Undefined("Command(\"not\")")] =_{α} λ x . x z$ である。また $λ x . λ y . x [PARSE ERROR: Undefined("Command(\"not\")")] =_{α} λ x . λ y . y$ であり、α同値どうちは束縛構造そくばくこうぞうを保存ほぞんする。

6β簡約かんやくへの接続せつぞく

β簡約かんやくは

(λ x . M) N ⟶_{β} M [x := N]

と定義ていぎされ、右辺うへんには捕縛回避置換ほばくかいひちかんを用もちいる。例たとえば

(λ x . λ y . x) y ⟶_{β} λ z . y

であり、 $λ y . y$ ではない。fresh変数へんすうの選択せんたくによって結果けっかの表記ひょうきは異ことなり得うるが、いずれの結果けっかもα同値どうちである。