「カリー／ハワード対応を小一時間で説明してみようか」と思ったのですが、すぐさま、この企ては諦めました。無理だよな。もちろん、ある程度の準備が必要という事情がありますが、分かりやすい対応を作る際に障害物・障壁があるんですよね、… ったくもう。愚痴を書きます。
内容：
何と何を対応させるのか
カリー／ハワード“対応”なんで、何かと何かを対応させるのでしょうが、何を対応させるの？ オーソドックスな答は「論理と型付きラムダ計算を対応させる」でしょう。はい、それでいいです、文句ありません。
型付きラムダ計算は、方言があるとはいえ、比較的安定した構文を持ちます。で、論理側の対応物は何にしましょう？ 自然演繹とシーケント計算が候補になるでしょう。僕は、自然演繹は一切使わないで、シーケント計算とラムダ計算の対応を取ったほうがスッキリすると思っています。しかし、自然演繹を使うほうが多数派です。僕自身も、2009年のセミナーでは自然演繹を使っています。
- 2009-03-21 カリー／ハワード（Curry-Howard）の対応を知らない子ども達および大人達へ
- 2009-04-01 カリー／ハワード（Curry-Howard）のお絵描きを楽しもう
なお、上記の記事からリンクされているKuwataさん記事 http://return0.dyndns.org/log/2009/03/20#s_2、superstring04さん記事 http://d.hatena.ne.jp/superstring04/20090328/1238211198 は現在でも残っています。リンク切れにならずにヨカッタ。
僕が（たぶん多くの人も）自然演繹を採用したのは、シーケント計算には抵抗感がある人が多いみたいだからです。僕の知る範囲では、いきなりシーケント計算を出されても「何してるかサッパリわからん！」という反応です。それに比べれば、「ソクラテスは死ぬ」とかどうでもいい例と一緒に自然演繹を出したほうがマシなようです。
という次第で、標準的（＝多数派の）選択としては、「カリー／ハワード対応は、自然演繹と型付きラムダ計算を対応させる」となるのでしょう。
シーケント計算を考慮する
いきなりシーケントを出してアレルギーを引き起こすのもなんだから、自然演繹を使うことにしたわけですが、僕が内心「シーケントのほうがいい」と思っている理由は、セマンティクスとの相性の問題です。自然演繹はセマンティクスと相性が悪い、つうか、セマンティクスと距離があるんですよ。一方、シーケントはセマンティクスに繋げるのが容易です。
シーケントとは、型理論で言えば型判断 x1:A1, ..., xn:An ⇒ E:B です。ここで、xiは変数、AiとBは型、Eは式です。変数と式を除いてしまえば、A1, ..., An ⇒ B なので、論理のシーケントです。逆に言うと、論理のシーケントに変数と式で註釈を追加すれば、型理論の型判断が出来上がるのです。
シーケント計算の証明図が、ラムダ式へ型付けしていく過程（型推論）をそのまま表現しているので、「論理の証明図←→ラムダ式の型付けの過程」という対応としてカリー／ハワード対応を提示できます。
シーケント＝型判断は、セマンティクスであるデカルト閉圏の射に対応します。この対応を使うと、シーケント論理／型理論とデカルト閉圏（より一般にはモノイド閉圏）との対応を調べることが出来ます。
構文（シーケント計算／ラムダ計算）からセマンティクスであるデカルト閉圏への対応をスムーズに進めるために、僕は「大きなラムダ式」というものを導入しました。「大きなラムダ式／大きなラムダ計算」は以下の記事で触れています。
「自然演繹の構文←→ラムダ計算の構文」のような構文のあいだの相互変換よりは、「構文→セマンティクス」のほうが重要だと僕は思っています。なので、大きなラムダ式を仲介として、「ラムダ計算の構文→デカルト閉圏」という対応を優先させたいのです。立場としては、セマンティクス重視、セマンティクス駆動な立場と言えます。
セマンティック駆動な立場については次の記事で述べています。
- 演繹系とお絵描き圏論
- 圏論からシーケント計算へ
- 圏論の筆算としてのシーケント計算
- シーケント計算と圏論（続きみたいな）
- 型付きラムダ計算のモデルの作り方
- セマンティック駆動な圏的ラムダ計算とシーケント
「ラムダ計算の構文→デカルト閉圏」が理解できて、「シーケント計算の構文→デカルト閉圏」も理解できれば、どちらもデカルト閉圏をモデルに持つのだから「ラムダ計算もシーケント計算も同じようなもんだ」と納得できるでしょう。僕の主観に過ぎませんが、構文のあいだの相互変換が在る事より、同じ意味（セマンティクス、モデル）を持つ事のほうが、類似性・同形性が腑に落ちる気がします。これは、心理的・心情的な納得感の問題だ、ともう一度断っておきますけどね。
邪魔だが無視できない存在としての自然演繹
冒頭で「愚痴を書きます」と記したのですが、今日の愚痴は自然演繹に関してです。「型付きラムダ計算と型判断」「シーケント計算」「デカルト閉圏（またはモノイド閉圏）」という三者は、（少なくとも僕にとっては）きれいなトリニティを形成しています。
ところが、かつての僕も含めて多数派の選択では、自然演繹を話題に取り上げます。自然演繹を入れると、きれいなトリニティが乱されるのでイヤだなー、と感じるのですが、まったく触れないのもドーヨ？ と不安になったりもします。
そもそも僕は、自然演繹には不満タラタラなんです。
自然演繹、シーケント計算、型付きラムダ計算の対応をまとめてみると：
| 自然演繹 | シーケント計算 | 型付きラムダ計算 |
|---|---|---|
| 命題 | 命題 | 型 |
| 証明図 | シーケント | 型判断 |
| 推論図 | 公理シーケント | 公理（自明と認める）型判断 |
| 証明図書き換えの規則 | 推論図 | 型付けの規則 |
| 証明図書き換えの過程 | 証明図 | 型付けの過程 |
「推論図」、「証明図」といった言葉が、自然演繹とシーケントではズレているんです。シーケントのほうがメタな記述になっているから「メタな分だけズレる」と言えば、そりゃそうなんだけど混乱を招きます。僕としては、自然演繹の証明図は縦書きシーケントとでも呼びたい。
自然演繹の証明図とシーケント計算の証明図は全然対応してなくて、自然演繹における証明過程（リーズニング）を表しているのは、証明図の時間方向での書き換え（アニメーション）です。「ちっとも自然じゃない」と悪態をついた主たる理由は、アニメーションを断片的静的図（スチル）で代用するという無茶をしているからです。
アニメーションをスチル1,2枚で代用するのはやめろよ！ と、「自然演繹はちっとも自然じゃない -- 圏論による再考」で主張しています。
自然演繹、シーケント計算、型付きラムダ計算は出自が違うので、それぞれに異なった歴史と伝統を持ちます。見た目がまったく異なるものが実は同一だった、と分かれば感動するかも知れません。が、見た目が異なっているのは歴史的（たぶんに偶発的）事情だとするなら、感動にいたる労力の多くは歴史的・文化的差異の理解に費やされるわけで、それって意味あんのかよ？ と疑問に感じるのです。
悩む！
現時点で、カリー／ハワード対応を小一時間、いや出来るだけ短時間で話すなら次のようにするでしょう。
- 非形式的に型付きラムダ式の構文を導入する。タプリングは最初から入れる。組み込みの関数（例えば整数の足し算）がないとかえって分かりにくいので、関数記号（指数型の定数記号）とデルタ変換（オラクル）も入れる。
- 変数（関数変数もあり）の型宣言があれば、式の型を決められるだろう、という話をする。
- 変数の型宣言のもとで、式の型を決定する規則を型判断（＝シーケント）の形で書く。
- ラムダ式の構文解析木に、型註釈を付けていくことにより、型付け（型推論）過程をツリー（一般にはグラフ）状に描くことができる。
- 型付け過程のグラフから、変数や式を消して型だけを残したグラフを作る。
- これって、命題の論理的証明の過程を描いたグラフじゃん。← って無理があるか？
最後のところが納得感があるかどうか疑問です。やっぱり自然演繹入れたほうがいいのか？ あー、悩む！
過去に書いた、手を変え品を変えの説明↓
いまだベストと思える説明に届かず。
