カリー／ハワード対応〈Curry-Howard correspondence〉は、複数（2つ以上）の分野、あるいは複数の理論体系のあいだの同型対応です。2つの分野のあいだにカリー／ハワード対応がある場合、これら2つの分野は事実上同じものとみなせます。有名なカリー／ハワード対応の事例は「連言含意論理 ←→ 単純型付きラムダ計算」の対応です（後述）。
2つの分野のうち片方について知っているなら、カリー／ハワード対応に伴う翻訳を施せば、もう一方の分野についても知ることができます。異なる2つの分野は同一の概念的対象物について異なる言葉で語っているだけです。内容は同じなので、新たに学ぶべきことは言葉使い、つまり“語学”です。語学の勉強もけっこう大変ですが、内容の学習は節約できます -- だって同じ内容だから。
2つの分野の両方とも知らない場合でも、カリー／ハワード対応を意識すれば、かなり効率的に学習できます。語学の学習は省略できませんが、内容の重複学習を避けることができます。そして、2つの分野をバラバラな別物としてではなく、一体化した統合体として把握できます。
2つの分野の両方とも知っている場合、それらの緊密な関係性を知ることにより、両分野への理解はより深いものとなるでしょう。カリー／ハワード対応の観点から両分野を吟味することにより、認識の歪みや不備を矯正することができます。
カリー／ハワード対応に圏論が絡んでいるとき、僕はカリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉と呼んでいます。圏論的発想を組み入れると、カリー／ハワード対応はより整合的で精密な構造・構成を手に入れます。圏論により強化されたカリー／ハワード対応がカリー／ハワード／ランベック対応です。
この記事では、確率論のなかのカリー／ハワード／ランベック対応の一例について述べます。この記事は以下の記事と一緒に読んでいただくことを想定しています。が、読む順番は自由です。どっちが先でもかまいません。そのため、2つの記事に重複記述があります。ご了承ください。
- 関連する記事： カリー／ハワード対応のための記法・図法
この記事で述べる「確率論のカリー／ハワード／ランベック対応」は、僕が行う有料オンライン・セミナー「ロマ数トレラン」のテーマです。1月16日に（場合によっては1月23日も）、セミナー内容を紹介する無料オンライン・ガイダンスをします。それについてはこの記事の最後に記します。興味がある方は、案内を先に御覧ください。
[追記]料金、日時などの具体的な情報はオンライン・セミナー「ロマ数トレラン」無料ガイダンス回のご案内にあります。セミナー参加申し込み方法も書いてあります。[/追記]
内容：
- カリー／ハワード／ランベック対応の典型例
- 構文論と意味論
- モデルとしてのデカルト閉圏
- マルコフ圏とカリー／ハワード／ランベック対応
- 確率的論理とアブダクション
- 「ロマ数トレラン」オンライン・セミナーのご案内
カリー／ハワード／ランベック対応の典型例
「連言含意論理 ←→ 単純型付きラムダ計算」の対応は、カリー／ハワード対応のプロトタイプ的〈典型的かつ基本的〉事例なので、やはりこれから話を始めましょう。
連言含意論理とは、連言（論理的「かつ」）と含意（論理的「ならば」）だけを持つ論理体系〈演繹体系 | deduction system〉です。選言（論理的「または」）、否定（論理的「ではない」）は考えないので、通常の論理（古典論理）に比べれば単純で小さい論理です。
単純型付きラムダ計算は、静的で強い型システムを持つ関数型プログラミング言語だと思えばいいです -- と言っても分かりにくいですね。現存する実用的関数型プログラミング言語の原型となっている計算系ですが、メチャクチャに単純・小規模なものです。型の構成法として、直積型〈ペア型〉と関数型〈指数型 | アロー型〉が使えます。
この2つの理論体系は同一の構造を持ち、双方向の同型対応があります。
連言含意論理と単純型付きラムダ計算が持つ共通構造を抽象化すると、デカルト閉圏と呼ばれる圏論的構造となります。「連言含意論理、単純型付きラムダ計算、デカルト閉圏」の三者間の対応は、圏論が使われるので（冒頭で言った言葉の約束により）カリー／ハワード／ランベック対応です。カリー／ハワード／ランベック対応の場合、三者が対等ではなく、次の図のような感じになります。
デカルト閉圏は、より抽象度が高いという意味で上位にあり、連言含意論理と単純型付きラムダ計算は、上位のデカルト閉圏により統制されています。同じ傘の下にいるという意味で、連言含意論理と単純型付きラムダ計算は共通性・同型性を持つわけです。「連言含意論理 ←→ 単純型付きラムダ計算」という対応は、デカルト閉圏を経由するので間接的となります（直接的に対応付けることも可能ですが）。
次節以降で、この状況をもう少し詳しく見ましょう。
構文論と意味論
連言含意論理も単純型付きラムダ計算も、構文の体系〈形式的体系 | formal system〉として導入されます。論理式やラムダ式〈ラムダ項〉と呼ばれる記号列がどんなものであるか、どのように操作するかを最初に学びます。記号列の機械的操作である証明（形式的証明*1）や計算に慣れてきたら、記号列に意味を与える意味論〈セマンティクス〉を学びます。
連言含意論理の意味論は次のように展開します； 集合 を固定して、そのベキ集合〈power set〉を
とします。論理式〈formula〉と呼ばれる記号列の意味は、
の要素、つまり
の部分集合だとします。一番簡単な例は
のときで、
となるので、
は二値ブール集合（二値は真と偽に対応）とみなせます。
構文と意味の対応（の基本部分）は次のようです*2。
| 構文 | 意味 |
|---|---|
| 真を表す記号 ' |
全体集合 |
| その他の原子記号 | |
| 連言記号 ' |
集合演算 |
| 含意記号 ' |
集合演算 |
ここで、集合演算 は次のように定義します。
単純型付きラムダ計算の意味論では、型（を表す記号列）には集合を割り当て、ラムダ式（関数を表す記号列）*3には実際の関数を割り当てます。次のようですね。
| 構文 | 意味 |
|---|---|
| 単位型を表す記号 ' |
単元集合 |
| その他の基本型の名前 | 特定の集合 例： |
| 直積型記号 ' |
集合の直積 |
| 関数型記号 ' |
集合の指数 |
同じ記号であっても、表の左欄の はラムダ計算の記号体系のなかにある記号で、表の右欄の
は実際の集合と集合演算です。
今これ以上詳しくは述べませんが、構文の領域から意味の領域への対応が意味論（が定義する割り当て）です*4。この状況を図示すると：
ここで、 は、単なるベキ集合ではなくて、集合演算と順序を備えた構造で、ハイティング代数〈Heyting algebra〉のミート部分となっています（ハイティング代数の定義は割愛）。
は、集合と関数〈写像〉からなる圏です。
モデルとしてのデカルト閉圏
前節で「意味の領域」と言った構造はモデル〈model〉とも呼びます。連言含意論理のモデルは、ハイティング構造*5を備えたベキ集合であり、単純型付きラムダ計算のモデルは集合圏なわけです。
ひとつの構文の領域（形式的体系）に対して複数のモデルを考えることができます。前節で述べたモデルは、比較的標準的と思われるモデルでした。
さて、連言含意論理のモデルであるベキ集合と、単純型付きラムダ計算のモデルである集合圏は異なるものですが、共通性を持ちます。それは、どちらもデカルト閉圏であることです。言い方を換えると、（ハイティング構造を備えた）ベキ集合と集合圏の共通性を、圏論的構造として抽象化したものがデカルト閉圏です。
このことを踏まえて、カリー／ハワード／ランベック対応の状況を再び図示すると：
モデルであるベキ集合と集合圏は、一般論としてのデカルト閉圏の議論に吸収されます。連言含意論理と単純型付きラムダ計算が異なるのは構文においてです。構文の違いとは、日本語と英語が異なるように、語彙、文法、背景文化などの違いです。デカルト閉圏という一般的共通構造を抑えてしまえば、あとは“語学”と“翻訳”の問題です。
先に、「ひとつの構文の領域（形式的体系）に対して複数のモデル」が可能だと言いました。それならば、連言含意論理の構文（形式的体系）に対して集合圏をモデルにすることは可能でしょうか？ もちろん可能です。そのときは次のような状況になります。ひとつのモデルに複数の構文ですね。
複数の構文が併存していることは無駄なのでしょうか？ そうではありません。構文ごとにメリット／デメリットがあります。自然言語の場合と同様、構文（言語）ごとに、文化や考え方は違うので、それぞれに固有の価値があります。
マルコフ圏とカリー／ハワード／ランベック対応
確率論のなかにもカリー／ハワード／ランベック対応を見出すことができます。確率論において、前節のデカルト閉圏の役割を果たす圏はマルコフ圏です。マルコフ圏については次の記事で書きました。
マルコフ圏が定式化されたのは比較的最近です。マルコフ圏により、確率的理論を統制する圏論的フレームワークが与えられました。マルコフ圏の登場で、確率論におけるカリー／ハワード／ランベック対応が記述可能になったとも言えます。
デカルト閉圏がそうであったように、マルコフ圏も抽象的〈公理的〉な圏の種別です。確率的文脈においてマルコフ圏の具体事例が出てきます。可測空間とマルコフ核の圏が最も重要な具体事例です。が、可測空間とマルコフ核の圏を十分に調べるには測度論・積分論が必要でだいぶ難しい。
可測空間とマルコフ核の圏より扱いやすく簡単な圏があります。有限集合を対象としてマルコフテンソルを射とする圏は線形代数だけで扱えます。そしてこのマルコフテンソルの圏は、可測空間とマルコフ核の圏の部分圏（有限離散確率圏）とみなすことができます。“マルコフテンソルの圏＝有限離散確率圏”を FinDiscStoc（finite discrete stochastic category）と書くことにします。
マルコフ圏とその具体事例であるFinDiscStocを含むカリー／ハワード／ランベック対応は次のようになります。
上図で、右側のテンソル構文による形式的体系は、マルコフテンソル計算〈Markov tensor calculus〉と呼んでいいでしょう*6。マルコフテンソル計算の意味論は、マルコフ圏（の具体事例である）FinDiscStocに値を取ります。この部分は基本的に線形代数の話です。
図の左側の論理構文による形式的体系とは何でしょうか？（次節）
確率的論理とアブダクション
FinDiscStoc（より一般には任意のマルコフ圏）をモデルにするような論理を確率的論理と呼ぶことにしましょう（漠然過ぎる呼び名ですが）。この意味の確率的論理は非常に弱い論理で、古典論理のような強い推論はできません。しかし、通常の論理（古典論理）とは甚だしく違っていて、面白い性質を持っています。
通常の論理（古典論理）では許されない推論をアブダクションと呼びます。アブダクションの典型例は、以下のような推論です。
A ならば B である B である よって A である
これがダメな推論であることは、A を「xは2の倍数」、B を「xは4の倍数」とすると：
「xは2の倍数」ならば「xは4の倍数」である 「xは4の倍数」である よって 「xは2の倍数」である
しかし、日常生活ではこのテの推論を使っています。黒い鳥を見てカラスだろうと推測することはあるでしょう。
「鳥xはカラス」ならば「鳥xは黒」である 「鳥xは黒」である よって 「鳥xはカラス」である
このような日常的推論の背後には確率的論理があると思われます。経験によって形成される次のような確率テーブルで推論しているのでしょう、たぶん*7。詳細は「アブダクションと確率的推論」を参照してください。
| カラスである | カラスでない | |
|---|---|---|
| 黒い | 60% | 12% |
| 黒くない | 0% | 28% |
マルコフ圏をそのまま論理のモデルにすることは、最も素朴なアプローチで、確率的論理の定式化にはより洗練されたアプローチもあります。が、素朴な方法でも、日常のアブダクションの幾つかに意味を与えることができます。
「ロマ数トレラン」オンライン・セミナーのご案内
この記事で述べたようなテーマで「ロマ数トレラン」オンライン・セミナーを行います。とはいえ、この記事は概念的背景の話であり、セミナーの内容はもっと具体的です。ストリング図をたくさん描いて、行列・テンソルの計算をたくさんしましょう、といったことになると思います。
1月30日(土曜)18時が第1回で、原則2週間おき1回2時間半、全10回です。告知とより詳し予定などを述べるために第0回（無料）を1月16日(土曜)18時にZoomで行います。Zoom URLなどのお知らせは、このブログやロマ数サイト http://romanticmathnight.org/でも行いますが、Twitterのフォローが確実で手っ取り早いと思います（次のリンクをクリック）。
[追記]料金、日時などの具体的な情報はオンライン・セミナー「ロマ数トレラン」無料ガイダンス回のご案内にあります。セミナー参加申し込み方法も書いてあります。[/追記]
*1:我々が通常行う数学的証明のことではなくて、形式的体系内部で遂行される機械的な操作のことです。
*2:スコットブラケットを使えば、、
のように書けます。
*3:ラムダ式、あるいはラムダ項は、記号'λ'から始まる式だけではありません。例えば、型付きの変数だけでもラムダ式です。
*4:意味論という分野も意味論が定義する割り当ても、両方とも「意味論」と呼びます。なんでも圏論を使う人は、意味論を関手と考えます。
*5:構成素〈素材〉の組 で、ハイティング代数の条件〈公理〉の一部を満たすもの。
*6:"tensor calculus"を「テンソル解析」と訳す場合は微積分が関係しています。ここでの "tensor calculus" は文字どおりの計算で、主にテンソルの掛け算を扱います。
