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

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変数へんすうの選択せんたくによって結果けっかの表記ひょうきは異ことなり得うるが、いずれの結果けっかもα同値どうちである。

Basics of Substitution and Alpha-Equivalence

1Introduction

This lecture defines the operation that replaces only the free occurrences of a variable by a term. Naive textual replacement may accidentally bind a free variable, so bound variables must sometimes be renamed to avoid variable capture. Alpha-equivalence formalizes these harmless renamings.

2Substitution and capture

$M [x := N]$ denotes the result of replacing the free occurrences of $x$ in $M$ by the term $N$ . Bound occurrences are not targets of substitution. For example,

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

By contrast, mechanically turning $(λ y . x) [x := y]$ into $λ y . y$ makes the inserted occurrence of $y$ bound by $λ y$ , although it was free before insertion. This change is variable capture. The correct result first renames the binder and is $λ z . y$ .

3Fresh variables

For a finite set of terms $S$ , a variable $z$ is fresh for $S$ if its name occurs in none of the terms in $S$ . Because $[PARSE ERROR: Undefined("Command(\"mathcal\")")] V$ is infinite and finitely many terms contain only finitely many variable names, a fresh variable can always be chosen. Below, $z$ is chosen not to occur in either $M$ or $N$ , avoiding ambiguity during renaming.

4Capture-avoiding substitution

Capture-avoiding substitution is defined recursively on syntax:

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]) .

There are three abstraction cases:

(λ 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)),

where $z$ in the last clause is fresh for both $M$ and $N$ . More precisely, if $x \notin F V (M)$ , the result is $M$ itself and no renaming is needed; the last clause need only be applied when $x \in F V (M)$ .

For example, choosing $z$ fresh and distinct from $x, y$ gives

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

The inserted occurrence of $y$ remains free in the result.

5Alpha-conversion and alpha-equivalence

Alpha-conversion simultaneously renames a binder and the occurrences that it binds to a fresh variable. If $y \notin F V (M)$ , then

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

where the substitution on the right is capture-avoiding. Alpha-equivalence $=_{α}$ is the least congruence relation that permits this elementary renaming in any subterm and is reflexive, symmetric, and transitive. Consequently,

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

but free variables cannot be renamed, so $λ x . x y [PARSE ERROR: Undefined("Command(\"not\")")] =_{α} λ x . x z$ . Moreover, $λ x . λ y . x [PARSE ERROR: Undefined("Command(\"not\")")] =_{α} λ x . λ y . y$ : alpha-equivalence preserves binding structure.

6Connection to beta-reduction

Beta-reduction is defined by

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

using capture-avoiding substitution on the right. For example,

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

not $λ y . y$ . Different choices of a fresh variable may produce different spellings, but all resulting terms are alpha-equivalent.