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

date2026-07-14document_iddoc_a981b8f475418940394a177eabf1e170descriptionλ項の構文、束縛子、作用域、束縛出現、自由出現、自由変数集合を厳密に定義する講義である。prerequisitesdata/lecture/information/discrete-math/sets-and-maps-basics.lecture.n.md / data/lecture/information/programming-languages/foundation/introduction-to-functional-programming.lecture.n.mdtype講義statusactive

informationprogramming-languageslambda-calculuslecture

1導入どうにゅう

この講義こうぎでは、λ項こうの構文こうぶんを定義ていぎし、変数へんすうの各かく出現しゅつげんを束縛出現そくばくしゅつげんまたは自由出現じゆうしゅつげんに分類ぶんるいする。変数名へんすうめいだけでは分類ぶんるいできず、その出現位置しゅつげんいちと束縛子そくばくしの作用域さよういきが必要ひつようである。

2構文こうぶんと構文木こうぶんぎ

可算無限かさんむげんな変数集合へんすうしゅうごうを $[PARSE ERROR: Undefined("Command(\"mathcal\")")] V$ とする。型かたなしλ項こうの集合しゅうごう $Λ$ は次つぎの生成規則せいせいきそくで再帰的さいきてきに定義ていぎする。

M : := x ∣ (M N) ∣ (λ x . M) (x \in [PARSE ERROR: Undefined("Command(\"mathcal\")")] V)

$x$ は変数へんすう、 $M N$ は適用てきよう、 $λ x . M$ はλ抽象ちゅうしょうである。括弧かっこを省略しょうりゃくするとき、適用てきようは左結合ひだりけつごうとし、λ抽象ちゅうしょうの本体ほんたいは可能かのうな限かぎり右みぎまで延長えんちょうする。したがって $M N P = (M N) P$ であり、 $λ x . M N = λ x . (M N)$ である。

3束縛子そくばくし・作用域さよういき・出現しゅつげん

$λ x . M$ の $λ x$ を $x$ の束縛子そくばくしbinder、部分項ぶぶんこう $M$ をその作用域さよういきscopeという。構文木こうぶんぎにおける変数へんすう $x$ の葉はの出現しゅつげんが、ある $λ x$ の本体ほんたいに含ふくまれるとき、その出現しゅつげんは束縛そくばくされる。該当がいとうする束縛子そくばくしが複数ふくすうある場合ばあいは、構文木上こうぶんぎじょうで最もっとも近ちかい束縛子そくばくしがその出現しゅつげんを束縛そくばくする。いずれの $λ x$ の作用域さよういきにも属ぞくさない $x$ の出現しゅつげんは自由じゆうである。

「束縛そくばくされる」という性質せいしつは変数名へんすうめいでなく出現しゅつげんに属ぞくする。例たとえば

x (λ x . x)

では、左端さたんの $x$ は自由出現じゆうしゅつげんであり、右端うたんの $x$ は内側うちがわの $λ x$ による束縛出現そくばくしゅつげんである。また

λ x . ((λ x . x) x)

では、内側うちがわの本体ほんたいにある $x$ は内側うちがわの束縛子そくばくしに、最後さいごの $x$ は外側そとがわの束縛子そくばくしに束縛そくばくされる。この現象げんしょうを遮蔽しゃへいshadowingという。

4自由変数集合じゆうへんすうしゅうごう

$F V (M)$ は $M$ に自由出現じゆうしゅつげんを持もつ変数名へんすうめいの集合しゅうごうであり、構文こうぶんに沿そって次つぎのように定義ていぎする。

F V (x) = {x}

F V (M N) = F V (M) \cup F V (N)

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

例たとえば、

F V (λ x . x y) = {y}, F V (λ x . λ y . x y) = [PARSE ERROR: Undefined("Command(\"varnothing\")")] .

$F V (M) = [PARSE ERROR: Undefined("Command(\"varnothing\")")]$ である項こうを閉項へいこうclosed term、それ以外いがいを開項かいこうopen termという。閉項へいこうであることは、変数へんすうの各出現かくしゅつげんがいずれかの束縛子そくばくしに束縛そくばくされることと同値どうちである。

5確認かくにん

$M = λ x . (x (λ y . x y) z)$ では、二ふたつの $x$ の出現しゅつげんは外側そとがわの $λ x$ に束縛そくばくされ、 $y$ の出現しゅつげんは $λ y$ に束縛そくばくされ、 $z$ の出現しゅつげんだけが自由じゆうである。したがって $F V (M) = {z}$ である。次つぎの講義こうぎでは、この出現しゅつげんごとの分類ぶんるいを用もちいて捕縛ほばくを回避かいひする置換ちかんを定義ていぎする。

Basics of Binding and Free Variables

1Introduction

This lecture defines the syntax of lambda terms and classifies every variable occurrence as bound or free. A name alone does not determine the classification; the occurrence's position and the scope of its binder are essential.

2Syntax and syntax trees

Let $[PARSE ERROR: Undefined("Command(\"mathcal\")")] V$ be a countably infinite set of variables. The set $Λ$ of untyped lambda terms is defined recursively by the grammar

M : := x ∣ (M N) ∣ (λ x . M) (x \in [PARSE ERROR: Undefined("Command(\"mathcal\")")] V) .

Here $x$ is a variable, $M N$ is an application, and $λ x . M$ is an abstraction. When parentheses are omitted, application associates to the left and the body of an abstraction extends as far to the right as possible. Thus $M N P = (M N) P$ and $λ x . M N = λ x . (M N)$ .

3Binders, scopes, and occurrences

In $λ x . M$ , the prefix $λ x$ is a binder for $x$ , and the subterm $M$ is its scope. An occurrence of $x$ at a leaf of the syntax tree is bound if it lies inside the body of some $λ x$ . If several such binders enclose the occurrence, the nearest one in the syntax tree binds it. An occurrence of $x$ that lies in the scope of no $λ x$ is free.

Boundness is a property of an occurrence, not merely of a variable name. For example, in

x (λ x . x),

the leftmost occurrence of $x$ is free, whereas the rightmost occurrence is bound by the inner $λ x$ . In

λ x . ((λ x . x) x),

the occurrence in the inner body is bound by the inner binder, while the final occurrence is bound by the outer binder. This phenomenon is called shadowing.

4The set of free variables

$F V (M)$ is the set of variable names that have at least one free occurrence in $M$ . It is defined structurally by

F V (x) = {x},

F V (M N) = F V (M) \cup F V (N),

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

For example,

F V (λ x . x y) = {y}, F V (λ x . λ y . x y) = [PARSE ERROR: Undefined("Command(\"varnothing\")")] .

A term $M$ is closed if $F V (M) = [PARSE ERROR: Undefined("Command(\"varnothing\")")]$ and open otherwise. A term is closed exactly when every variable occurrence is bound by some binder.

5Check

In $M = λ x . (x (λ y . x y) z)$ , both occurrences of $x$ are bound by the outer $λ x$ , the occurrence of $y$ is bound by $λ y$ , and only the occurrence of $z$ is free. Hence $F V (M) = {z}$ . The next lecture uses this occurrence-level classification to define substitution that avoids capture.