束縛そくばくと自由変数じゆうへんすうの基本きほん

date2026-04-01descriptionλ項における束縛・自由変数・スコープの概念を整理し、変数の出現が構文的にどう決まるかを説明する講義である。prerequisitesdata/lecture/information/discrete-math/集合と写像の基本-講義.n.md / data/lecture/information/programming-languages/foundation/関数型プログラミングの入口-講義.n.mdtype講義statusactive

informationprogramming-languageslambda-calculuslecture

導入どうにゅう

この講義こうぎの核心かくしんは、「変数へんすうの名前なまえは本質ほんしつでなく、どこに束縛そくばくされているかが本質ほんしつである」という点てんにある。 $λ x . x$ と $λ y . y$ は名前なまえが違ちがうが「同おなじ関数かんすう」である。この見方みかたをできるようにするために、束縛そくばく・自由変数じゆうへんすう・スコープの概念がいねんを正確せいかくに定義ていぎする。

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

$λ x . (λ y . x y)$ において、最外側そとがわの $x$ と内側うちがわの $y$ はどう違ちがうか。また $λ x . (x y)$ の $y$ はなぜ「外そとから来る何なにか」なのか。

用語ようご

λ項らむだこうλ-term: 変数へんすう・λ抽象ちゅうしょう・適用てきようのいずれかから再帰的さいきてきに構成こうせいされる式しき
束縛変数そくばくへんすうbound variable: λ抽象ちゅうしょうのパラメータとして宣言せんげんされ、そのスコープ内ないで参照さんしょうされる変数へんすう
自由変数じゆうへんすうfree variable: 束縛そくばくされていない出現しゅつげんを持もつ変数へんすう
スコープscope: λ抽象ちゅうしょう $λ x . M$ において $x$ が束縛そくばくする領域りょういき $M$

方針ほうしん

まずλ項らむだこうの構文こうぶん（BNF）を確認かくにんする。つぎに自由変数じゆうへんすうの集合しゅうごう $F V (t)$ を構造帰納法こうぞうきのうほうで定義ていぎする。最後さいごに、束縛そくばくの重かさなり（ネスト）がスコープに何なにをもたらすかを見みる。

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

プログラミングの経験けいけんから「関数かんすうの引数名ひきすうめいはその関数かんすうの中なかだけで有効ゆうこうだ」という感覚かんかくはあるはずである。 $λ x . M$ の $x$ はちょうどそれで、 $M$ の外そとでは $x$ という名前なまえは意味いみを持もたない。

逆に $λ x . (x y)$ の $y$ は「この関数かんすうが呼よばれる文脈ぶんみゃくから来る何なにか」であり、定義ていぎの中なかにスコープが存在そんざいしない。これが自由変数じゆうへんすうである。

λx. (λy. x y)
↑ ↑↑
y は内側うちがわの λy で束縛そくばく
x は外側そとがわの λx で束縛そくばく
外側そとがわのスコープは λy. x y 全体ぜんたいである

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

1. λ項らむだこうの構文こうぶん

t : := x ∣ λ x . t ∣ t_{1} t_{2}

$x$ : 変数へんすう（Variable）
$λ x . t$ : λ抽象ちゅうしょう（Abstraction）—「 $x$ を受うけ取とって $t$ を返かえす関数かんすう」
$t_{1} t_{2}$ : 適用てきよう（Application）—「 $t_{1}$ に $t_{2}$ を渡わたす」

2. 自由変数じゆうへんすう集合しゅうごう $F V (t)$

F V (x) = {x}

F V (λ x . t) = F V (t) ∖ {x}

F V (t_{1} t_{2}) = F V (t_{1}) \cup F V (t_{2})

λ抽象ちゅうしょうの場合ばあい、 $x$ が束縛そくばくされるので $F V (t)$ から除のぞかれる。

3. 束縛変数そくばくへんすう集合しゅうごう $B V (t)$

B V (x) = \emptyset

B V (λ x . t) = {x} \cup B V (t)

B V (t_{1} t_{2}) = B V (t_{1}) \cup B V (t_{2})

4. 閉項へいこう

$F V (t) = \emptyset$ である項こうを閉項へいこうclosed term（またはコンビネータcombinator）という。閉項へいこうは外部がいぶの文脈ぶんみゃくに依存いぞんしない。

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

例れい 1

$t = λ x . (x y)$

$F V (t) = F V (x y) ∖ {x} = ({x} \cup {y}) ∖ {x} = {y}$

$y$ が自由変数じゆうへんすうである。

例れい 2

$t = λ x . λ y . (x y)$

$F V (t) = F V (λ y . (x y)) ∖ {x} = ({x, y} ∖ {y}) ∖ {x} = \emptyset$

閉項へいこうである。

例れい 3: スコープの重かさなり

$t = (λ x . x) (λ x . x x)$

左側がわと右側みぎがわで別々べつべつに $x$ が束縛そくばくされており、2 つの $x$ は別物べつものである。どちらも外そとから見みえない。 $F V (t) = \emptyset$ 。

別べつの見方みかた

λ抽象ちゅうしょうを「新あたらしいスコープを開ひらくブロック」とみると、スコープの入いれ子こはファイルシステムの階層かいそうに似にている。変数へんすう名の解決かいけつは「最もっとも内側うちがわのスコープから外側そとがわへ探さがす」ルールで行おこなわれる。自由変数じゆうへんすうはどのスコープにも見みつからなかった変数へんすう名である。

見分みわけ方かた

変数へんすう $x$ のある出現あるしゅつげんが束縛そくばくか自由じゆうかは、「そこから外側そとがわへ向むかって $λ x$ が現あらわれるか」を確認かくにんする
$F V (t)$ を計算けいさんするには、BNF の場合分ばあいわけに従したがって内側うちがわから再帰的さいきてきに求もとめる
$F V (t) = \emptyset$ なら閉項へいこうであり、単独たんどくで評価ひょうかできる

一言ひとことでいうと

λ項らむだこうにおける変数へんすうの意味いみは名前なまえでなくスコープで決きまる。自由変数じゆうへんすうとは「この項こうの外そとから供給きょうきゅうされる値あたいのプレースホルダ」であり、束縛変数そくばくへんすうとは「この項こうの内部ないぶで宣言せんげん・参照さんしょうされるもの」である。