Propositions-as-Types は、幾度となく話題にしています。ブログ記事だけでなく、口頭での説明もけっこうな回数おこなっています。これがうまく説明できないのですわ。説明が困難な主たる原因は、用語の対応があまりにもグジャグジャで混乱必至なことです。
用語の対応を何度も整理していますが、単語と単語の対応を並べる方法では全く不十分です。グジャグジャ具合が複雑で錯綜しているので、単純な整理など不可能なのです。
最近、「パンダ用法と用語・用法図」で用語・用法図を導入しました。これは、用語に関する問題の分析装置／説明装置となります。用語・用法図を使うことにより、Propositions-as-Types 周辺のグジャグジャを分析・整理してみます。$`
\newcommand{\T}[1]{\text{#1} }
`$
内容：
ハブ記事：
Propositions-as-Types
Propositions-as-Types は、カリー／ハワード／ランベック対応のキャッチフレーズです。「命題〈proposition〉は、型〈type〉とみなせる」、「命題と型は同じようなもんだ」という意味です。命題は型とみなせるので、論理は型理論のなかで展開できることになります。論理は型理論に吸収できる、とも言えますが、そんなこと言うと論理の人が嫌な顔をするでしょう。命題と型は同じようなものなので、論理の手法やフレームワークを型理論に応用することもできます。
論理も型理論も圏論的に定式化できるので、論理・型理論・圏論の三位一体〈トリニティ〉が形成されます。カリー／ハワード／ランベック対応とは、このトリニティを構成する論理・型理論・圏論のあいだの対応のことです。この記事では、論理-型理論の対応を扱うので、圏論は登場しません。
カリー／ハワード／ランベック対応は、理論的には整合的できれいな対応となっているのですが、残念ながら用語の対応がうまくいきません。過去何度も、用語の対応を整理しようと試みました。古い順に過去記事を並べます。
- カリー／ハワード／ランベック対応の辞書
- 続・カリー／ハワード／ランベック対応の辞書
- まだある、カリー／ハワード／ランベック対応の辞書
- カリー／ハワード／ランベック対応の辞書： 推論規則再論
- カリー／ハワード／ランベック対応： チートシート
上記の記事達では、対応する2つの用語を横に並べた対応表（テーブル）を提示しています。結局、それじゃ無理なようです。
記法・図法や定式化についても文句をたれています（以下に過去記事）。
内容・本質とは無関係な部分で障害が多すぎるのですよね。やんなっちゃう。
用語・用法図
用語・用法図は、用語のあいだの相互関係や曖昧多義語の状況を記述するための図です。次の過去記事で導入しました。
用語・用法図の応用例は以下の記事にあります。
例えば、「定数」という語が3つの意味で曖昧に使われていることは次の図で表します。
$`\quad \xymatrix{
{}
&{\T{定数リテラル}}
\\
{\T{【曖昧】定数}} \ar@{|->}[ur] \ar@{|->}[r] \ar@{|->}[dr]
&{\T{自由変数}}
\\
{}
&{\T{定数値関数}}
}
`$
3つの意味を参照するときのために番号を付けることもあります。
$`\quad \xymatrix{
{}
&{\T{定数リテラル}}
\\
{\T{【曖昧】定数}} \ar@{|->}[ur]^1 \ar@{|->}[r]^2 \ar@{|->}[dr]_3
&{\T{自由変数}}
\\
{}
&{\T{定数値関数}}
}
`$
「定数リテラル」は省略されて単に「リテラル」ともいうこと、「定数リテラル」と「固有名」は事実上同義であることも付け加えると次のようになります。
$`\quad \xymatrix{
{}
&{固有名} \ar@{=}[d]
&{}
\\
{}
&{\T{定数リテラル}} \ar@{=}[r] \ar@/^1pc/[r]^{\T{省略}}
&{\T{リテラル}}
\\
{\T{【曖昧】定数}} \ar@{|->}[ur]^1 \ar@{|->}[r]^2 \ar@{|->}[dr]_3
&{\T{自由変数}}
&{}
\\
{}
&{\T{定数値関数}}
&{}
}
`$
「リテラル」という言葉は論理でも使われ（意味は、原子論理式または原子論理式の否定）、コンフリクト〈衝突〉が起きることは次のように図示します。
$`\quad \xymatrix{
{\T{定数リテラル}}\ar@{=}[r] \ar@/^1pc/[r]^{\T{省略}}
&{\T{リテラル}} \ar@{-}[d]|{☓}
\\
{\T{論理リテラル}}\ar@{=}[r] \ar@/^1pc/[r]^{\T{省略}}
&{\T{リテラル}}
}`$
コンフリクトしたままに「リテラル」を使い続ければ、「リテラル」は曖昧多義語となります。
$`\quad \xymatrix{
{}
&{\T{定数リテラル}}
\\
{\T{【曖昧】リテラル}} \ar@{|->}[ur] \ar@{|->}[dr]
&{}
\\
{}
&{\T{論理リテラル}}
}
`$
命題と型
カリー／ハワード／ランベック対応のキャッチフレーズである Propositions-as-Types に登場する2つの語「命題〈proposition〉」と「型〈type〉」の曖昧性を分析しましょう。
「命題」という言葉は、国語辞書的意味で日常でも使われます。この状況を図示すると：
$`\T{用法 1}\\
\quad \xymatrix{
{}
&{\T{日常語「命題」}}
\\
{\T{【曖昧】命題}} \ar@{|->}[ur] \ar@{|->}[dr]
&{}
\\
{}
&{\T{専門用語「命題」}}
}
`$
日常語としては、「課題」「解くべき問題」「提言」「ミッション」といった意味で「命題」が使われたりします。論理の専門用語の「命題」に限定しても曖昧です。
$`\T{用法 2}\\
\quad \xymatrix{
{}
&{\T{真偽値}}
\\
{\T{【曖昧】命題}} \ar@{|->}[ur]^1 \ar@{|->}[r]^2
\ar@{|->}[dr]_3 \ar@{|->}[ddr]_4
&{\T{述語} }
\\
{}
&{\T{論理式}}
\\
{}
&{\T{定理}}
}
`$
「～ は我々にとって永遠の命題である」という言い回しを耳にしました。この場合、「命題」は「課題」、「問題」に置き換えても意味は通じます。この文のニュアンスでは、「解けない課題・問題」、「謎」といった含みがあるのでしょう。
専門用語の「命題」の意味のひとつに「定理」があります。これは、真であることが保証された命題を単に「命題」と呼んでいることになります。日常語でも専門用語でも、真実・事実の意味で「命題」が使われることがあります。
提示された命題〈論理式〉に対する態度も、「命題」の解釈により変わってきます。
- 「命題は偽のときもある」と思っていれば： 真偽を問う、ファクトチェックを試みる。
- 「命題は真だ」と思っていれば： そのまま信じる、鵜呑みにする。何も考えずに受け入れる。
[/追記]
型理論の専門用語としての「型」も同様に曖昧です。
$`\T{用法 3}\\
\quad \xymatrix{
{}
&{\T{単純型}}
\\
{\T{【曖昧】型}} \ar@{|->}[ur]^1 \ar@{|->}[r]^2
\ar@{|->}[dr]_3
&{\T{依存性型} }
\\
{}
&{\T{型項}}
}
`$
「依存性型」という見慣れない言葉を使っているのは、もっと曖昧性がひどい用語「依存型」（後述）と区別するためです。「依存性型」は、「依存性を持つかも知れない型」という意味です。「単純型」は「依存性を持たない型」です。
“用法 3”では、曖昧語「型」の曖昧性解決（$`\mapsto`$ の矢印）の結果として「単純型」がありますが、「単純型」も曖昧語です。集合論的型理論で考える前提で、「単純型」の曖昧性は次のようになります。
$`\T{用法 4}\\
\quad \xymatrix{
{\T{単純型＠3}} \ar@{=}[d]
&{\T{集合}}
\\
{\T{【曖昧】単純型}} \ar@{|->}[ur] \ar@{|->}[r]
\ar@{|->}[dr]
&{\T{自明なファミリー} } \ar@{<->}[u] \ar@{_{(}->}[d]
\\
{}
&{\T{定数値ファミリー}} \ar@{_{(}->}[d]
\\
{}
&{\T{ファミリー}} \ar@{=}[r]
&{\T{依存性型＠3}}
}
`$
上記の図の説明を付け加えます。
- 「単純型＠3」と「依存性型＠3」 は、“用法 3”に出現した「単純型」と「依存性型」という意味です。
- '$`\leftrightarrow`$' は、一対一対応があることを示します。今の場合、集合と自明なファミリーは一対一対応します。
- 自明なファミリーとは、単元集合をインデキシング集合とするファミリー〈集合族〉です。
- '$`\hookrightarrow`$' は、用語が表すモノ達の集合のあいだに包含関係があることを示します。
- 定数値ファミリーとは、関数とみなして定数値関数となるファミリーのことです。すべてのインデックス〈引数〉に対して同じ集合を対応させます。
“用法 4”の図から読み取れることを念の為に書いておくと：
- 集合論的型理論においては、単純型は集合と同義になる。
- 単純型は、自明なファミリーと解釈されることもある（曖昧性）。
- 集合と自明なファミリーは一対一対応する。したがって、集合としての解釈と自明なファミリーとしての解釈は“微妙な差”となる。
- 単純型は、定数値ファミリーと解釈されることもある（曖昧性）。
- 自明なファミリーは特別な定数値ファミリーであり、定数値ファミリーは特別なファミリーである。
- 集合論的型理論においては、依存性型（依存性を持つかも知れない型）はファミリーと同義になる。
- 単純型は、特別なファミリーとして解釈されることもあるので、「単純型は依存性型だ」とも言える。
- 「単純型」と「依存性型」が排他的かどうかは、解釈により変わるので、何ともいえない。
共通な曖昧性構造
前節の“用法 4”と同様な曖昧性は論理側にもあります。論理のほうが幾分単純ですが、あえて“用法 4”と同じレイアウトで描くと以下の図になります。
$`\T{用法 5}\\
\quad \xymatrix{
{\T{真偽値＠2}} \ar@{=}[d]
&{\T{真偽値(狭義)}}
\\
{\T{【曖昧】真偽値}} \ar@{|->}[ur] \ar@{|->}[r]
\ar@{|->}[dr]
&{\T{自明な述語} } \ar@{<->}[u] \ar@{_{(}->}[d]
\\
{}
&{\T{定数値述語}} \ar@{_{(}->}[d]
\\
{}
&{\T{述語}} \ar@{=}[r]
&{\T{述語＠2}}
}
`$
ここで、「真偽値(狭義)」は「真か偽のどちらかの値」という意味で、それ以外の意味を持たない狭い意味での「真偽値」のことです。単に「真偽値」と言うと、曖昧性から複数の意味があり得ます。
「命題」の曖昧性と一緒に図にすると：
$`\T{用法 6}\\
\quad \xymatrix{
{}
&{\T{真偽値(狭義)}}
&{}
\\
{\T{【曖昧】真偽値}} \ar@{|->}[ur] \ar@{|->}[r]
\ar@{|->}[dr]
&{\T{自明な述語} } \ar@{<->}[u] \ar@{_{(}->}[d]
&{}
\\
{}
&{\T{定数値述語}} \ar@{_{(}->}[d]
&{\T{【曖昧】命題}} \ar@{|->}[uul]_{1.1} \ar@{|->}[ul]_{1.2}
\ar@{|->}[l]_{1.3} \ar@{|->}[dl]^{2}
\ar@{|->}[ddl]^{3} \ar@{|->}[dddl]^{4}
\\
{}
&{\T{述語}}
&{}
\\
{}
&{\T{論理式}}
&{}
\\
{}
&{\T{定理}}
&{}
}
`$
「命題」が「定理」の意味でも使われる曖昧性は論理特有ですが、それを除くと、型理論側の曖昧性も同じレイアウトで書けます。曖昧性の構造もある程度は対応しているわけです。
$`\T{用法 7}\\
\quad \xymatrix{
{}
&{\T{集合}}
&{}
\\
{\T{【曖昧】単純型}} \ar@{|->}[ur] \ar@{|->}[r]
\ar@{|->}[dr]
&{\T{自明なファミリー} } \ar@{<->}[u] \ar@{_{(}->}[d]
&{}
\\
{}
&{\T{定数値ファミリー}} \ar@{_{(}->}[d]
&{\T{【曖昧】型}} \ar@{|->}[uul]_{1.1} \ar@{|->}[ul]_{1.2}
\ar@{|->}[l]_{1.3} \ar@{|->}[dl]^{2}
\ar@{|->}[ddl]^{3}
\\
{}
&{\T{ファミリー}}
&{}
\\
{}
&{\T{型項}}
&{}
}
`$
構文論と意味論を区別する
論理でも型理論でもはびこっている悪習として、「構文論と意味論を区別しない」習慣があります。この悪習にも致し方ない面はあります。
- 構文論と意味論をいちいち区別していると、煩雑な用語法・記法になってしまう。
- 構文論と意味論の境界線がハッキリしない場合がある。
しかし、構文論と意味論を区別してない記述を読み解くのはかなりのストレスです。できることなら、構文論と意味論は区別するのが望ましいでしょう。
現実には使われていないルールですが、構文的対象物〈syntactic object〉は「◯◯項」と呼び、意味的対象物〈semantic object〉は「◯◯実体」と呼ぶと約束します。ただし、多少の揺らぎを許容します。
- 構文的対象物は、「◯◯項」以外に「◯◯式」、「◯◯記号」と呼んでもよい。
また、「◯◯項」と「◯◯実体」のあいだは「解釈できる」とラベルされた破線矢印で結ぶことにします。
$`\quad \xymatrix@1{ \T{◯◯項} \ar@{-->}[r]^{\T{解釈できる}} &{\T{◯◯実体}}}`$
例えば：
$`\quad\xymatrix{
{\T{単純型項}} \ar@{-->}[d]^{解釈できる}
&{}
\\
{\T{単純型実体}} \ar@{=}[r]
&{\T{集合}}
}`$
これは、構文的対象物である「単純型項」は、意味的対象物である「単純型実体」と解釈できて、「単純型実体」とは「集合」のことである（「集合」と同義である）と読めます。
同じことは論理にもあって：
$`\quad\xymatrix{
{\T{単純命題項}} \ar@{-->}[d]^{解釈できる}
&{}
\\
{\T{単純命題実体}} \ar@{=}[r]
&{\T{真偽値(狭義)}}
}`$
構文的対象物である「単純命題項」は、意味的対象物である「単純命題実体」と解釈できて、「単純命題実体」とは「真偽値」のことであると読めます。
しかし、実際の用語法は一律なルールで統制されているわけではなくて：
$`\quad\xymatrix{
{\T{命題論理式}} \ar@{=}[d]
&{}
\\
{\T{【不使用】単純命題項}} \ar@{-->}[d]^{解釈できる}
&{}
\\
{\T{【不使用】単純命題実体}} \ar@{=}[r]
&{\T{真偽値(狭義)}}
}`$
「【不使用】」は、一律なルールに関しては整合的であるが実際には使用されてない、ということです。つまり、実際に使用されている用語法にはほとんどルールがなくグジャグジャだ、ということです。
実際に使用しているかどうかは無視して、論理にも型理論にも共通のパターンを抽出して図に描いてみましょう。以下のようになります。
$`\xymatrix@C+1pc{
{◯◯変数記号} \ar@{^{(}->}[dr]
&{}
&{}
\\
{◯◯定数記号\phantom{mm}} \ar@{^{(}->}[r] \ar@{-->}[ddr]_{解釈できる}
&{単純◯◯項} \ar@{^{(}->}[r] \ar@{-->}[dd]_{解釈できる}
&{非単純◯◯項} \ar@{-->}[d]_{解釈できる}
\\
{}
&{}
&{非単純◯◯実体}
\\
{}
&{単純◯◯実体} \ar@{<->}[dr]
&{定数値非単純◯◯実体} \ar@{_{(}->}[u]
\\
{}
&{}
&{自明な◯◯実体} \ar@{_{(}->}[u]
}
`$
「◯◯」に「命題」を入れてみると次のようになります。
$`\T{用法 8}\\
\xymatrix@C+1pc{
{命題変数記号} \ar@{^{(}->}[dr]
&{}
&{}
\\
{命題定数記号} \ar@{^{(}->}[r] \ar@{-->}[ddr]_{解釈できる}
&{単純命題項} \ar@{^{(}->}[r] \ar@{-->}[dd]_{解釈できる}
&{非単純命題項} \ar@{-->}[d]_{解釈できる}
\\
{}
&{}
&{非単純命題実体}
\\
{}
&{単純命題実体} \ar@{<->}[dr]
&{定数値非単純命題実体} \ar@{_{(}->}[u]
\\
{}
&{}
&{自明な命題実体} \ar@{_{(}->}[u]
}
`$
これをこのまま使えたらいいのですが、そういうわけにはいかず、慣用の用語は以下のようになります。
$`\T{用法 9}\\
\xymatrix@C+1pc{
{命題変数} \ar@{^{(}->}[dr]
&{}
&{}
\\
{命題定数} \ar@{^{(}->}[r] \ar@{-->}[ddr]_{解釈できる}
&{命題論理式} \ar@{^{(}->}[r] \ar@{-->}[dd]_{解釈できる}
&{述語論理式} \ar@{-->}[d]_{解釈できる}
\\
{}
&{}
&{述語}
\\
{}
&{真偽値} \ar@{<->}[dr]
&{定数値述語} \ar@{_{(}->}[u]
\\
{}
&{}
&{自明な述語} \ar@{_{(}->}[u]
}
`$
「◯◯」に「型」を入れてもそのままは通用しないので、慣用の用語を入れると以下のようになります。
$`\T{用法 10}\\
\xymatrix@C+1pc{
{型変数} \ar@{^{(}->}[dr]
&{}
&{}
\\
{型定数} \ar@{^{(}->}[r] \ar@{-->}[ddr]_{解釈できる}
&{単純型項} \ar@{^{(}->}[r] \ar@{-->}[dd]_{解釈できる}
&{依存性型項} \ar@{-->}[d]_{解釈できる}
\\
{}
&{}
&{ファミリー}
\\
{}
&{集合} \ar@{<->}[dr]
&{定数値ファミリー} \ar@{_{(}->}[u]
\\
{}
&{}
&{自明なファミリー} \ar@{_{(}->}[u]
}
`$
これでも現実・実際に使われている用語法よりは単純化していて、よくわからないニュアンスや細かい修飾や方言の言い回しが付け加わるかもしれません。
曖昧語「依存型」
「型理論のジャングルに踏み込むための心構えと装備 2/2 // そもそも「依存型」が意味不明」において、「依存型」が曖昧語だと言いました。ここで、曖昧性を分析しておきましょう。
$`\T{用法 11}\\
\quad \xymatrix{
{}
&{}
&{\T{依存性型}}
&{}
\\
{\T{【曖昧】依存型}} \ar@{|->}[urr] \ar@{|->}[drr]
&{}
&{}
&{}
\\
{}
&{}
&{\T{シグマ型またはパイ型}} \ar@{=}[d]
&{}
\\
{}
&{}
&{\bullet}
&{}
\\
{}
&{\T{シグマ型}} \ar@{^{(}->}[ur]
&{}
&{\T{パイ型}} \ar@{_{(}->}[ul]
}
`$
依存性型（依存性を持つかも知れない型）を「依存型」と呼びますが、シグマ型やパイ型のことも「依存型」と呼びます。文脈によって「依存型」がシグマ型のことだと分かっても、「シグマ型」がまた曖昧語です。
$`\T{用法 12}\\
\quad \xymatrix{
{\T{単純型}} \ar@{=}[r]
&{\T{集合}}
\\
{}
&{\T{シグマ型集合}} \ar@{^{(}->}[u]
\\
{\T{【曖昧】シグマ型}} \ar@{|->}[ur] \ar@{|->}[dr]
&{}
\\
{}
&{\T{シグマ型バンドル}}
}
`$
シグマ型が、単なる集合を意味するか、バンドル（2つの集合のあいだの写像）を意味するかは文脈次第です。シグマ型が集合の意味だとすると、集合は単純型なので、シグマ型は単純型です。つまりこの場合、「依存型」と呼ばれた「シグマ型」は単純型（依存性がない型）になります。このような、一見矛盾した言い回しが出現してしまうことは、グジャグジャの用語法においては日常茶飯事です。
そしてそれから
過去に何度も用語対応表を作ろうと試み実際に作ってみましたが、満足のいくものはできませんでした。それもそのはずで、いくら頑張って用語対応表を作ったところで、そんなことで済むほどに事態が単純ではないのです。
どのような曖昧性や揺らぎがあるのか？ どこできれいな対応が破綻するのか？ なぜに対応が歪んでしまうのか？ なども含めて分析し解説しないと理解不可能なのです。
この記事では、カリー／ハワード／ランベック対応そのものを話題にはしませんでした。この記事で説明した曖昧性や揺らぎの知見を前提としてカリー／ハワード／ランベック対応について再度語りたい気持ちはあります。いつになるかは分かりませんが。
