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

date2026-04-01descriptioncapture-avoiding substitution（捕縛回避置換）とα同値の定義を整理し、変数名の付け替えが計算の意味を変えない理由を説明する講義である。prerequisitesdata/lecture/information/programming-languages/foundation/束縛と自由変数の基本-講義.n.mdtype講義statusactive

informationprogramming-languageslambda-calculuslecture

導入どうにゅう

この講義こうぎの核心かくしんは、「β簡約かんやくの実体じったいは置換ちかんであり、置換ちかんは自由変数じゆうへんすうを誤あやまって束縛そくばくしないように行おこなわなければならない」という点てんにある。この「誤あやまった束縛そくばく」を防ふせぐ仕組しくみが捕縛回避置換ほばくかいひちかんcapture-avoiding substitutionであり、名前なまえの付つけ替かえが計算けいさんの意味いみを変かえないことの保証ほしょうがα同値どうちである。

中心ちゅうしん課題かだい

$λ x . (λ y . x)$ に $y$ を代入だいにゅうしようとすると何なにが起おきるか。なぜ単純たんじゅんな文字列置換もじれつちかんでは不十分ふじゅうぶんなのか。

用語ようご

置換ちかんsubstitution: 項こう $t$ の中なかの変数へんすう $x$ の自由じゆうな出現しゅつげんを項こう $s$ で置おき換かえる操作そうさ。 $t [x := s]$ と書かく
変数捕縛へんすうほばくvariable capture: 置換ちかんによって自由変数じゆうへんすうが意図いとせず束縛そくばくされてしまう現象げんしょう
捕縛回避置換ほばくかいひちかんcapture-avoiding substitution: 変数捕縛へんすうほばくを防ふせぐために、必要ひつように応おうじて束縛変数そくばくへんすうを改名かいめいしてから行おこなう置換ちかん
α変換へんかんα-conversion: $λ x . t$ の $x$ を新あたらしい名前なまえ $y$ に付つけ替かえて $λ y . t [x := y]$ にする操作そうさ（ただし $y \notin F V (t)$ ）
α同値どうちα-equivalence: α変換へんかんで行ゆき来きできる項こうどうしの同値どうち関係かんけい

方針ほうしん

まず単純たんじゅんな文字列置換もじれつちかんがなぜ失敗しっぱいするかを見みる。つぎに捕縛回避置換ほばくかいひちかんの定義ていぎを BNF の場合分ばあいわけで書かく。最後さいごにα同値どうちを「名前なまえの違ちがいを無視むしする商集合しょうしゅうごう上うえの等ひとしさ」として捉とらえる。

直感的ちょっかんてきな説明せつめい

「 $x$ を $s$ に置換ちかんする」を「文書ぶんしょの中なかの単語たんごを検索けんさく・置換ちかんする」と同おなじだと思おもうと問題もんだいが起おきる。

たとえば $(λ y . x) [x := y]$ を「 $x$ を $y$ に書かき換かえる」と機械的きかいてきに行おこなうと $λ y . y$ になる。しかし元もとの意味いみは「 $x$ という外側そとがわの値あたいを受うけ取とって、 $y$ 無関係むかんけいに $x$ を返かえす関数かんすう」だった。置換後ちかんごの $λ y . y$ は「 $y$ を受うけ取とって $y$ を返かえす関数かんすう」になってしまい、意味いみが変かわっている。

解決策かいけつさくは「置換ちかんしようとしている自由変数じゆうへんすう $y$ が束縛そくばくされる状況じょうきょうに入はいろうとしたら、束縛変数そくばくへんすうを別名べつめいに改名かいめいする」ことである。

（問題もんだい）
(λy. x)[x := y]
→ λy. y ← y が捕縛ほばくされた（意味いみが変かわった）

（正ただしい手順てじゅん：まず y を z に改名かいめい）
λy. x →(α変換へんかん)→ λz. x
(λz. x)[x := y] → λz. y ← y は自由じゆうのまま保たもたれた

厳密げんみつな説明せつめい

1. 捕縛回避置換ほばくかいひちかんの定義ていぎ

