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

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

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

［参照用 記事］

イプシロン計算ってなんですかぁ？ こんなもんですよぉ

雑記／備忘

ラムダ計算は、計算モデルとしてだけでなく、手計算の実際的手段としても役立ちます。しかし、通常使われる各種変換（アルファ、ベータ、イータ、デルタ）ではうまく計算が進まないときがあります。例えば、gがfの逆関数のとき、f(g(y)) は y に簡約されるのだけど、f(g(y)) ⇒ y って簡約規則は通常のラムダ計算ではうまく定式化できません（いや、できるかもしれませんが、僕にはうまい方法が思いつきません）。

そこで、ラムダ計算に加えてイプシロン計算も使うとよさそうです。でも、イプシロン計算は、ラムダ計算ほどにポピュラーではないですね。簡単な例でイプシロン計算を紹介しましょう。

内容：

イプシロン記号とイプシロン項

負の数-1とか、無理数√2とかを導入するとき、次のような定義をしましたよね。

  • -1とは、x + 1 = 0 であるようなx
  • 2の平方根とは、x2 = 2 であるようなx（のひとつ）
  • √2とは、x2 = 2 かつ x ≧ 0 であるようなx

ここで、「…であるようなx」という表現が登場します。これを、εx.(…) と書きます。つまり、

  • -1 = εx.(x + 1 = 0)
  • 2の平方根 = εx.(x2 = 2)
  • √2 = εx.(x2 = 2 ∧ x ≧ 0) （∧は論理ANDです）

「…であるようなx」、εx.(…) の「…」の部分は、なにかxを含む命題です。その命題をP(x)と書くと、「P(x)であるようなx」を、εx.P(x) と書くことになります。

もうこれで、イプシロン記号とイプシロン項の説明は終わりです。念のためちゃんと言っておけば：

変数xの名前（綴り）に意味はないので、εx.P(x) を εy.P(y) と書いても同じです。これは、ラムダ式のアルファ変換と同じです。イプシロンの直後に付く変数（イプシロン変数と呼びましょう）は束縛変数です。束縛機構も、述語論理式やラムダ式と同じです。

イプシロン項の意味

εx.(x + 1 = 0) の場合、このイプシロン項が-1を表すことは直観的に明かです（これ以上は詮索しない）。しかし、εx.(x2 = 2) のとき、x2 = 2 であるxは２つあります。どっちを表すのでしょう？ また、xが実数の範囲で動くとき、εx.(x2 = -1) は何も表しません。「xの範囲を複素数まで拡げるんだ」って？ では、εx.(x ≠ x) ならどうでしょう？

実は、P(x)がどんな命題でも、εx.P(x) の意味を定義できるのですが、話を煩雑にしないために、∃x.P(x) が保証されているか、∃x.P(x) を前提とする場合にだけ、εx.P(x) を使っていいと約束しましょう。

そうすると、εx.P(x)、つまり「P(x)であるようなx」は1つ以上存在します。問題は、複数のxがあるときどれを選ぶかです。この問題の答は「どれでもいいから、どれか1つを選ぶ」です。そんなアヤフヤな定義で大丈夫か？ 大丈夫です。問題ありません。

大事なことは、P(x) のxのところに εx.P(x) を代入したら、それは真な命題になることです。つまり、次の形の命題は常に成立します。

  • P(εx.P(x))

例を挙げると：

  • εx.(x + 1 = 0) + 1 = 0
  • (εx.(x2 = 2))2 = 2

これは、次のことを言っています。

  • (-1) + 1 = 0
  • (√2)2 = 2

もっとも、二番目は √2 じゃなくて -√2 だと思ってもかまいません。+√2 と -√2 を区別する必要はありません。どっちにしろ「二乗すれば2」ですから。

イプシロン項に名前を付けておいて、その名前を使って書くと見やすくなります。

  • a = εx.P(x) ならば P(a)

