ラムダ記法とイプシロン記法を組み合わせて関数を定義する - 檜山正幸のキマイラ飼育記 (はてなBlog)

イプシロン記号／イプシロン記法／イプシロン計算については何度か述べたことがあります。今回は、イプシロンを実用的に使うための補助構文について述べます。ここで述べるアイディアは、証明検証系Mizarから拝借しています。ただし、Mizarそのものには触れませんし、Mizarの知識も不要です。

内容：

関数の書き方
イプシロン記法
イプシロン項の基本性質
イプシロン項の不定性
イプシロン項による関数定義
関数の余域を制限する

関数の書き方

中学校で習う1次関数は、

y = 2x + 1

のような形で書かれます。このため、「関数とは、等式の書き方の一種だ」と思っている人もいます。「y = 」の部分は、関数の定義としてはどうでもいい部分です。関数としてエッセンシャルな部分だけを書くにはラムダ記法が便利です。

λx.(2x + 1)

しかし、ラムダ記法にも制限があります。既にある定数、関数、演算子などを組み合わせて新しい関数を構成するにはラムダ記法で十分ですが、命題で条件付けて関数を定義するときはラムダ記法ではうまく表現できません。

例えば、非負平方根を求める関数sqrt（square root から）をラムダ記法で定義するにはどうしたらいいでしょうか。

sqrt := λx.(……)

(……) の部分をどう書きますか？ -- うまく書けないでしょ。

非負平方根は、（通常は）値を求める式やアルゴリズムで定義されるのではなくて、次のような条件で定義されます。

xの非負平方根とは、y² = x かつ y ≧0 であるようなyである。

このような定義を表現するにはイプシロン記法が必要です。

イプシロン記法

イプシロン記法〈epsilon notation〉とは、イプシロン記号'ε'を使った表現方法で、例えば“xの非負平方根”を表すなら、次のように書きます。

εy.(y² = x ∧ y ≧ 0)

イプシロン記法で書かれた式は、英語の冠詞'a'と関係代名詞'such that'に読み替えると、だいたいの意味は解釈できます。

a y such that y² = x and y ≧ 0

冠詞も関係代名詞も自然な日本語に訳すのが難しいのですが、自然でなくてもよいなら：

y² = x かつ y ≧ 0 であるところのどれかひとつのy

'ε'を含んだ式〈expression | 表現〉をイプシロン項〈epsilon term〉と呼び、イプシロン項を含む計算体系をイプシロン計算〈epsilon calculus〉といいます。イプシロン計算は、ヒルベルト〈David Hilbert〉によって始められたので、イプシロン計算で使う'ε'はヒルベルトのイプシロン記号〈Hilbert's epsilon〉とも呼ばれます。

以上の説明でだいたい大丈夫だとは思いますが、イプシロン記法／イプシロン計算についてもう少し詳しいことは、次の記事で説明しています。

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

イプシロン計算の利用例は次の記事にあります。

イプシロン項の基本性質

イプシロン項は、Pを（述語論理の）論理式として、εx.P の形です。ヒルベルトのイプシロン計算では、論理式Pに何の制限もありません。Pが変数xを含んでいなくてもかまいません。x以外の変数がPに出現しても、もちろんOKです。いくつか例を挙げると：

εx.(x = y)
εx.(x = x)
εx.(a ≦ y ∧ y ≦ b)
εa.(a ≦ y ∧ y ≦ b)
εy.(a ≦ y ∧ y ≦ b)

論理式Pに対して、Pに出現する変数xを項Eで置き換えたものを P[x := E] と書きます。角括弧は論理式の一部ではなくて、構文的オペレーターを表すメタ記号です。例を挙げましょう。以下で、記号'≡'は、構文的に等しい（同じ論理式である）ことを示す“メタな等号”です。

(x = y)[y := 1] ≡ (x = 1)
(x = y)[x := 2x + 1] ≡ (2x + 1 = y)
(x = y)[x := y] ≡ (y = y)
(a ≦ y ∧ y ≦ b)[a := x²] ≡ (x² ≦ y ∧ y ≦ b)
(a ≦ y ∧ y ≦ b)[a := 1] ≡ (1 ≦ y ∧ y ≦ b)

イプシロン計算における基本的な公理は次のものです。

∃x.P ⇒ P[x := εx.P] ---(イプシロン項の基本性質)

これは、単一の命題ではなくて、変数xと命題Pの組み合わせごとに作られる無限個の命題を表すパターンです。変数yと命題 (a ≦ y ∧ y ≦ b) の組み合わせだと：

∃y.(a ≦ y ∧ y ≦ b) ⇒ (a ≦ εy.(a ≦ y ∧ y ≦ b) ∧ εy.(a ≦ y ∧ y ≦ b) ≦ b)

