自由変数と束縛変数
変数束縛機構は数学、論理学、計算機科学など様々な分野で使われるが、いずれの場合もそれらは式と変数についてのその分野における全く統語的な属性である。ここでは式を木で表し、その葉ノードに変数、定数、定項などが対応し、葉でないノードに論理演算子が対応するように構成すると考える。変数束縛演算子は論理演算子であり、ほとんど全ての形式言語に存在する。実際、束縛ができない言語は非常に表現能力が低く、使いにくい。束縛演算子 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} である。