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

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

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

［参照用 記事］

カリー／ハワード対応に親しむ （誰も書かないCoq入門以前 3）

雑記／備忘

「Coqの証明はカリー／ハワード対応に基づいていて云々」とはよく言われてますが、その本質は真偽値をどう解釈するか？ というあたりじゃないか、と思います。スローガンは「真偽値は、なんだっていいのだ」です。

Coqにおいて、真偽や論理演算（AND、ORなど）をどう考えるかについて書いてみます。「Coqにおいて」と言いましたが、Coqの操作やスクリプトは全然出てきません。背景となる考え方の話です。

内容：

  1. C言語の真偽値
  2. 集合全体を真偽値に使う
  3. 空集合ではない証拠
  4. 論理システムと型システム

関連する記事：

C言語の真偽値

C言語では、真偽値用の型（boolとかbooleanとか）は特になくて、数値型で代用するのが習慣です*1。ゼロは偽で、それ以外の値は真です。

この方法は、なんだかイイカゲンみたい（実際イイカゲン）ですが、カリー／ハワード対応も似たようなことをやっています。{true, false} の二値が標準的な真偽値ですが、なにもそれに拘る必要はないわけで、場合によっては {true, false} とは別な値を使ったほうが都合がいいこともあるのです。

C言語の場合は整数値全体（int）を真偽値に使うのが普通ですが、実数値全体でもいいです。あるいは非負の実数値の集合 {x∈R | x ≧ 0} を真偽値に使ってもいいでしょう。値の全体がどんなものであるかはどうでもよくて、大事なのは次のことです。

  • その値が、真を表すのか偽を表すのかを判断できる。

この判断基準がハッキリしているなら、どんな値を真偽値にしてもいいのです。

非負の数値（整数でも実数でもよい、負の数はダメ）を真偽値に使うと便利なことがあります。新たにAND、ORの論理演算を定義しなくても掛け算と足し算で代用できます。ORに関して考えてみると：

  1. 真 OR 真 = 真
  2. 真 OR 偽 = 真
  3. 偽 OR 真 = 真
  4. 偽 OR 偽 = 偽

非負の数の足し算では次が成立します。

  1. 非ゼロ + 非ゼロ = 非ゼロ
  2. 非ゼロ + ゼロ　 = 非ゼロ
  3. ゼロ　 + 非ゼロ = 非ゼロ
  4. ゼロ　 + ゼロ　 = ゼロ

これは論理ORと同じじゃないですか。ANDと掛け算でも同様な対応が成立します。

ANDとORは既存の掛け算・足し算で済みますが、IMPLY（含意）は次のように定義してやる必要があります。

  • x -> y を if (x == 0) then 1 else y として定義する。

矢印記号「->」は二項演算記号です。C言語（やその他多くの言語）で、「->」は別な意味で使われているのでこのまま使うのはダメでしょうが、仮に演算記号のオーバーロードができるとして話しましょう。

上記の含意の定義を使うと、x -> 0 が、xの否定 !x になることは分かるでしょう。「->」は演算記号なので、(x * y) -> z とか、x -> (y -> z) とかも数値として確定します。そしてその値の真偽値としての解釈が、論理記号を使った（「⊃」は含意演算を表す記号） (x∧y)⊃z、x⊃(y⊃z) の真偽に対応します。非負の数値と足し算・掛け算に含意さえ付け加えれば、特別なブーリアンなんて要らないのです。

集合全体を真偽値に使う

集合の集まりをUとしましょう。U自体は集合になるとは限りませんが、集合論の技法を使えば、Uも集合にすることはできます*2。

Uのなかで、集合論的な構成が自由にできるとします。具体的に書けば：

  1. A, B∈U ならば、A×B∈U （直積）
  2. A, B∈U ならば、(A + B)∈U （直和）
  3. A, B∈U ならば、BA∈U （指数集合）
  4. 0∈U 0は空集合
  5. 1∈U 1は単元集合

このような性質を持つ集合の集まりを宇宙（universe）と呼びます。宇宙の定義は他に色々ありりますが、ここでは積・和・指数の演算が自由にできるような集合論的な舞台だとします。指数 BA とは関数集合のことで、BA = {f | fはAからBへの関数} です。

さて、宇宙全体を真偽値だと考えましょう。C言語の「数値が真偽値」の場合と同じように、真偽の解釈規則を与えます。

  1. 空集合は偽とみなす。
  2. 他の集合はすべて真とみなす。

集合Aが真偽値として真であるとは、Aが空でないことです。別な言い方をすると、Aが要素を持つことです。「真偽値として真である」を単に「真である」と端折って言ってしまうと：

  • 集合Aが真であるとは、Aが非空であること。

丁寧に言えば：

  • 集合Aが真であるとは、Aが少なくとも1つの要素を持つこと。

こうなります。

真偽をこのように定義すると、論理演算ANDとORは集合の直積と直和で代用できます。ORに関しては、数値の足し算と同じように次が成立します。

  1. 非空集合 + 非空集合 = 非空集合
  2. 非空集合 + 空集合　 = 非空集合
  3. 空集合　 + 非空集合 = 非空集合
  4. 空集合　 + 空集合　 = 空集合

ANDと直積の関係も同様です。

IMPLY（含意）は、集合の指数で代用できます。含意の定義を完全に書き下してみます。

  1. pが真、qが真ならば、p⊃q は真。
  2. pが真、qが偽ならば、p⊃q は偽。
  3. pが偽、qが真ならば、p⊃q は真。
  4. pが偽、qが偽ならば、p⊃q は真。

集合の指数（関数集合）に関して次が成立します。

  1. Aが非空集合、Bが非空集合ならば、BA は非空集合。
  2. Aが非空集合、Bが空集合ならば、BA は空集合。
  3. Aが空集合、Bが非空集合ならば、BA は非空集合。
  4. Aが空集合、Bが空集合ならば、BA は非空集合。

