自由変数と束縛変数

数学、および数理論理学やコンピュータサイエンスなどの形式言語を伴う他の分野では、変数は自由または束縛のいずれかであると言えます。古い書籍の中には、自由変数と束縛変数をそれぞれ実変数と見かけの変数という用語で表すものもあります。自由変数は、式の中で置換が行われる場所を指定する表記法(記号)であり、この式または任意のコンテナ式のパラメータではありません。この考え方は、プレースホルダ(後で何らかの値に置き換えられる記号)、または未指定の記号を表す ワイルドカード文字に関連しています。

コンピュータ プログラミングにおいて、自由変数という用語は、関数内で使用される変数のうち、ローカル変数でもその関数のパラメータでもない変数を指します。この文脈では、非ローカル変数という用語は同義語としてよく使用されます。

対照的に、変数シンボルのインスタンスは、その変数シンボルの値が、談話領域またはユニバース内の特定の値または値の範囲にバインドされている場合、バインドされています。これは、論理量指定子、変数バインド演算子、または変数に許可される値の明示的なステートメント (「... は正の整数」など) を使用することで実現できます。変数シンボルは、少なくとも 1 つの出現がバインドされている場合に全体的にバインドされます。 ^{[1] pp.142--143}同じ変数シンボルが式の複数の場所に現れることがあるため、変数シンボルの一部はフリーである一方、他の出現はバインドされている可能性があります。^{[1] p.78}したがって、「フリー」と「バインド」は、最初に出現に対して定義され、次に式内のその変数シンボルのすべての出現に対して一般化されます。どのように行われるかに関係なく、その値が真理値であるか、計算の数値結果であるか、またはより一般的には関数のイメージ セットの要素であるかに関係なく、変数は式の値が依存する独立変数ではなくなります。 ${\displaystyle n}$

多くのコンテキストでは、談話ドメインは理解されていますが、バインドされた変数の値の範囲が明示的に指定されていない場合は、式を適切に評価するためにドメインを指定する必要がある場合があります。たとえば、両方の変数が論理量指定子によってバインドされている次の式を考えてみましょう。

${\displaystyle \forall y\,\exists x\,\left(x={\sqrt {y}}\right).}$

この式は、との定義域が実数の場合はfalseと評価されますが、定義域が複素数の場合は true と評価されます。${\displaystyle x}$${\displaystyle y}$

「ダミー変数」という用語は、束縛変数を指すために使用されることもあります（コンピュータサイエンスよりも一般的な数学でより一般的です）。ただし、これは統計学、特に回帰分析で使用される、同じ名前ですが関連のないダミー変数の概念と混同しないでください。^{[2] p.17}

自由変数と束縛変数の正確な定義を述べる前に、定義よりもこの 2 つの概念をより明確にする例をいくつか示します。

表現では

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

n は自由変数であり、k は束縛変数です。したがって、この式の値はnの値に依存しますが、依存できる kと呼ばれるものはありません。

表現では

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

y は自由変数であり、x は束縛変数です。したがって、この式の値はyの値に依存しますが、依存できる xと呼ばれるものはありません。

表現では

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

x は自由変数であり、hは束縛変数です。したがって、この式の値はxの値に依存しますが、依存できる hと呼ばれるものはありません。

表現では

${\displaystyle \forall x\ \exists y\ {\Big [}\varphi (x,y,z){\Big ]},}$

zは自由変数であり、xとy は論理量指定子に関連付けられた束縛変数です。したがって、この式の論理値はzの値に依存しますが、依存できるxやyと呼ばれるものはありません。

より広く言えば、ほとんどの証明では束縛変数が使われます。例えば、次の証明は、すべての正の偶数平方が${\displaystyle 4}$

を正の偶数とする。するととなる整数が存在する。 なので、は で割り切れる。${\displaystyle n}$${\displaystyle k}$${\displaystyle n=2k}$${\displaystyle n^{2}=4k^{2}}$${\displaystyle n^{2}}$${\displaystyle 4}$

証明では、 kだけでなくnも全体として束縛変数として使用されています。

次の

${\displaystyle \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}$

は、一般的な変数バインディング演算子です。各演算子は、変数x を何らかの集合Sにバインドします。