(-1)や√2という定数は、イプシロン項に付けられた名前だと解釈できます*1。ですから、何か変な記号、たとえば「♂」を持ち出して、

  • ♂ = εx.(x + 1 = 0)

とすれば、♂は通常の-1とまったく同じ役割を演じます。

イプシロン項が定義する関数

命題Pのなかに、変数xだけでなく、変数tも含まれているとします。この状況のときPを、P(x, t) と書いていいでしょう。さらに、tの値によらず、∃x.P(x, t) が保証されている（または前提する）としましょう。そのとき、イプシロン項εx.P(x, t)を使っていいことになります。

例を出しましょう。

  • εx.(x + t = 0) -- x + t = 0 であるようなx
  • εx.(x2 = t) -- x2 = t であるようなx

これって何だろう？ 少し考えてみてください。

考えました？ εx.(x + t = 0) は -t のことですよね。εx.(x2 = t) は √t、、、、とは断定できませんが、tごとに √t か -√t のどっちを対応させる関数です。もっとハッキリスッキリさせたいなら、

  • εx.(x2 = t ∧ x ≧ 0 ∧ t ≧ 0)

と書けば、√t （t ≧0 ）を表すと言えますね。

一般に、ある適当な範囲のtに対して、∃x.P(x, t) であるときには、イプシロン項 εx.P(x, t) は、tの関数を表すとみていいのです。その関数をfとするなら、

  • f(t) = εx.P(x, t) （tは ∃x.P(x, t)である範囲を動く）

自由変数がtだけでなくて、t1, t2, ..., tn といっぱいあっても話は同じで、

  • f(t1, t2, ..., tn) = εx.P(x, t1, t2, ..., tn)

として、関数fを定義できます。このfは（Pに対する）スコーレム関数と呼ばれています。

イプシロン記号を使うイプシロン記法は、スコーレム関数にいちいち名前を付けずに直接表記する方法です。

例題：gがfの断面（セクション）であること

f:X→Y が関数で、どんなy∈Yに対しても f(x) = y となるxが存在することは保証されているとします（fが全射ってこと）。つまり、∃x.(f(x) = y)。P(x, y) ≡ (f(x) = y) と置くと、このP(x, y)の変数xに関するイプシロン項 εx.P(x, y) が作れます。

εx.P(x, y)、より具体的には εx.(f(x) = y) は変数yに関する関数gを表します。

  • g(y) = εx.(f(x) = y)

g(y)を言葉で説明すれば、

  • g(y)とは、f(x) = y であるようなxの（どれだか分からないが）ひとつ

です。

εx.P(x, y) に関しては、P(εx.P(x, y), y) が成立します。具体的に書けば：

  • f(εx.P(x, y)) = y

g(y) = εx.(f(x) = y) を使って置き換え（代入）すれば：

  • f(g(y)) = y

これだけでは、gがfの逆関数とは断定できませんが、gはかなり逆関数に近いものです。gとfは「『円周率は3』についてキッチリ考えてみる -- EPペアの例として」に出てきたEPペアです。gが埋め込み（E）、fが引き込み（射影 P）です。ただし、全射fが先に与えられたときは、fに対するgを断面（セクション）と呼んだりします。選択関数とも言いますね。なんだかイッパイ言葉があって（引き込み＝射影、埋め込み＝断面＝選択関数＝スコーレム関数）ややこしいですが、f(g(y)) = y が頻繁に登場して重要なんだってことです。

f(g(y)) ⇒ y のような簡約規則はラムダ計算では導入しにくいのですが、gをイプシロン項として書いておいて、P(εx.P(x, y), y) を簡約規則とみなすと計算がうまくいくようです。もっともこれは経験則なので、ラムダ計算とイプシロン計算を混ぜたような形式的なモデルがうまく作れるかどうかはよくわかりません。命題Pの形に制限を付けないと、計算が止まりそうにないですね。

なんかシマリがない終わり方ですが、以上、イプシロン計算の簡単な紹介でした。

*1:±√2 という記号表現は、εx(x2 = 2) に付けられた名前だと解釈できます。