空集合から任意の集合への関数（写像）は常に1つだけあることに注意してください。このため、B空集合はBが何であれ空ではないのです！

「真偽値はなんであってもかまわない、問題はその解釈だ」という立場にたてば、集合を真偽値として、「真は非空集合、偽は空集合」と約束すれば、それで何の問題も起きません。論理演算は集合演算で完全に代用できます。その関係をまとめておきましょう。

普通の真偽値 集合を使った真偽値
二元集合 {true, false} 宇宙U
trueまたはfalse 宇宙Uに属する集合
true 非空な集合ならなんでもよい
false 空集合
AND（連言） 直積
OR（選言） 直和
IMPLY（含意） 指数（関数集合）

この対応が、ほぼカリー／ハワード対応の内容です。

空集合ではない証拠

引き続き、「集合Aが真偽値として真である」を「集合Aが真である」と言うことにします。では、集合Aが真であることを確実に保証するにはどうしたらいいのでしょうか？ 集合Aに所属する要素をひとつ示してしまえば、それで済みです。

「真である」とは「非空である」ことですから、「要素を少なくとも1つ持つ」ことであり、現に目の前に要素を出されたら反論のしようがありません。このとき、ほんとに確実な要素を出す必要があります。極めて具体的な要素を見せる必要があります。

Aが真であることを示す、極めて具体的で文句の付けようがない要素を、Aが真である証拠（witness）と呼びます。証拠である要素を、Aの住人（inhabitant/habitant）と呼ぶこともあります。「空き家でない証拠は、そこに住んでいる住人だ」というわけです。

Aの住人aと、Bの住人bが具体的に与えられているとき、直積集合A×Bの住人は、デカルトペア (a, b) として具体的に与えることができます。このことを別な言い方で述べると：

  • Aが真である証拠aと、Bが真である証拠bがあれば、A×Bが真である証拠が得られる。

上記の内容を次の図式で表すことができます。

     a∈A        b∈B
  ----------------------
      (a, b)∈A×B

横線（マイナスの並び）の上段が現在得られている事実だとすると、下段がそれから確実に推論されます。

通常の命題論理の推論図（下の図）と比較してみましょう。

     A        B
  -----------------[∧の導入]
        A∧B

同じ形をしてますね。違いは、

  1. A、Bを集合と呼ぶか命題と呼ぶかの違い。
  2. 直積記号「×」と論理AND記号「∧」の違い。
  3. 真である証拠（住人）を添えるかどうかの違い。

一番目・ニ番目の違いは呼び名と記号の違いですから本質的ではありません。三番目の違いは次のように考えることができます。

  • 集合を真偽値に使う場合は、「Aが真である」ことを保証するために証拠を添えて「a∈A」と書く。
  • 命題論理では、単に「A」と書いただけで「Aが真である」の意味となる。

そう考えると、どちらの図式も次の内容だと言えます。

  • 「Aが真である」と「Bが真である」（上段）が既に分かっているならば、「AとBの直積（または連言）が真である」（下段）が言える。

単なる「A」と「Aが真である」の区別が気になる人は、片側シーケント「⇒A」を導入して、次の推論図に代えてみればいいでしょう。

    ⇒A     ⇒B
  -----------------[∧の導入]
      ⇒A∧B

今はANDに関する推論だけを取り上げましたが、命題論理における論理計算（AND、OR、IMPLY）と真偽の判定は、集合における集合計算（直積、直和、指数）とその非空性の判定にそっくり置き換え可能なのです。

論理システムと型システム

前節で、論理の真偽値計算が、集合の宇宙内の集合計算で代用できることを述べました。直積、直和、指数に加えて依存積という集合演算を導入すると、述語論理も集合計算でシミュレートできるようになります。つまり、依存積を持つ宇宙内では、述語論理（のモデル）を構成できるのですね。

「命題」という言葉は人により場合により解釈が変わってしまい曖昧な言葉ですが、確か高校あたりでは「真偽が判定できるもの」と説明していたような気がします（最近の高校のことは知りませんけど）。となると、集合も非空か空かで真偽が判定できるので「命題」と呼んでもよいでしょう。CoqのPropは、命題とみなした集合の宇宙のことです。

集合の場合、それが真であることを保証する証拠（witness）は住人（habitant）だと言いました。カリー／ハワード対応では、この証拠を証明（proof）だとみなします。このことは、なかなか納得がいかないと思います。なので、今は深入りしませんが対応表だけ示します。

論理 集合論
命題 集合
全称命題 依存積
命題が真 集合が非空
命題の証明 集合の住人（証拠）

a∈A という記法は、aがAの住人であることです。住人がいればAは非空なので、命題としてAは真となります。集合とその要素（住人）という言葉の代わりに、型とそのインスタンスと言い換えても意味は変わりません。また、a∈A を a:A と書いて「aの型はAである」と読んでも同じことですね。

そうすると、対応表は次のように拡張できます。

論理 集合論 型理論
命題 集合 型
全称命題 依存積 依存型
命題が真 集合が非空 型がインスタンスを持つ
命題の証明 集合の住人（証拠） 型のインスタンス

論理の証明を遂行するために、型理論の実装系（型システム）を利用できる根拠がこの対応です。

後半は急ぎ足で大雑把な話になってしまいました。まだ『？』な感触が残るとは思いますが、安全なプログラムを書くためのメカニズムとして開発された型システムが、証明を行う論理システムとしても使えるらしいことが少しはイメージできたでしょうか。

*1:C99でブーリアンのサポートが入ったようです。

*2:Uをグロタンディーク宇宙、またはグロタンディーク宇宙のサブクラスと考えましょう、ということです。