形式的解説
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:09 UTC 版)
変数束縛機構は数学、論理学、計算機科学など様々な分野で使われるが、いずれの場合もそれらは式と変数についてのその分野における全く統語的な属性である。ここでは式を木で表し、その葉ノードに変数、定数、定項などが対応し、葉でないノードに論理演算子が対応するように構成すると考える。変数束縛演算子は論理演算子であり、ほとんど全ての形式言語に存在する。実際、束縛ができない言語は非常に表現能力が低く、使いにくい。束縛演算子 Q {\displaystyle Q} は2つの引数をとる。一つは変数 v {\displaystyle v} 、もう一つは式 P {\displaystyle P} であり、これによって新たな式 Q ( v , P ) {\displaystyle Q(v,P)} が生成される。束縛演算子の意味は、その言語の意味論で提供されるもので、ここでは考慮しない。 変数束縛は三つのものと関連する。一つめは変数 v {\displaystyle v} 、二つめは式内でその変数が現れる場所 a {\displaystyle a} 、三つめは Q ( v , P ) {\displaystyle Q(v,P)} で形成される木の葉でないノード n {\displaystyle n} である。ここでは、変数は葉ノードにあると定義したので、束縛はノード n {\displaystyle n} の下で起きる。 数学における例として、次の関数定義式を考える。 ( x 1 , … , x n ) ↦ t {\displaystyle (x_{1},\ldots ,x_{n})\mapsto \operatorname {t} } ここで、 t {\displaystyle t} は式である。 t {\displaystyle t} には x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} の全部または一部が含まれることがあり、他の変数も含まれることがある。この場合、関数定義が変数 x 1 , … , x n {\displaystyle x_{1},\dots ,x_{n}} を束縛していると言える。 ラムダ計算では、 M = λ x . T {\displaystyle M=\lambda x.T} というラムダ式で、 x {\displaystyle x} は M {\displaystyle M} においては束縛変数、 T {\displaystyle T} においては自由変数である。 T {\displaystyle T} にさらにラムダ式 λ x . U {\displaystyle \lambda x.U} が含まれる場合、 x {\displaystyle x} はこの中で再束縛される。このような入れ子の内側の x {\displaystyle x} の束縛は外側の束縛を覆い隠す。 U {\displaystyle U} における x {\displaystyle x} の出現は新たな x {\displaystyle x} の自由な出現である。 プログラムのトップレベルで束縛された変数は、技術的にはそれが束縛された項の中では自由変数であるが、固定アドレスにコンパイルされるため、特別な扱われ方をすることが多い。同様に計算可能関数に束縛された識別子も技術的にはその本体内では自由変数だが、特別に扱われる。 自由変数を全く含まない項あるいは式を閉項（英: closed term）または閉論理式（英: closed formula）または閉式と呼ぶ。
※この「形式的解説」の解説は、「自由変数と束縛変数」の解説の一部です。
「形式的解説」を含む「自由変数と束縛変数」の記事については、「自由変数と束縛変数」の概要を参照ください。
- 形式的解説のページへのリンク
