自由変数と束縛変数

数学や形式言語に関連する分野（数理論理学と計算機科学）において、自由変数（または自由変項、）は数式や論理式で置換が行われる場所を指示する記法である。この考え方はプレースホルダーやワイルドカードにも関連する。
変数"x" は、例えば次のように書くと 束縛変数（または束縛変項、）になる。
あるいは
これらの命題では、"x" の代わりに別の文字を使っても論理的には全く変化しない。しかし、複雑な命題で同じ文字を別の意味で再利用すると混乱が生じる。すなわち、自由変数が束縛されると、ある意味ではその後の数式の構成をサポートする作業に関与しなくなる。
プログラミングにおいては、自由変数とは関数の中で参照される局所変数や引数以外の変数を意味する。
例.
自由変数と束縛変数を正確に定義する前に、定義をより明確にする例を以下に示す。
次の式
において、formula_6 は自由変数、formula_7 は束縛変数である。結果として、この式は formula_6 の値によって変化するが formula_7 には依存しない。
次の式
において、formula_11 は自由変数、formula_1 は束縛変数である。同様にこの式の値は formula_11 の値によって変化するが、formula_1 には依存しない。
次の式
において、formula_1 は自由変数、formula_17 は束縛変数である。同様にこの式の値は formula_1 の値によって変化するが、formula_17 には依存しない。
次の論理式
において、formula_21 は自由変項、formula_1 と formula_11 は束縛変項である。この論理式の真理値は formula_21 の値によって変化するが、formula_1 と formula_11 には依存しない。
束縛作用素（演算子）.
以下は変数束縛作用素（演算子）である。それぞれ、変数 formula_1 を束縛する。
形式的解説.
変数束縛機構は数学、論理学、計算機科学など様々な分野で使われるが、いずれの場合もそれらは式と変数についてのその分野における全く統語的な属性である。ここでは式を木で表し、その葉ノードに変数、定数、定項などが対応し、葉でないノードに論理演算子が対応するように構成すると考える。変数束縛演算子は論理演算子であり、ほとんど全ての形式言語に存在する。実際、束縛ができない言語は非常に表現能力が低く、使いにくい。束縛演算子 formula_29 は2つの引数をとる。一つは変数 formula_30、もう一つは式 formula_31 であり、これによって新たな式 formula_32 が生成される。束縛演算子の意味は、その言語の意味論で提供されるもので、ここでは考慮しない。
変数束縛は三つのものと関連する。一つめは変数 formula_30、二つめは式内でその変数が現れる場所 formula_34、三つめは formula_35 で形成される木の葉でないノード formula_6 である。ここでは、変数は葉ノードにあると定義したので、束縛はノード formula_6 の下で起きる。
数学における例として、次の関数定義式を考える。
ここで、formula_39 は式である。formula_39 には formula_41 の全部または一部が含まれることがあり、他の変数も含まれることがある。この場合、関数定義が変数 formula_41 を束縛していると言える。
ラムダ計算では、formula_43 というラムダ式で、formula_1 は formula_45 においては束縛変数、formula_46 においては自由変数である。formula_46 にさらにラムダ式 formula_48 が含まれる場合、formula_1 はこの中で再束縛される。このような入れ子の内側の formula_1 の束縛は外側の束縛を覆い隠す。formula_51 における formula_1 の出現は新たな formula_1 の自由な出現である。
プログラムのトップレベルで束縛された変数は、技術的にはそれが束縛された項の中では自由変数であるが、固定アドレスにコンパイルされるため、特別な扱われ方をすることが多い。同様に計算可能関数に束縛された識別子も技術的にはその本体内では自由変数だが、特別に扱われる。
自由変数を全く含まない項あるいは式を閉項（）または閉論理式（）または閉式と呼ぶ。
参考文献.
本項目の一部はGFDLでリリースされているFOLDOCの記述に基づいているが、大部分はその後の編集によるものである。