イプシロン記号は、ラム計算のラムダ記号や述語論理の限量子と同様に束縛子なので、εで束縛された変数のリネーム（アルファ変換）は自由にできます。以下の論理式では、すぐ上と比べて、y→z, y→w というリネームをしてます。意味は変わりません。

∃y.(a ≦ y ∧ y ≦ b) ⇒ (a ≦ εz.(a ≦ z ∧ z ≦ b) ∧ εw.(a ≦ w ∧ w ≦ b) ≦ b)

イプシロン項の不定性

イプシロン項 εx.P の直感的な意味は：

aが定数（あるいは値そのもの）で、P[x := a] が成立するなら、そのようなaを表す。
P[x := a] が成立するaが存在しないとき、0を表す。

二番目は、「なんで0なんだ？」と突っ込まれそうです。実は何でもいいのです。何でもいいのなら、特に0に固定してもいいだろう、ということです。

一番目の状況では、P[x := a] が成立し、a = εx.P ですから、次の2つの命題が成立しています。

∃x.P
P[x := εx.P]

イプシロン項の基本性質 ∃x.P ⇒ P[x := εx.P] は P[x := εx.P] と同値です（含意命題の前件が真だから後件だけと同じ）。もちろん、基本性質は成立します。

ニ番目の状況では、∃x.P は成立せず、0 = εx.P です。P[x := 0] も成立しません。しかし、∃x.P ⇒ P[x := 0] は真です。含意命題の前件が偽なので、後件が何であっても真なのです。結果として、基本性質が成立します。

以上の解釈から、イプシロン項の基本性質 ∃x.P ⇒ P[x := εx.P] は常に成立する感じがします。

さて、では次の命題は成立するでしょうか？

∃x.(x = x) ⇒ εx.(x = x) = εx.(x = x)

これは、変数xと命題 (x = x) に対するイプシロン項の基本性質です。残念ながら、これが真だとは断言できません。なぜなら、イプシロン項 εx.P は唯一の値を表すわけではなくて、「Pを満たすどれか」という不定性（非決定性）を持つからです。等式の左辺のイプシロン項の値と右辺のイプシロン項の値が同じである保証がないのです。

となると、等式の基本性質 E = E （反射律）が破綻してしまいます。これはとても困ります。対策として、イプシロン項の出現ごとに毎回値が偶発的に選ばれるのではなくて、一度だけ任意選択が発生し、一度決めた値はずっと使い続ける、と決めます。候補が複数あれば、どの値であるかはやはり分からないのですが、出現ごとに違う値という事態はなくなります。

別な考え方として、イプシロン項は不定（非決定的）だとしたまま、論理のほうを変える方法があります。εx.(x = x) = εx.(x = x) の真偽は決まらないので、第三の真偽値を割り当てます。使う論理は三値以上の真偽値を持つ論理になります。話はややこしくなります。

今説明したような事情があるので、イプシロン記法を、何の条件も付けずに使うのはちょっと厄介です。そこで、過去の記事では条件付きでイプシロン記法を使っています。

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

話を煩雑にしないために、∃x.P(x) が保証されているか、∃x.P(x) を前提とする場合にだけ、εx.P(x) を使っていいと約束しましょう。

「論理式内の名前の消去とイプシロン項」：

イプシロン項εx.P(x)の使用条件をさらにきびしくして、次のようにしましょう。

∃!x.P(x)が真であるときに限り、εx.P(x)を使ってよい。

ここで出てきた∃!は、一意的な存在を意味します。

イプシロン項による関数定義

前節最後に引用した「∃!x.P が真であるときに限り、εx.P を使ってよい」という規則は、イプシロン記法を簡単安全に使う良い方法です。この規則に従えば、イプシロン項は定数や関数として扱えます。特別に気を使う必要はありません。

この方法は証明検証系Mizarで採用されています。Mizarでは、イプシロン項が自由に使えるわけではなくて、関数定義の内部でだけ使えます。次のような感じです。



function sqrt := λx.εy.(y² = x ∧ y ≧ 0)

実際のMizarでは、ユーザーにそれがイプシロン項だと意識させないようなシンタックスシュガーがかかっていますが、ここではイプシロン記号をそのまま使い続けます。

さて、上のような定義では「∃!x.P が真であるときに限り、εx.P を使ってよい」という条件を守っているかどうか分かりません。Mizarの方法は、関数定義と同時に ∃!x.P の証明を書かせるものです。次のような感じです。



function sqrt := λx.εy.(y² = x ∧ y ≧ 0)

justification

  existence 存在命題

    存在の証明

  uniqueness 一意性命題

    一意性の証明

end

存在や一意性の命題と証明を書けるようにするには、変数に型が必要です。ここでは、型は集合のことだとして、「変数∈集合」の形で型を明示します。部分集合の型も必要になるので、次の書き方を認めます。

λx∈(R | x≧ 0).εy∈R.(y² = x ∧ y ≧ 0)