$t [x := s]$ を次つぎの場合分ばあいわけで定義ていぎする。

x [x := s] = s

y [x := s] = y (y \neq x)

(t_{1} t_{2}) [x := s] = (t_{1} [x := s]) (t_{2} [x := s])

λ抽象ちゅうしょうの場合ばあいが重要じゅうようである。

(λ x . t) [x := s] = λ x . t $ x $ は [こ の 中 / こ の な か] で [束 縛 / そ く ば く] さ れ て い る の で [置 換 / ち か ん] し な い) [PARSE ERROR: Undefined("RBrace")]

(λ y . t) [x := s] = λ y . (t [x := s]) $ y \neq x $ か つ $ y \notin F V (s) $) [PARSE ERROR: Undefined("RBrace")]

(λ y . t) [x := s] = λ z . (t [y := z] [x := s]) $ y \neq x $ か つ $ y \in F V (s) $ 、 $ z $ は [新 / あ た ら] し い [名 前 / な ま え]) [PARSE ERROR: Undefined("RBrace")]

最後さいごの行ぎょうが捕縛回避ほばくかいひのための改名かいめいである。

2. α同値どうち

α変換へんかん $λ x . t \to_{α} λ y . t [x := y]$ （ただし $y \notin F V (t)$ ）によって行ゆき来きできる項こうはα同値どうちである。

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

記号きごうとしての名前なまえは異ことなるが、「受うけ取とったものをそのまま返かえす関数かんすう」という意味いみは同おなじである。

3. β簡約かんやくとの関係かんけい

β簡約かんやくの定義ていぎ（次つぎの講義こうぎ）は：

(λ x . t) s \to_{β} t [x := s]

右辺うへんの置換ちかんは必かならず捕縛回避ほばくかいひで行おこなわれる。α同値どうちを認みとめることで、 $t [x := s]$ は代表元だいひょうもとの取とり方かたに依存いぞんしない（名前なまえの選えらび方かたに依存いぞんしない）ことが保証ほしょうされる。

最小さいしょうの具体例ぐたいれい

例れい 1: 捕縛回避ほばくかいひが不要ふようなケース

$(λ x . λ y . x) [x := a]$

$a$ は変数名へんすうめいだけとして $a \notin {y}$ と仮定かていすると：

$= λ x . λ y . x$ （外側そとがわの $λ x$ が $x$ を束縛そくばくしているので置換ちかんしない）

例れい 2: 捕縛回避ほばくかいひが必要ひつようなケース

$(λ y . x) [x := y]$ → $y \in F V (y)$ なので改名かいめいが必要ひつよう

$z$ を新あたらしい名前なまえとして：

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

別べつの見方みかた

α同値どうちを「商しょう」として見みると、λ項らむだこうの集合しゅうごうをα同値どうち類るいで割わった商集合しょうしゅうごうの上うえでβ簡約べーたかんやくを定義ていぎすることになる。あるいはde Bruijn 指標de Bruijn index（変数へんすうを名前なまえでなく「何なん番目ばんめの λ に束縛そくばくされているか」という番号ばんごうで表あらわす方法ほうほう）を使つかえば、α同値どうちな項こうは同一どういの表現ひょうげんになり改名かいめいが不要ふようになる。

見分みわけ方かた

$t [x := s]$ を計算けいさんするとき、 $s$ に自由変数じゆうへんすうが含ふくまれるかを先さきに $F V (s)$ で確認かくにんする
$λ y . \dots$ に入はいるとき、 $y \in F V (s)$ なら改名かいめいしてから置換ちかんする
$λ x . x =_{α} λ y . y$ のように束縛変数そくばくへんすうの付つけ替かえはα同値どうちの範囲はんい内ない

一言ひとことでいうと

置換ちかんは「 $x$ を $s$ に書かき換かえる」だけでなく「自由変数じゆうへんすうを誤あやまって束縛そくばくしないように慎重しんちょうに行おこなう操作そうさ」であり、α同値どうちは「変数名へんすうめいは本質ほんしつでない」ことの形式化けいしきかである。