カリー／ハワード／ランベック対応とハイティング／ド・モルガン圏

カリー／ハワード／ランベック対応については、このブログ内で何度も言及しています。

• このブログ内 ハワード の検索結果

論理／型理論／圏論の三者のあいだに、精密で綺麗な対応があります -- それがカリー／ハワード／ランベック対応です。カリー／ハワード／ランベック対応はとても重要な概念だし、実用的な意義もあります。

しかしながら、この綺麗な対応がなかなか伝わらないようです。対応が見えにくくなっている大きな原因は、構造が綺麗に対応していても、言葉や記号は対応してないことです。論理／型理論／圏論の三者において、まったく違った呼び名・書き方・言い回しが使われています。

言葉や記号が違っていても、単純な翻訳ルールがあればいいのですが、例外と場合分けが多いゴチャゴチャしたルールになってしまいます。だったら、翻訳なんてしなければいいじゃないか -- まったくそのとおりです！ 呼び名・書き方・言い回しに囚われずに、ダイレクトに概念を捉える人にとっては、翻訳は不要です。概念・構造の同型性を直接的に観測できるでしょう。

が実際には、表層的な呼び名・書き方・言い回しの違いに惑わされて、概念・構造の同型性が見えにくくなっているケースが多いようです。この記事では、呼び名・書き方・言い回しの悪影響を軽減する工夫について述べます。$`
\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
\newcommand{\hyp}{\text{－} }
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{ \text{ in } }
%\newcommand{\ot}{\leftarrow}
%\newcommand{\op}{\mathrm{op}}
\newcommand{\Imp}{\Rightarrow }
`$

内容：

• 追記

関連記事：

• 「命題」と「型」の曖昧性を図示

PAT PAT

カリー／ハワード／ランベック対応、特に論理と型理論の対応の原理を端的に表すキャッチフレーズとして「PAT PAT」があります*1。次の言葉の頭文字〈イニシャリズム〉です。

　　Propositions-as-Types, Proofs-as-Terms

このキャッチフレーズは次の対応があることを指摘しています。

論理	型理論
命題	型
証明	項

このキャッチフレーズは本質を付いたものでまったく正しいのですが、言葉づかい〈用語法〉の歪み・崩れが既に現れています。

「命題」という語が曖昧多義語なことは「Propositions-As-Typesを曲解しないで理解するために // 「命題」を排除したい！」で指摘しました。「命題」には次の用法があります（国語辞書的用法は除く）。

1. 真偽値という意味
2. 述語という意味
3. 論理式という意味
4. 定理という意味

「命題」の曖昧性に関する分析は「「命題」の曖昧性から前層意味論へ」に書いています。

型理論側の「型」と「項」もアンバランスな用法です。「型理論の「代入」の分析」から引用しましょう。

次のようなアンバランスな規約が多数派です。

1. 「ソート〈型〉」はソート項〈型項〉を意味する。
2. 単に「項」と言ったら、それはオペレーション項〈関数項〉を意味する。
3. 「ソート」が（文脈により）ソート実体を意味することもある。
4. 「項」が（文脈により）オペレーション実体を意味することもある。

構文論的対象物には語尾に「項」または「式」を付けて、意味論的対象物には語尾に「実体」を付けて区別することにして、先の対応表を構文論と意味論に分けて書き直しましょう。

論理の構文論	型理論の構文論
論理式	型項
証明項	関数項

論理の意味論	型理論の意味論
述語	型実体
証明実体	関数実体

これでもまだ一貫性が欠如しているので、次の言い方を使うことにします。

論理の構文論	型理論の構文論
命題項〈論理式〉	型項
定理の証明項	関数の計算項

論理の意味論	型理論の意味論
命題実体〈述語〉	型実体
定理実体	関数実体

曖昧多義語の「命題」を復活させていますが、語尾の「項」と「実体」で、論理式のことか述語のことかは区別しています。命題と真偽値の関係は後で述べます。定理と命題は別な意味で使います。

慣用とは違いますが、次の規則により構文論的対象物〈syntactic object〉と意味論的対象物〈semantic objects〉の区別をします。