ここで、λx∈(R | x≧ 0) は、λx∈{t∈R | t ≧ 0} の略記です。

これで、関数に付随する存在命題と一意性命題を書き下すことができます。



function sqrt := λx∈(R | x≧ 0).εy∈R.(y² = x ∧ y ≧ 0)

justification

  existence ∀x∈(R | x≧ 0).∃y∈R.(y² = x ∧ y ≧ 0)

    存在の証明

  uniqueness ∀x∈(R | x≧ 0).∀v, w∈R.((v² = x ∧ v ≧ 0) ∧ (w² = x ∧ w ≧ 0) ⇒ v = w)

    一意性の証明

end

存在命題と一意性命題は、関数定義の本体部分から機械的に作り出せます。関数定義本体が次のようだとします。

function f := λx∈(X | A).εy∈Y.P

ここで、Aはxを絞り込む条件を表す命題です。すると、存在命題と一意性命題は次の形です。

∀x∈(X | A).∃y∈Y.P
∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)

∀x∈(X | A) という略記を用いなければ：

∀x∈X.(A ⇒ ∃y∈Y.P)
∀x∈X.(A ⇒ ∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w))

関数の余域を制限する

非負平方根の関数sqrtを定義する本体の式は λx∈(R | x≧ 0).εy∈R.(y² = x ∧ y ≧ 0) です。この式を見れば、関数定義を正当化〈justify〉するための存在命題と一意性命題は自動的に書けます。それだけでなく、関数の域〈domain | source domain〉と余域〈codomain | target domain〉も自動的に分かります。この例では：

sqrt:{x∈R | x≧0}→R

関数の域と余域の組み合わせは関数のプロファイルというので、「関数定義の本体は、関数のプロファイル情報を持っている」とも言えます。

さて、関数sqrtの値は負にならないので、余域を非負の実数にしてもよいでしょう。つまり、sqrtのプロファイルを次のようにしよう、ということです。

sqrt:{x∈R | x≧0}→{y∈R | y≧0}

この状況を表現するために、次の書き方を許しましょう。

λx∈(R | x≧ 0).εy∈(R | y≧0).(y² = x ∧ y ≧ 0)

これで関数の余域に関する条件も書けます。しかし勝手に条件を追加していいわけではありません。例えば次はどうでしょうか。

λx∈(R | x≧ 0).εy∈(R | y≦0).(y² = x ∧ y ≧ 0)

関数sqrtの余域を非正の実数に制限しています。こうすると、値の行き場所がなくなり、もはや関数とはいえません。

関数がちゃんと定義される〈well-defined〉ためには、「値が余域内に収まる」という条件も必要です。一般的に言えば、λx∈(X | A).εy∈(Y | B).P の形の定義があれば、次の条件です。

∀x∈(X | A).(P ⇒ B)

sqrtの例では：

∀x∈(R | x≧0).((y² = x ∧ y ≧ 0) ⇒ y≧0)

うまくいかない例では：

∀x∈(R | x≧0).((y² = x ∧ y ≧ 0) ⇒ y≦0)

余域の条件も付けたsqrtの定義をあらためて書けば次のようです。



function sqrt := λx∈(R | x≧ 0).εy∈(R | y≧0).(y² = x ∧ y ≧ 0)

justification

  existence ∀x∈(R | x≧ 0).∃y∈R.(y² = x ∧ y ≧ 0)

    存在の証明

  uniqueness ∀x∈(R | x≧ 0).∀v, w∈R.((v² = x ∧ v ≧ 0) ∧ (w² = x ∧ w ≧ 0) ⇒ v = w)

    一意性の証明

  codomain ∀x∈(R | x≧0).((y² = x ∧ y ≧ 0) ⇒ y≧0)

    余域条件の証明

end

一般的な関数定義の形は次のようになります。



function f := λx∈(X | A).εy∈(Y | B).P

justification

  existence ∀x∈(X | A).∃y∈Y.P

    存在の証明

  uniqueness ∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)

    一意性の証明

  codomain ∀x∈(X | A).(P ⇒ B)

    余域条件の証明

end

余域条件を存在命題のなかに組み入れてしまってもかまいません（そのほうがスッキリします）。



function f := λx∈(X | A).εy∈(Y | B).P

justification

  existence ∀x∈(X | A).∃y∈(Y | B).P

    存在の証明

  uniqueness ∀x∈(X | A).∀v, w∈Y.(P[y := v]∧P[y := w] ⇒ v = w)

    一意性の証明

end

ここで、∃y∈(Y | B).P は ∃y∈Y.(B ∧ P) の略記です。

このような形で関数定義を書いてみるメリットは、関数が関数として成立するにはどんな条件が必要かがハッキリすることです。それらの条件をキチンと保証しない限りは、関数を定義したとは言えないのです。