カリー／ハワード対応には、ある種の主張が伴います。その主張とは次のようなタイプのものです。
- 歴史的に別々に発展してきた異なる分野が扱っている概念的対象物が、実は同じものだ。
複数の分野のあいだの同型性を主張してるんですね。そんな同型を与える対応を、カリー／ハワード対応、あるいはカリー／ハワード同型と呼びます。
典型的なカリー／ハワード対応には、単純型付きラムダ計算と連言含意論理の同型対応があります。さらにデカルト閉圏を含めた三分野のあいだの同型性もあります*1。他にも、カリー／ハワード対応の事例は色々と在ります。
カリー／ハワード対応（のひとつ）を理解してしまうと、その対応／同型性は自明なように思えます。しかし、自明に見えるまでには様々な困難・障害があります。同型対応で結び付けられる異なる分野は、異なる用語法／異なる記法を使用しているので、異なる言語（文化も含む）間の“翻訳”が必要になります。この翻訳作業はなかなかに大変で、それだけで疲弊してしまうことがあります。
異なる言語・文化のあいだの翻訳を、できるだけ効率的に低コストで遂行するにはどうしたらいいのでしょう？
内容：
- 関連する記事： 確率論のカリー／ハワード／ランベック対応
ラムダ計算と論理
冒頭で触れた「単純型付きラムダ計算 ←→ 連言含意論理」という同型対応を念頭に話をします。ラムダ計算と論理は、まったく異なる言語・文化を持ちます。概念的には同一なものを異なる名前で呼び、概念的に同一なことを違う記法で表現します。
論理とラムダ計算のカリー／ハワード対応では、以下のように対応付けをします。
| 連言含意論理 | 単純型付きラムダ計算 |
|---|---|
| 命題〈論理式〉 | 型 |
| 連言命題 | 直積型 |
| 含意命題 | 関数型〈function type〉 |
| 真を表す命題 | 単位型 |
| 証明 | 関数（を表す項） |
| 含意導入 | ラムダ抽象 |
使っている標準的記法も異なります。
| 連言含意論理 | 単純型付きラムダ計算 |
|---|---|
| 連言〈論理AND〉 |
直積型 |
| 含意 |
関数型 |
| 真 |
単位型 |
カリー／ハワード対応を述べるには、論理とラムダ計算の中間的・中立的な用語法・記法をはさむと便利です。そのような、中間的・中立的、あるいは一般的な用語法・記法を圏論から借りましょう。
| 連言含意論理 | 単純型付きラムダ計算 | 圏論 |
|---|---|---|
| 命題〈論理式〉 | 型 | 対象 |
| 連言命題 | 直積型 | 直積対象 |
| 含意命題 | 関数型 | 指数対象 |
| 真を表す命題 | 単位型 | 単位対象 |
| 証明 | 関数 | 射 |
| 含意導入 | ラムダ抽象 | カリー化 |
原則的には、圏論の用語・記法を使い、圏の特定事例として“論理の圏”と“ラムダ計算の圏”を考えればスッキリします。が、些細な事にように見えて、根が深くタチが悪い問題があります（次節）。
矢印記号の問題
圏論では、矢印記号「→」は、f:A → B in C のように、射の域と余域を示すために使います。矢印の両側に対象を置いた A → B という形は、射 f のプロファイル〈profile〉といいます。
型付きラムダ計算（というよりむしろ関数型プログラミング言語）でも A → B の形を使いますが、これはプロファイルではなくて関数型（関数を要素とする型）です*2。圏論では BA または [A, B] と書いて矢印を使うことはありません*3。
論理における矢印「→」の使い方は幾つかの流儀があって：
- 含意記号に矢印「→」を使うことがある。これは、ラムダ計算（関数型プログラミング言語）と同じ使い方。
- シーケントに矢印「→」を使うことがある。これは、圏論と同じ使い方。
「シーケント」とは、圏論のプロファイルの、論理における呼び名です（分野によって呼び名は異なります）。
圏論の用語・記法を使う原則なら、矢印「→」はプロファイルに使うことになりますが、後々ラムダ計算／関数型プログラミング言語／証明支援系などの話をしたいなら、矢印を“関数型＝含意命題＝指数対象”に予約しておいたほうが得策です。
となると、プロファイル記述には別な記号、例えば二重矢印「⇒」を割り当てることになります。皆さんご存知でしょうが、「⇒」は含意によく使われる記号です。一方圏論では、「⇒」は2-射〈2-セル〉のプロファイル記述に使われます。
少数の記号を各分野で取り合っているので、どう塩梅しても丸くは収まらないのです（競合・衝突しまくり）。エイヤッと決めてしまえばそれでオシマイだし、実際そうするしかありません。ですが、今まで見慣れ／使い慣れていた記号に別な意味・使用法を与えられると、その違和感・抵抗感・ストレスは相当なものがあり、これで疲弊・挫折してしまう人がいます。
カリー／ハワード対応の話は過去に何度もしていますが、用語・記法の激しい変更に耐えることは、想像以上にストレスフルなようです*4。とはいえ、異なる複数分野を扱うなら、必然的に見慣れない用語・記号は出てくるし、いつもとは違った用語・記号を強制される事態も生じます。
ここから先では、次のように矢印記号を使うことに決めます*5。誰かが違和感・抵抗感・ストレスを感じようとも何かに決めないと話が進みませんから。
- 「→」は、含意／関数型／指数対象を作る記号とする。
- 「⇒」は、シーケント／プロファイルを作る記号とする。
圏論の f:A → [B, C] は、f::A ⇒ (B → C) と書くことになります。ダブルコロンにした理由は後で説明します。
証明図の問題
論理では、形式化された証明を表すために証明図と呼ばれる図式を使います。例えば、A, B, A → (B → C) という3つの仮定から、C という結論を得る証明は次のような証明図で表します。
A A → (B → C)
-----------------
B B → C
--------------
C横棒は推論規則と呼ばれ、この場合は2本ともモーダスポネンス〈modus ponens〉という推論規則を表しています。日本語で書くなら次のようでしょう。
A である A ならば「B ならば C」である
---- よって（モーダスポネンスにより） -----
B である B ならば C である
---- よって（モーダスポネンスにより） ----
C である証明図は、通常の組版技術のなかで、証明の2次元構造を表現するために工夫された図法です。1次元の文字列であるテキストより遥かにマシですが、問題点・欠点もあり僕は推奨しません。
さて、カリー／ハワード対応から言えば、証明は関数と同じ（少なくとも同型対応する）概念です。であるなら、証明図に対応する関数図があってもよいはずですが聞いたことありません。圏論では？ と言えば、射を表す各種図式は無闇と使われています*6。なかでもストリング図は直感（直観？）に訴える優れた図法です。
証明も関数も射も一律にストリング図で表す、というのはとても良いアイディアです。伝達手段として欠陥が多いテキスト記法と自然言語では、カリー／ハワード対応の要点がうまく伝わるはずもなく、学習者を苦しめます。ストリング図をふんだんに使えるなら、カリー／ハワード対応は劇的にやさしくなります。
ならばそうすればいいじゃないか -- 残念ながらストリング図を容易に作成できるツール・環境が整備されていません。僕自身のことを言えば、手描きの絵図をスキャンした画像を使っていました。これは手間がかかるし、少しだけ違う絵を作るときにコピー＆ペースト＆モデファイの手法が使えません。結局、10枚のストリング図が必要なときでも1,2枚だけ載せてお茶を濁すことになります。ダメですなー。
「なんとかならないものか!?」と、年末年始に試行錯誤していました。理想からはかけ離れていますが、なんとか実用になる方法を案出しました。次節で説明します。
XyJaxで描く
現時点での結論は、「ストリング図をXyJaxで描く」というものです。XyJaxとは、ブラウザ内で動くJavaScriptの描画エンジンです。次の記事は、この件で大晦日にゴニョゴニョしていたときに書いたものです。
XyJaxは、ストリング図を描くために設計されているわけではないので、綺麗なストリング図を描く能力はありません。が、「綺麗な」を諦めて、なんとかギリ、ストリング図に見える絵を描くことは出来ます。
XyJaxでも頑張れば見栄えを良くすることは可能ですが、頑張りません。書き手に負担がかかり過ぎると、ストリング図がイヤになってテキスト記法や自然言語に戻ってしまいます。元の木阿弥、本末転倒です。審美的な観点には拘らず妥協します。先に挙げた証明図をXyJaxによるストリング図で描くと次のようになります。
XyJaxの問題点は、ブラウザ側でレンダリングするので、ストリング図をたくさん含む記事は“重いWebページ”になってしまうことです*7。これはどうしようもないので諦めます。
貧相なストリング図
審美的には妥協した結果、XyJaxで描くストリング図の見栄えは良くありません。以下に妥協点の説明をします。
ワイヤーは矢印付き
ストリング図は、描画方向を事前に決めてワイヤーには矢印（のアローヘッド）を付けない習慣です。が、XyJaxで描くストリングには矢印が付きます。これは、描画方向を気にしなくていいのでメリットとも言えます。
曲線の代わりに折れ線
XyJaxでなめらかな曲線を引くのは困難（不可能ではないけど）なので、カクカクした折れ線で我慢します。次のような感じです。
ちなみに、この図が表す関数／証明／射をテキストで書けば：
関数／証明／射の横結合〈並列結合〉を ''、縦結合〈直列結合〉を ';' で表しています。
は、ワイヤーの交差した部分が表す射〈対称射 | 入れ替え〉です。入力は単一の
（あるいは
）ではなくて、3つの入力があるとみなしています*8。
ループの中間部分を省略する
“関数のラムダ抽象／証明における含意導入／射のカリー化”は同じ概念ですが、これの図示にはワイヤーを曲げてループさせます*9。
XyJaxでループらしきものを描けなくはないです。次はラムダ抽象を描いてみたものです。
テキストで書けば：
左肩の '∩'〈キャップ記号〉は、関数のラムダ抽象〈カリー化〉を表すオペレーターです。
これを描くには、曲がりの調整にかなりの試行錯誤が必要です。たぶん、やってられません。次の形に簡略化します。
ループの中間を省略して、番号（ここでは #1）で繋ぐ箇所を示します。ワイヤーのループを描きたいのはヤマヤマですが*10、ループが複数になったときのレイアウト調整は地獄なので勘弁。
入れ子は使えない
ストリング図のノードの内部構造が再びストリング図で表されることがあります。入れ子のストリング図ですね。XyJaxで入れ子の図を描くのは困難なので、入れ子の内側は別な図とします。
メインの図では、'H' というラベルのノードを描き、Hの内部構造は 'where' に引き続く部分で説明します。上記の図をひとつの図に展開すれば次のようになります。
ループと入れ子が描けないのは欠点ですが、ループの補完や入れ子の展開を手描きや頭の中で行うことはトレーニングになるともいえます（言い訳だけど）。
変数無しスタイルと変数使用スタイル
分野のあいだの書き方や考え方のギャップのひとつとして、関数記述に変数を使うか使わないかの違いがあります。
圏論では、関数（つうか射）の入力変数／出力変数という概念がないので、関数記述に変数を使うことはありません。一方ラムダ計算では、変数の使用は本質的です。
先に例に挙げたループを含むストリング図のテキスト表示を3種類示しましょう。最初は図式順記法の変数無しスタイル（ポイントフリースタイルと呼ぶことが多い）、次は反図式順記法の変数無しスタイル、そして変数使用スタイルです。
変数使用スタイルでは、x, y, w が変数で、xは型Aのラムダ束縛変数（関数の引数変数）、y, w は自由変数です。
変数使用スタイルのときのプロファイルとストリング図は次のように書く／描くことにします。
プロファイルのなかで、自由変数の型宣言を行います。このとき、型宣言にコロンを使うので、関数名／関数項とプロファイルの区切りはダブルコロンにしたのです。異なる文化・記法の複数分野を混ぜ合わせるときは、こういう変更・調整が必要になります*11。
ストリング図のススメ
ついでに言っておくと、ラムダ式〈ラムダ項〉とそのプロファイルには別な書き方があります。以下の３つは、すべて完全に同じ意味です。
書き方が変わると呼び名も変わって、二番目・三番目の形は型判断〈type judgement〉と呼んだりします。論理ではシーケント〈sequent〉と呼ぶのでした。アサーション〈assertion〉とかステートメント〈statement〉と呼ぶこともあります。
なんで、同じ概念を別な名前で呼び、別な記法で書くのだ？ と腹立たしいでしょうが、繰り返し言います； それぞれの分野はまったく別々に発展してきて、異なる文化・言語を持ちます。後知恵で同じ概念だと分かったところで、分野固有の習慣・伝統を捨てるわけにはいかないんです。
結局我々は、同じ概念／同じ内容を、異なった習慣・伝統のもとで何度も何度も繰り返し重複して学ぶことになります。「同じことなんだ」と認識していれば「色々な文化・言語があるもんだなー」と旅行気分を楽しめるかも知れません。しかしもし、概念／内容も異なると思っていたとしたら、なんという恐ろしい無駄でしょうか、ゾッとします。
だからこそ、異なる習慣・伝統・文化・言語を横断した共通構造／同型性を認識する必要があるのです。カリー／ハワード対応を学んで、ゾッとする無駄を省くべきなのです。
異なる分野の共通構造／同型性を記述するためには、そのための記法・図法が必要です。なかでも、ストリング図は実に強力な武器になります。にも関わらず、この最強の記述手段が満足に使えない状況なのです。
この記事で述べたXyJaxを使う方法は、まったくもってギゴチないのですが、最強の記述手段＝ストリング図を使えるチャンスを広げることにはなると思います。
- 関連する記事： 確率論のカリー／ハワード／ランベック対応
*1:僕は、圏論が絡んできた場合はカリー／ハワード／ランベック対応〈Curry-Howard-Lambek correspondence〉と呼んでいます。
*2:「関数型言語」という言葉に出てくる「型」は、"functional language" の "nal" の部分です。今話題にしている「関数型」は、"function type" です。
*3:ロリポップと呼ばれる先端が丸い矢印記号 を使うことはあります。
*4:用語・記法の激しい変更に耐えられる基礎体力を付けるためのトレーニングが「基本スキルの確認と練習 (G2 A6P3, C A7P3)」にあります。
*5:もちろん、この約束もこの記事だけのローカルな取り決めに過ぎません。あらゆる記法の約束はローカルルールです。
*6:一番よく使われている図式は、アローを使った可換図式です。高次元版も含めてペースティング図といいます。ストリング図／サーフェイス図はペースティング図とは別な図法です。
*7:XyJaxのレンダリング結果は、画像のようにキャッシュされないので、毎回レンダリングが走ります。レンダリング結果のキャッシュ技術が生まれるか、または高速レンダリングで気にならなくなるか -- どっちでもいいから早く実現されないかな。
*8:正確に言えば、ストリング図は圏の射ではなくて、復圏〈multicategory〉の復射〈multimorphism〉を表しています。さらには、多圏〈polycategory〉まで広げて考えるのが便利です。
*9:なめらかな曲線を使った綺麗な描画は「ボブ・クック教授による、対称とは限らないモノイド閉圏における絵の描き方」参照。
*10:カーブしない、カクカクの閉路を作るテもありますね。
*11:記法、文化といった抽象的な組織体のあいだのネゴシエーション〈すり合わせ協議〉を行うわけです。このネゴシエーションはホントに大変な作業です。