これらの多くは、束縛された変数の関数に作用する演算子です。より複雑なコンテキストでは、このような表記は扱いにくく混乱を招く可能性があります。次のように、束縛を明示的にする表記に切り替えると便利です。

${\displaystyle \sum _{1,\ldots ,10}\left(k\mapsto f(k,n)\right)}$

金額または

${\displaystyle D\left(x\mapsto x^{2}+2x+1\right)}$

差別化のため。

変数バインディング メカニズムは、数学、論理学、コンピューター サイエンスのさまざまなコンテキストで使用されます。ただし、すべての場合において、それらは純粋に式と式内の変数の構文上の特性です。このセクションでは、式を、リーフ ノードが変数、定数、関数定数、または述語定数であり、リーフ以外のノードが論理演算子であるツリーで識別することによって構文を要約できます。次に、ツリーを順序どおりにトラバーサルすることで、この式を決定できます。変数バインディング演算子は、ほとんどすべての形式言語で使用される論理演算子です。バインディング演算子 Q は、変数vと式P の2 つの引数を取り、その引数に適用すると、新しい式 Q( v , P ) を生成します。バインディング演算子の意味は言語のセマンティクスによって提供されるため、ここでは考慮しません。

変数バインディングは、変数v、式内のその変数の位置a 、および形式 Q( v , P ) の非リーフ ノードnの 3 つを関連付けます。注: 式内の位置は、構文ツリーのリーフ ノードとして定義します。変数バインディングは、その位置がノードn の下にある場合に発生します。

ラムダ計算では、xは項 の束縛変数でありM = λx. T、 の自由変数です。は で束縛され、 で自由であるとT言います。に部分項が含まれる場合、 はこの項で再束縛されます。 のこのネストされた内部束縛は、外部束縛を「隠蔽」すると言われています。におけるの出現は、新しい の自由出現です。^[3]xMTTλx. UxxxUx

プログラムのトップ レベルでバインドされた変数は、バインドされている条件内では技術的には自由変数ですが、固定アドレスとしてコンパイルできるため、特別に扱われることがよくあります。同様に、再帰関数にバインドされた識別子も、それ自体の本体内では技術的には自由変数ですが、特別に扱われます。

閉じた項とは、自由変数を含まない項です。

数学の例を挙げると、関数を定義する式を考えてみましょう。

${\displaystyle f=\left[(x_{1},\ldots ,x_{n})\mapsto t\right]}$

ここで、tは式です。tには、 x ₁、…、x _nの一部、すべて、またはいずれも含まれない場合があり、他の変数が含まれる場合もあります。 この場合、関数定義は変数x ₁、…、x _nをバインドすると言います。

このように、上記のような関数定義式は、ラムダ計算のラムダ式に類似した変数束縛演算子と考えることができます。他の束縛演算子、例えば和記号は、関数に適用される高階関数と考えることができます。したがって、たとえば、式

${\displaystyle \sum _{x\in S}{x^{2}}}$

の表記として扱うことができる。

${\displaystyle \sum _{S}{(x\mapsto x^{2})}}$

ここで、は 2 つのパラメータ (1 つのパラメータを持つ関数と、その関数を評価するセット) を持つ演算子です。上記の他の演算子も同様の方法で表現できます。たとえば、全称量指定子は、ブール値関数P を(無限の可能性がある) セットSに適用した論理積を評価する演算子と考えることができます。 ${\displaystyle \sum _{S}{f}}$ ${\displaystyle \forall x\in S\ P(x)}$

形式意味論で分析すると、自然言語には自由変数と束縛変数があることがわかります。英語では、he、she、theyなどの人称代名詞は自由変数として機能します。

リサは自分の本を見つけました。