• 構文論的対象物の語尾には「項」または「式」を付ける。
• 意味論的対象物の語尾には「実体」を付ける。

「項／式」も「実体」も末尾に付いてないときの解釈は：

1. 前もってデフォルトルールが決まっている。例えば、「型＝型項」とか「関数＝関数実体」とか。
2. 構文論と意味論で共通な話をしている。例えば、「型」を型項と解釈しても型実体と解釈しても通用する。
3. 文脈ごとに意味が変わる。

三番目の「文脈」を把握する負担を軽減する工夫がこの記事の内容です。

命題と真偽値

曖昧多義語「命題」を使っても、接尾辞（語尾に付ける言葉）「項／式」「実体」を使えば、次のような区別ができます。

• 命題項 ＝ 論理式（ラムダ記法も併用する）
• 命題実体 ＝ 述語

述語は、なんらかの（個体領域〈domain of individuals〉とか論域〈domain of discourse〉と呼ばれる）集合 $`X`$ 上で定義された真偽値を値とする関数です。真偽値の集合を $`\mbf{B} = \{ \mrm{True},\mrm{False}\}`$ とすると、述語 $`p`$ は次のように書けます*2。

$`\quad p: X \to \mbf{B} \In \mbf{Set}`$

特に、$`X = \mbf{1}`$ と置いた場合は：

$`\quad p: \mbf{1} \to \mbf{B} \In \mbf{Set}`$

単元集合 $`\mbf{1}`$ を域（個体領域／論域）とする述語（余域が $`\mbf{B}`$ である関数）は、$`\mbf{B}`$ の要素と同一視できます。

$`\quad \mrm{Map}(\mbf{1}, \mbf{B}) \cong \mbf{B}`$

この同一視のもと〈under this identification〉では、真偽値は述語〈命題実体〉の特別なものだとみなせます。したがって、次の言い方は間違いではありません。

• 真偽値は命題実体〈述語〉である。

しかし、次は間違いです*3。

• 命題実体〈述語〉は真偽値である。

次なら間違いになりません。

• 命題実体〈述語〉は真偽値のこともある。

構文論側では：

• 「真偽値定数記号は命題項〈論理式〉である」は間違いではない。
• 「命題項〈論理式〉は真偽値定数記号である」は間違い。
• 「命題項〈論理式〉は真偽値定数記号のこともある」は間違いではない。

曖昧多義語「命題」を使っても、次の点に注意すれば、コミュニケーションはとれます。

• 構文論的対象物である「命題項 ＝ 論理式」か、意味論的対象物である「命題実体 ＝ 述語」かを区別する。
• 古典二値真偽値の集合 $`\mbf{B}`$ と、ポインティング関数の集合 $`\mrm{Map}(\mbf{1}, \mbf{B})`$ は適宜同一視する。

「真偽値」の曖昧性

真偽値を古典二値真偽値に限定しておけば、前節の約束により、曖昧多義語「命題」も適切に運用できます。

しかし、真偽値がいつでも古典二値真偽値とは限りません。真偽値の概念も一般化・抽象化されるのです。「一般化された真偽値」とか「抽象化された真偽値」とか言ってみても、一般化・抽象化の方法がイッパイあるので、結局ハッキリしません。各人が、自分が知っている「一般化された真偽値」「抽象化された真偽値」だと思い込んでコミュニケーションが破綻します。

人により、「一般化・抽象化された真偽値」で三値論理／四値論理／ファジー論理／確率的論理などを思い浮かべるかも知れません。が、今はそのような非古典論理は扱いません。古典論理で成立する法則を温存したいのです*4。それらの法則が成立しないと、普通に論理をするには辛すぎます。

曖昧に「一般化・抽象化された真偽値」とか言うのはやめて、欲しい法則が成立するような代数的・圏論的構造を公理的に提示することにします。

我々の「一般化・抽象化された真偽値」が居住する代数的・圏論的構造をハイティング／ド・モルガン圏〈Heyting-De Morgan category〉と呼ぶことにします（詳細は次節）。今の文脈における、一般化・抽象化された真偽値とは、ハイティング／ド・モルガン圏の対象のことです。

