自由変数と束縛変数のソースを表示

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

[[変数 (数学)|変数]]''x'' は、例えば次のように書くと '''束縛変数'''（または'''束縛変項'''、{{lang-en-short|bound variable}}）になる。
: 全ての <math>x</math> について <math>(x+1)^2\ge x^2+2x+1</math> が成り立つ。
あるいは
: <math>x^2=2</math> となるような <math>x</math> が存在する。
これらの命題では、''x'' の代わりに別の文字を使っても論理的には全く変化しない。しかし、複雑な[[命題]]で同じ文字を別の意味で再利用すると混乱が生じる。すなわち、自由変数が束縛されると、ある意味ではその後の数式の構成をサポートする作業に関与しなくなる。

[[プログラミング (コンピュータ)|プログラミング]]においては、'''自由変数'''とは[[サブルーチン|関数]]の中で参照される[[局所変数]]や[[引数]]以外の[[変数 (プログラミング)|変数]]を意味する。

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

次の式

:<math>\sum_{k=1}^{10} f(k,n)</math>

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

次の式

:<math>\int_0^\infty x^{y-1} e^{-x}\,dx</math>

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

次の式

:<math>\lim_{h\rightarrow 0}\frac{f(x+h)-f(x)}{h}</math>

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

次の論理式

:<math>\forall x\ \exists y\ \varphi(x,y,z)</math>

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

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

: <math>\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</math>

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

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

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

::<math> (x_1, \ldots , x_n) \mapsto \operatorname{t}</math>

ここで、<math>t</math> は式である。<math>t</math> には <math>x_1, \dots, x_n</math> の全部または一部が含まれることがあり、他の変数も含まれることがある。この場合、関数定義が変数 <math>x_1, \dots, x_n</math> を束縛していると言える。

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

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

自由変数を全く含まない項あるいは式を'''閉項'''（{{lang-en-short|closed term}}）または'''閉論理式'''（{{lang-en-short|closed formula}}）または'''閉式'''と呼ぶ。

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

== 関連項目 ==
*[[変数 (数学)]]
*[[変数 (プログラミング)]]
*[[クロージャ]]
*[[生成 (数学)]]
*[[スコープ (プログラミング)]]

== 外部リンク ==
* [http://schubert.cs.shinshu-u.ac.jp/~miyao/UD/Subjects/Kouri/node28.html 束縛変数と自由変数] 師玉康成

{{DEFAULTSORT:しゆうへんこうとそくはくへんこう}}
[[Category:数学の表記法]]
[[Category:論理記号]]
[[Category:述語論理]]
[[Category:変数 (数学)]]
[[Category:数学に関する記事]]