Free variables and bound variables

ウィキペディア

自由変数と束縛変数

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 10:09 UTC 版)

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

変数x は、例えば次のように書くと 束縛変数（または束縛変項、英: bound variable）になる。

全ての $x$ について $(x+1)^{2}\geq x^{2}+2x+1$ が成り立つ。

あるいは

$x^{2}=2$ となるような $x$ が存在する。

これらの命題では、x の代わりに別の文字を使っても論理的には全く変化しない。しかし、複雑な命題で同じ文字を別の意味で再利用すると混乱が生じる。すなわち、自由変数が束縛されると、ある意味ではその後の数式の構成をサポートする作業に関与しなくなる。

プログラミングにおいては、自由変数とは関数の中で参照される局所変数や引数以外の変数を意味する。

例

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

次の式

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

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

次の式

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

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

次の式

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

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

次の論理式

$\forall x\ \exists y\ \varphi (x,y,z)$

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

束縛作用素（演算子）

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

$\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$

形式的解説

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

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

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

$(x_{1},\ldots ,x_{n})\mapsto \operatorname {t}$

ここで、$t$ は式である。$t$ には $x_{1},\dots ,x_{n}$ の全部または一部が含まれることがあり、他の変数も含まれることがある。この場合、関数定義が変数 $x_{1},\dots ,x_{n}$ を束縛していると言える。

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

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

自由変数を全く含まない項あるいは式を閉項（英: closed term）または閉論理式（英: closed formula）または閉式と呼ぶ。

参考文献

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

関連項目

• 変数 (数学)
• 変数 (プログラミング)
• クロージャ
• 生成 (数学)
• スコープ (プログラミング)

外部リンク

• 束縛変数と自由変数 師玉康成

Weblio日本語例文用例辞書

「Free variables and bound variables」の例文・使い方・用例・文例

• 私はまず、この点をAmandaに確認します。
• 11月21日にHolyoke Bar and Grillで、Pete Laurenの退職パーティーが開かれることをお知らせします。11 月10 日までにお返事をください。
• 来月のロンドンへの出張のために、飛行機の便を予約して、Southland銀行の近くの宿泊施設を手配してもらえますか。
• 年次監査を行うために、Bradford and Partnersの会計士たちが10 月10 日の午前10 時に当社を訪ねてくる予定です。
• 一般に公開されたことのない、Ruth and Steve Whitmanの個人コレクションの絵画を含む、およそ120 点の作品が展示される。
• Ruth and Steve Whitmanを紹介すること。
• Conteeさんは、昨年Hope and Learnの会長に就任された、受賞歴のあるミュージカル女優さんです。
• Hope and Learnは遠隔地に学校を建設する資金を集める慈善団体です。
• Hope and Learnへの寄付は、この夜会の最後に集めます。
• 気をつけの姿勢で立つ (⇔stand at ease).
• 等位[対等]接続詞 《対等の語句を接続する and, but など》.
• 等位接続詞 《and, but, or, for など; ⇔subordinate conjunction》.
• 連結接続詞 《and など》.
• 【文法】 相関接続詞 《both…and; either…or など》.
• 蒸留酒, 火酒 《brandy, gin, rum, whiskey など》.
• 英国陸軍士官学校 《Berkshire の Sandhurst /sndhɚːst｜‐həːst/ にある》.
• (英国の)運輸省. the Ministry of Education(, Science and Culture) (日本の)文部省.
• 中央裁判所施設 《London の Strand 街にある高等法院の建物》.
• 弱形 《and の /ən/など》.
• 《主に米国で用いられる》 ＝ 《主に英国で用いられる》 the Committee of Ways and Means 歳入委員会.