ハイティング／ド・モルガン圏

ハイティング圏〈Heyting category〉*5は、直和付きデカルト閉圏〈Cartesian closed category with direct sum〉の別名〈同義語〉だとします。実際、ハイティング代数〈Heyting algebra〉は、やせた直和付きデカルト閉圏にほかなりません。

直和はデカルト余積〈Cartesian coproduct〉なので、直積と直和の両方を持つ圏は双デカルト圏〈biCartesian category〉とも呼ばれます。なので、言い方を変えると、ハイティング圏は内部ホム〈指数〉を持つ双デカルト圏です。

ハイティング圏 $`\cat{C}`$ を、記号の乱用で次のように書きます。

$`\quad \cat{C} = (\cat{C}, \times, 1, [\hyp, \hyp], +, 0)`$

ここで：

• $`(\cat{C}, \times, 1, [\hyp, \hyp])`$ は、デカルト閉圏になっている。
• $`(\cat{C}, +, 0) `$ は、余デカルト圏になっている。

直和と直積のあいだに分配法則が成立することは証明できそうですが、最初から仮定しておいてもいいでしょう。

$`\text{For }A, B, C\in |\cat{C}|\\
\quad A\times (B + C) \cong A\times B + A \times C \In \cat{C}\\
\quad (A + B)\times C \cong A\times C + B \times C \In \cat{C}
`$

ハイティング圏において、次の3つの記号を定義します。

1. 否定演算 $`\lnot`$
2. プレ順序関係 $`\le`$
3. 同値関係 $`\equiv`$

否定は、内部ホム〈指数〉と始対象を使って次のように定義します。

$`\text{For }A \in |\cat{C}|\\
\quad \lnot A := [A , 0]
`$

プレ順序関係 $`\le`$ （エンテイルメント関係）は次のとおりです。

$`\text{For }A, B \in |\cat{C}|\\
\quad ( A \le B) := (\cat{C}(A, B) \ne \emptyset)
`$

同値関係 $`\equiv`$ は、$`\le`$ を使って定義します。

$`\text{For }A, B \in |\cat{C}|\\
\quad ( A \equiv B) := (A \le B \land B \le A)
`$

プレ順序関係 $`\le`$ と同値関係 $`\equiv`$ は、ハイティング圏に限らず任意の圏に対して定義可能なことに注意してください。

以上の準備のもとで、ド・モルガンの法則〈De Morgan's laws〉は次のように書けます。

$`\text{For }A, B \in |\cat{C}|\\
\quad \lnot (A + B) \equiv (\lnot A) \times (\lnot B)
`$

（上の同値だけではダメでした。すぐ下の追記を参照。）

ド・モルガンの法則が任意の対象 $`A, B`$ に対して成立するハイティング圏がハイティング／ド・モルガン圏〈Heyting-De Morgan category〉です。

[追記]
選言〈disjunction〉（直和）に対するド・モルガンの法則 $`\lnot (A + B) \equiv (\lnot A) \times (\lnot B)`$ は、どうもハイティング圏の公理だけから出そうです。つまり、あえて公理として要求する必要性はなさそう。

連言〈conjunction〉（直積）に対するド・モルガンの法則 $`\lnot (A \times B) \equiv (\lnot A) + (\lnot B)`$ のほうが問題で、ハイティング圏の公理からは出ないようです。ということは反例があるんでしょうが、思いつきません（後で調べよう）。

という事情で、「連言〈直積〉の否定が否定の選言〈直和〉に展開できる」という公理がド・モルガン性の主張になります。人名形容詞の順番は「ド・モルガン／ハイティング〈De Morgan-Heyting〉」が普通のようです。確かに、ド・モルガン性を持つハイティング圏ということで、ド・モルガン／ハイティング圏のほうがシックリくるかも。

ド・モルガン性を持つハイティング圏（ド・モルガン／ハイティング圏）で、古典論理ができるか？ というと、そうはいかないようです。古典論理といえば二重否定の法則や排中律が象徴的ですが、これらはド・モルガン／ハイティングの公理系からは出てこないらしい。ウーム、ややこしいな。

