命題と型は実質的に同じ概念であり、同じ構造を持つ -- これはカリー/ハワード/ランベック対応の主張です。Propositions-as-Types, Types-as-Propositions と表現されることもあります。
ところが、「命題」という言葉は非常に曖昧です。同様に「型」という言葉も非常に曖昧です。不幸中の幸いというか、「命題」と「型」の曖昧性のパターンは同じです。言葉の曖昧性も含めて Propositions-as-Types, Types-as-Propositions というわけです。
「命題」「型」に共通な曖昧性を図にしました。この図をシッカリ目に焼き付ければ、カリー/ハワード/ランベック対応を理解するときの助けになるでしょう。
内容:
「命題」の曖昧性
導入としては「命題とは、真偽が判定できる文である」でいいと思います。この素朴な意味の「命題」を厳密化していくわけですが、異なる厳密化を味噌もクソも一緒に全部「命題」と呼んでしまうことが困るのですよ。
「命題」の用法は*1:
- 曖昧なままに総称的に「命題」を使う。
- 構文論の文脈で、「命題」を論理式の意味で使う。
- 意味論の文脈で、「命題」を真偽値または述語(ここは曖昧)の意味で使う。
- 意味論の文脈で、「命題」を真偽値の意味で使う。
- 意味論の文脈で、「命題」を述語の意味で使う。
これを図示すると次のようです。
説明を追加します。構文論〈syntax〉とは、語彙〈ボキャブラリー〉と文法〈グラマー〉の議論です。文字・名前・記号などから、文法の規則に従って記号的表現を組み上げます。記号的表現は項〈term〉とか式〈expression〉と呼びます。一般的には、項と式は同義語ですが、論理では項〈term〉と論理式〈formula〉を区別しています。構文論を語っている文脈で「命題」が出てきたら、それは論理式のことです。
意味論〈semantics〉とは、記号的表現〈項・式〉が表す対象物のほうを調べる分野です。論理式が表す対象物は、真偽値または述語です。真偽値〈truth value〉とは、とりあえずは古典二値真偽値(つまり、$`\mathrm{True}, \mathrm{False}`$)と理解しましょう。述語〈predicate〉は、なんらかの集合 $`X`$ 上で定義された、真偽値を値とする関数です。
構文論と意味論の両方で使われる曖昧多義語(今は「命題」)があるとき、曖昧性を解消するために、構文論の用語には語尾に「項」、意味論の用語には語尾に「実体」を付けるとする(「カリー/ハワード/ランベック対応とハイティング/ド・モルガン圏」参照)なら、次の用語になります。
- 命題項: 構文論における命題、すなわち論理式のこと
- 命題実体: 意味論における命題、すなわち真偽値か述語
「型」の曖昧性
ほんとに不幸中の幸いなのですが、「型」の曖昧性が、「命題」の曖昧性と同じパターンなので、同じ図が描けます。
「型値〈type value〉」は見慣れない言葉だと思います。「値とみなした型」という意味です。稀に使われますが一般的な言葉ではありません。「真偽値」に対応する言葉として「型値」を採用しました。
型値とは、とりあえずは集合のことだと理解しましょう。型ファミリー〈type family〉は、なんらかの集合 $`X`$ 上で定義された、型値を値とする関数です。型値が集合なら、型ファミリーとはインデックス付き集合族〈indexed family of sets〉にほかなりません。
論理では、構文論と意味論〈モデル論〉をハッキリと分けて議論することが多いですが、型理論では構文論と意味論の区別をハッキリさせないままの議論が多いです。構文論と意味論に分けるのが難しいとか、そもそも構文論だけで意味論は一切考えないとかの事情があります。が、やはりゴッチャにした議論は混乱するので、できるだけ構文論と意味論は分けたほうがいいでしょう。
「真偽値」と「型値」
真偽値と型値に関して次のように書きました。
- 真偽値とは、とりあえずは古典二値真偽値(つまり、$`\mathrm{True}, \mathrm{False}`$)と理解しましょう。
- 型値とは、とりあえずは集合のことだと理解しましょう。
なぜ「とりあえず」かというと、「真偽値」「型値」は、なにかを固定的に指し示す言葉ではないからです。一般化・抽象化された状況で、役割りに付けられた名前なのです。
一般化・抽象化すれば、述語も型ファミリーも関数〈写像〉です*2。述語も型ファミリーも次の形に書けます。
$`\quad f: X \to Y`$
論理では $`f`$ を「述語」と呼び、型理論では $`f`$ を「型ファミリー」と呼ぶ、というだけです。そして、論理では述語 $`f`$ の余域の要素を「真偽値」と呼び、型理論では型ファミリー $`f`$ の余域の要素を「型値」と呼ぶ、というだけです。
歴史・伝統・文化・背景・気持ち・集合のサイズへの違和感*3などを捨ててしまえば、関数・域・余域を分野ごとに違う呼び名で呼んでいただけのことになります(そして、たくさんの同義語があります)。
論理 | 型理論 | |
---|---|---|
関数 $`f`$ | 述語 | 型ファミリー |
域 $`X`$ の要素 | 個体 | パラメータ、インデックス |
余域 $`Y`$ の要素 | 真偽値 | 型値 |
「真偽値」も「型値」も、余域の要素という役割りの名前なので、実体は何であってもかまいません。
- 真偽値の典型的事例は古典二値真偽値だが、それだけに拘ってはいけない。
- 型値の典型的事例は集合だが、それだけに拘ってはいけない。
例えば、直積集合 $`X\times Y`$ 上で定義された $`\mathbf{B} = \{ \mathrm{True}, \mathrm{False}\}`$ に値をとる述語 $`p`$ を考えます。
$`\quad p: X\times Y \to \mathbf{B}`$
これをカリー化した関数 $`p'`$ を考えます。
$`\quad p': X \to \mathrm{Map}(Y, \mathbf{B})`$
$`p'`$ を述語と呼ぶなら:
- 述語 $`p'`$ の域 $`X`$ の要素は個体と呼ぶ。
- 述語 $`p'`$ の余域 $`\mathrm{Map}(Y, \mathbf{B})`$ の要素は真偽値と呼ぶ。
つまり、集合 $`Y`$ 上で定義された述語が、述語 $`p'`$ にとっての真偽値なのです。述語を真偽値と呼ぶのです。それは、「真偽値」が特定のなにかを指しているのではなくて、あくまで役割りの名前だからです。
一方で、真偽値を述語とみなすこともあります。一般的に、集合 $`Y`$ の要素 $`b\in Y`$ に対して、次のような定数値関数を考えることができます。
$`\quad (\lambda\, x\in X. b) : X \to Y`$
論理の文脈では、余域の要素 $`b`$ は真偽値と呼び、関数は述語と呼ぶのですから、定数値関数 $`(\lambda\, x\in X. b)`$ は、真偽値を述語とみなしたものになります。
実際、論理では、真偽値を述語とみなすことは日常的に行います。同様に、型理論でも型値を型ファミリーとみなします。
おわりに
論理でも型理論でも、名指し〈ネーミング〉のメカニズムが曖昧でイイカゲン(よく言えば柔軟で自由)です。「名前がなにかを固定的に名指す」という思い込みを捨てない限り、曖昧でイイカゲン(柔軟で自由)なネーミングシステムと用語運用についていくことは出来ません。
ある意味恐ろしいことですが、曖昧でイイカゲンなシステム・運用に慣れてしまうと、それが便利で心地良くて、イチイチ区別する気など全く消え失せてしまうのです。コワーッ。
追記: 曖昧性の図示テンプレート
「命題」の曖昧性の図と「型」の曖昧性の図は、同じ図を使いまわし出来ました。ということは、次のテンプレートが他の曖昧性の図示にも使える可能性があります。
例えば、小学校で習う自然数の加減乗除を算術〈arithmetic〉と呼ぶことにします。上のテンプレートの疑問符のところに「算術」を入れます。
これは「算術」の曖昧性の図として通用しなくもないでしょう。算術には構文論と意味論があります。算術の構文論で扱う構文的対象物〈syntactic object〉は算術項あるいは算術式(「項」と「式」は同義語)です。一方、算術項〈算術式〉が表す意味は、自然数と自然数を引数・戻り値とする関数(例えば、足し算)です。算術で扱う意味的対象物〈semantic object〉全般が「算術実体」で、それは算術値〈自然数〉と算術関数(足し算など)になります。
次に、「多項式〈polynomial〉」という言葉を、テンプレートの疑問符のところに機械的に入れてみます。
なんか奇妙なことになってしまいました。「多項式項」は「馬から落馬」みたいですが、構文的対象物としての多項式ということだとはわかります。「多項式値」は意味がハッキリしません。多項式の係数のことだとコジツケもできそうですが、コジツケはやめときます。
奇妙な図を修正すれば、次のようです。
「多項式」という言葉を、構文論的文脈で使うときと意味論的文脈で使うことがあり、意味論的文脈での「多項式〉は多項式関数のことだ、ということです。
すべての曖昧性がこのテンプレートで図示できるわけではありません。が、幾つかの曖昧性のパターンと図示テンプレートを準備すれば、曖昧性の分析・理解・視覚化に役立ちそうです。