自由変数と束縛変数

数学や形式言語に関連する分野（数理論理学と計算機科学）において、自由変数（または自由変項、英: free variable）は数式や論理式で置換が行われる場所を指示する記法である。この考え方はプレースホルダーやワイルドカードにも関連する。

変数x は、例えば次のように書くと 束縛変数（または束縛変項、英: bound variable）になる。

全ての $x$ について $(x+1)^{2}\geq x^{2}+2x+1$ が成り立つ。

あるいは

$x^{2}=2$ となるような $x$ が存在する。

これらの命題では、x の代わりに別の文字を使っても論理的には全く変化しない。しかし、複雑な命題で同じ文字を別の意味で再利用すると混乱が生じる。すなわち、自由変数が束縛されると、ある意味ではその後の数式の構成をサポートする作業に関与しなくなる。

プログラミングにおいては、自由変数とは関数の中で参照される局所変数や引数以外の変数を意味する。

例

自由変数と束縛変数を正確に定義する前に、定義をより明確にする例を以下に示す。

次の式

$\sum _{k=1}^{10}f(k,n)$

において、$n$ は自由変数、$k$ は束縛変数である。結果として、この式は $n$ の値によって変化するが $k$ には依存しない。

次の式

$\int _{0}^{\infty }x^{y-1}e^{-x}\,dx$

において、$y$ は自由変数、$x$ は束縛変数である。同様にこの式の値は $y$ の値によって変化するが、$x$ には依存しない。

次の式

$\lim _{h\rightarrow 0}{\frac {f(x+h)-f(x)}{h}}$

において、$x$ は自由変数、$h$ は束縛変数である。同様にこの式の値は $x$ の値によって変化するが、$h$ には依存しない。

次の論理式

$\forall x\ \exists y\ \varphi (x,y,z)$

において、$z$ は自由変項、$x$ と $y$ は束縛変項である。この論理式の真理値は $z$ の値によって変化するが、$x$ と $y$ には依存しない。

束縛作用素（演算子）

以下は変数束縛作用素（演算子）である。それぞれ、変数 $x$ を束縛する。

$\sum _{x\in S}\quad \quad \prod _{x\in S}\quad \quad \int _{0}^{\infty }\cdots \,dx\quad \quad \lim _{x\to 0}\quad \quad \forall x\quad \quad \exists x$

形式的解説

変数束縛機構は数学、論理学、計算機科学など様々な分野で使われるが、いずれの場合もそれらは式と変数についてのその分野における全く統語的な属性である。ここでは式を木で表し、その葉ノードに変数、定数、定項などが対応し、葉でないノードに論理演算子が対応するように構成すると考える。変数束縛演算子は論理演算子であり、ほとんど全ての形式言語に存在する。実際、束縛ができない言語は非常に表現能力が低く、使いにくい。束縛演算子 $Q$ は2つの引数をとる。一つは変数 $v$、もう一つは式 $P$ であり、これによって新たな式 $Q(v,P)$ が生成される。束縛演算子の意味は、その言語の意味論で提供されるもので、ここでは考慮しない。

変数束縛は三つのものと関連する。一つめは変数 $v$、二つめは式内でその変数が現れる場所 $a$、三つめは $Q(v,P)$ で形成される木の葉でないノード $n$ である。ここでは、変数は葉ノードにあると定義したので、束縛はノード $n$ の下で起きる。

数学における例として、次の関数定義式を考える。

$(x_{1},\ldots ,x_{n})\mapsto \operatorname {t}$

ここで、$t$ は式である。$t$ には $x_{1},\dots ,x_{n}$ の全部または一部が含まれることがあり、他の変数も含まれることがある。この場合、関数定義が変数 $x_{1},\dots ,x_{n}$ を束縛していると言える。

ラムダ計算では、$M=\lambda x.T$ というラムダ式で、$x$ は $M$ においては束縛変数、$T$ においては自由変数である。$T$ にさらにラムダ式 $\lambda x.U$ が含まれる場合、$x$ はこの中で再束縛される。このような入れ子の内側の $x$ の束縛は外側の束縛を覆い隠す。$U$ における $x$ の出現は新たな $x$ の自由な出現である。

プログラムのトップレベルで束縛された変数は、技術的にはそれが束縛された項の中では自由変数であるが、固定アドレスにコンパイルされるため、特別な扱われ方をすることが多い。同様に計算可能関数に束縛された識別子も技術的にはその本体内では自由変数だが、特別に扱われる。

自由変数を全く含まない項あるいは式を閉項（英: closed term）または閉論理式（英: closed formula）または閉式と呼ぶ。

参考文献

本項目の一部はGFDLでリリースされているFOLDOCの記述に基づいているが、大部分はその後の編集によるものである。

関連項目

• 変数 (数学)
• 変数 (プログラミング)
• クロージャ
• 生成 (数学)
• スコープ (プログラミング)

外部リンク

• 束縛変数と自由変数 師玉康成