ハイティングの公理系のなかで、二重否定の法則と排中律は同値で、どちらかを仮定すると、ド・モルガンの法則が証明可能なので、ハイティングの公理系に例えば排中律を追加すれば、古典論理をする環境が整います。

排中律は成立しないけどド・モルガンの法則は使えるハイティング圏は面白そうな気がします。しかし実用性を考えると、結局排中律を入れて古典論理になっちゃうかなー。
[/追記]

ハイティング／ド・モルガン圏の実例

集合圏は、通常の直積、直和、指数〈関数集合〉によりハイティング／ド・モルガン圏になります。同値関係 $`\equiv`$ は、すべての集合達を、空集合かそうでないかの2つの同値類に分類します。

古典二値真偽値の集合 $`\mbf{B}`$ は、適切な演算と順序関係でブール代数になりますが、順序集合から圏を作る手順で圏とみなすと、ハイティング／ド・モルガン圏になります。習慣として、違う記号一式を使います。

• $`\times`$ の代わりに $`\land`$
• $`+`$ の代わりに $`\lor`$
• $`[\hyp, \hyp]`$ の代わりに $`\Imp`$
• $`1`$ の代わりに $`\mrm{True}`$（あるいは $`\top`$）
• $`0`$ の代わりに $`\mrm{False}`$（あるいは $`\bot`$）

使う記号が違うだけで、$`\mbf{Set}`$ も $`\mbf{B}`$ もハイティング／ド・モルガン圏なのです。したがって、集合も古典二値真偽値も、どちらも「ハイティング／ド・モルガン圏の対象」と言えます。ハイティング／ド・モルガン圏の対象を“真偽値”と呼ぶ約束をするなら、「集合は“真偽値”」だし「古典二値真偽値は“真偽値”」です。

なんらかの（個体領域とか論域と呼ばれる）集合 $`X`$ 上で定義された“真偽値”を値とする関数を述語と呼ぶなら、述語の定義は次のようです。

• $`\cat{C}`$ をハイティング／ド・モルガン圏だとして、$`p : X \to |\cat{C}|`$ の形の写像が述語〈predicate〉

$`\cat{C} = \mbf{Set}`$ の場合なら、述語 $`p`$ は：

$`\quad p: X \to |\mbf{Set}| \In \mbf{SET}`$

$`\cat{C} = \mbf{B}`$ の場合なら、述語 $`p`$ は：

$`\quad p: X \to |\mbf{B}| \In \mbf{Set}`$

普段、順序集合や圏としての $`\mbf{B}`$ と、台集合である単なる集合 $`\mbf{B}`$ を区別してませんが（悪習！）、$`\mbf{B}`$ をハイティング／ド・モルガン圏だとするなら、対象の集合（二元集合）は $`|\mbf{B}|`$ です。

まとめ

今回扱った言葉は、「命題」と「真偽値」の2つです。

• 「命題」は、命題項〈論理式〉と命題実体〈述語〉を意味することがある。
• 単元集合上で定義された命題実体〈述語〉は、真偽値と同一視可能である。
• 「真偽値」は、古典二値真偽値を意味する場合と、一般化・抽象化された真偽値を意味する場合がある。
• カリー／ハワード／ランベック対応を論じる文脈では、一般化・抽象化された真偽値とは、ハイティング／ド・モルガン圏の対象だと定義する。
• 古典二値真偽値も、ハイティング／ド・モルガン圏の対象だとみなせる。

*1:「パット・パット」と読めばいいでしょう。

*2:集合 $`X`$ 上の述語が、$`p : X^n \to \mbf{B}`$ を意味することもあります。

*3:「述語のことも真偽値と呼ぼう」と言われればそれまでのことで、用語が指すものが何であるかはあくまでも集団内の約束なのです。

*4:若干は譲歩するとしても、直観主義論理の法則は欲しいところです。

*5:「Heyting の Hey は『ヘイ』だ」「Heyting の g は発音されないか、かすかに『ク』に聞こえるくらいだ」と聞いたことがあります。「ヘイティンク代数」という表記も見たことがあります。が、一般的な「ハイティング」にします。