このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

束縛子(binder)

とある論文に"binder"という言葉が出てきました。文房具のバインダーじゃありません。束縛子とでも訳せば良さそうです。束縛子が何であるかを厳密に説明するのはけっこう面倒なので、例をいくつか出します。例から一般的概念を推測できるでしょう。

述語論理で出てくる限量子(量化子)は束縛子の例です。より具体的には、全称限量子∀と存在限量子(特称限量子)∃は束縛子です。これらの記号は、直後に変数を伴って、その後に続く論理式内の変数を束縛します。∀x.F、∃x.F のとき、論理式F内の変数xは束縛変数になります*1。自由変数を含む式に構文的に作用して、自由変数を何らかの意味で束縛する記号的作用素が束縛子ってことになります。

もうひとつ典型的な束縛子はラムダ記号λです。λx.E によって、式E内の変数xを束縛します。束縛子により束縛された変数は、リネームしてもかまいません。ラムダ計算ではリネームをアルファ変換と呼びますが、リネーム可能であることは、どんな束縛子/束縛変数でも持つ共通の特性です。

イプシロン記号εも束縛子です。限量子と同じように、論理式Fに対して εx.F を作れます。

集合の内包的表記法 {x | F} もイプシロン記号と似た束縛子になっています。論理式Fを、真偽値を値とする関数の表現と考えると、ラムダ式 λx.F が定義する関数は、集合 {x | F} の特性関数になっています。部分集合と特性関数を同一視するなら、内包的表記法はラムダ束縛と同じことです。

式Eで定義される関数の最小不動点を表す μx.E も束縛子です。最大不動点なら νx.E ですね。これらは、ラムダ束縛を省略した書き方とみなせるので、本質的な束縛子はラムダ記号です; μx.E ≡ μ(λx.E)、νx.E ≡ν(λx.E)。

積分記号∫、総和のΣ、総積のΠなども束縛子記号です。極限 limx→∞f(x) のlimも束縛子で、この例のxが束縛変数になります。

「束縛子」という言葉を使うと、色々な構文的作用素の共通性を言い表すことができて便利です。

*1:正確に言えば、自由に出現しているxだけが束縛の対象です。