上記の文では、所有代名詞herは自由変数です。これは、前述のLisaまたは他の女性を指す場合があります。言い換えると、her book はLisa の本 (共参照の例) を指す場合もあれば、別の女性の所有する本 (例: Jane's book) を指す場合もあります。herの指示対象が誰であるかは、状況 (つまり、語用論的) コンテキストに従って確立できます。指示対象の同一性は、共参照の下付き文字を使用して示すことができます。ここで、 i は1 つの指示対象を示し、j は2 番目の指示対象 ( iとは異なる) を示します。したがって、 Lisa found her bookという文には、次の解釈があります。

リサ、_私は彼女の本を見つけました_。（解釈＃1：彼女＝リサ）

リサ、_彼女の_Jブックを見つけた。（解釈2：彼女＝リサではない女性）

この区別は純粋に学術的な興味から来るものではありません。言語によっては、実際にher _iとher _jの形式が異なっているからです。たとえば、ノルウェー語とスウェーデン語では、共参照のher _{i を}sinと翻訳し、共参照でないher _{j を}hennesと翻訳します。

英語では共参照の指定は許可されていますが、前の例の両方の解釈が有効であるため、これはオプションです (文法的に正しくない解釈はアスタリスクで示されます)。

リサ、_私は彼女_の自分の本を見つけました。（解釈＃1：彼女＝リサ）

*リサ_{、私は彼女}自身の本を見つけました。（解釈＃2：彼女＝リサではない女性）

ただし、himself、her、themselvesなどの再帰代名詞やeach otherなどの相互代名詞は、束縛変数として機能します。次のような文では、

ジェーンは自分自身を傷つけた。

再帰詞himself は、前述の先行詞、この場合はJaneのみを参照でき、別の女性を参照することはできません。この例では、変数himself は主語の位置に出現する名詞Janeにバインドされています。共索引を示すと、 Janeとhimselfが共索引されている最初の解釈は許容されますが、共索引されていない他の解釈は文法的に誤りです。

ジェーン_は自分を傷つけました。_（解釈その1：彼女自身=ジェーン）

*ジェーン_は自分を傷つけました_j。（解釈その2：彼女自身= ジェーン以外の女性）

共参照結合は、前の形式的説明のセクションで述べたように、ラムダ式を使用して表現できます。再帰文は次のように表現できます。

(λ x . x傷ついたx )ジェーン

ここで、Jane は主語参照引数であり、λx.x hug x はラムダ記法による述語関数 (ラムダ抽象) であり、x は文の意味主語と意味目的語の両方がバインドされていることを示します。これは、JANE が同一人物 であるJANE hug JANEという意味解釈を返します。

代名詞も異なる動作をすることがあります。以下の文では

アシュリーは彼女を殴った。

代名詞her は、Ashley 以外の女性にのみ言及できます。つまり、この代名詞はAshley hit himselfと同じ再帰的な意味を持つことは決してありません。文法的な解釈と非文法的な解釈は次のとおりです。

*アシュリー_{、僕は彼女}を殴った。（解釈その1：彼女＝アシュリー）

アシュリー_{、私は彼女}を殴った。（解釈その2：彼女＝アシュリーではない女性）

最初の解釈は不可能です。文法上、2 番目の解釈のみが許可されます。

このように、再帰詞と相互詞は束縛変数（専門的には照応詞と呼ばれる）であるのに対し、真代名詞は一部の文法構造では自由変数であるが、他の文法構造では束縛できない変数であることがわかります。自然言語に見られる束縛現象は、統語統治と束縛理論にとって特に重要でした（「束縛（言語学） 」も参照）。

• クロージャ（コンピュータサイエンス）
• 組み合わせ論理
• ラムダリフティング
• 名前バインディング
• スコープ（プログラミング）
• スコープ（ロジック）

• トンプソン、サイモン (1991)。『型理論と関数型プログラミング』。ウォキンガム、イギリス: アディソン・ウェスレー。ISBN 0201416670. OCLC  23287456.
• ウルフ、ロバート S. (2005)。数学論理の旅。第 30 巻。アメリカ数学協会。ISBN 978-0-88385-042-8. JSTOR  10.4169/j.ctt5hh94h.

• ガワーズ、ティモシー、バローグリーン、ジューン、リーダー、イムレ、編 (2008)。プリンストン数学コンパニオン。プリンストン、ニュージャージー：プリンストン大学出版局。pp. 15–16。doi :10.1515 / 9781400830398。ISBN 978-0-691-11880-2。JSTOR  j.ctt7sd01. LCCN  2008020450. MR  2467561. OCLC  227205932. OL  19327100M. Zbl  1242.00016。