Curry–Howard のやさしい紹介
命題＝型、証明＝プログラム
入門（高校〜大学1年レベル）
このページの目標
論理と計算が同じ構造を持つという Curry–Howard 対応の直感をつかむ。「命題は型、証明はプログラム、簡約は計算」という対応を具体例で一望し、この分野の背骨を最初に見渡す。
1. 論理と計算が出会う
これまでの章で、証明とは「公理から推論規則を適用して結論に至る記号操作」だと見てきた。一方、計算とは「プログラムを規則に従って実行（簡約）すること」である。20世紀半ば、この二つがまったく同じ構造をしていることが発見された。これが Curry–Howard 対応である。
論理と型付き計算の間の次の対応をいう。 命題は型に、証明はその型を持つプログラム（項）に、証明の簡約（正規化）は計算（プログラムの実行）に対応する。
2. 対応の一覧
論理側の概念が、計算側の何に対応するかを並べると、対応の広さが見えてくる。
3. 「ならば」は関数
対応の中心は含意である。「$A$ ならば $B$」を証明するとは、「$A$ の証明が与えられたら、それを使って $B$ の証明を作る方法」を示すことに他ならない。これはまさに、$A$ 型の入力から $B$ 型の出力を作る関数である。
$A \to B$ の証明（＝関数 $f$）と $A$ の証明（＝値 $a$）があれば、$B$ の証明が得られる。これは関数適用 $f(a)$ そのものである。論理の推論規則「モーダスポネンス」が、計算の「関数に引数を渡す」操作に対応している。
$$\dfrac{A \to B \qquad A}{B} \quad\longleftrightarrow\quad f : A \to B,\ a : A \ \Rightarrow\ f(a) : B$$同様に、$A \land B$ の証明は「$A$ の証明と $B$ の証明のペア」、$A \lor B$ の証明は「どちらを証明したかのラベル付きの証明」に対応する。論理結合子のそれぞれが、プログラミングでおなじみのデータ構造になる。
4. なぜこれが分野の背骨なのか
Curry–Howard 対応のもとでは、型検査がそのまま証明検査になる。型の正しいプログラムを書ければ、対応する命題を証明したことになる。計算機は型を機械的に検査できるので、証明の正しさも機械的に保証できる。
証明アシスタントの原理
Coq・Lean・Agda などの証明アシスタントは、この対応を実装したものである。ユーザは命題（型）を述べ、その型を持つ項（証明＝プログラム）を構成する。システムは型検査によって証明の正しさを確認する。「証明を書く」ことと「型の付くプログラムを書く」ことが、文字どおり同じ作業になる。
この対応の本格的な土台は、λ計算（計算の側）と 型理論（型の側）で扱う。さらに量化子 $\forall, \exists$ まで対応を広げると 依存型理論 に至り、Coq・Lean の表現力の源になる。入門のいまは、「論理と計算は同じものの二つの顔である」という一望を持ち帰れば十分である。
まとめ
この章のポイント
- Curry–Howard 対応：命題＝型、証明＝プログラム、簡約＝計算
- 含意 $A \to B$ は関数型、連言 $A \land B$ はペア、選言 $A \lor B$ は直和
- モーダスポネンスは関数適用 $f(a)$ に対応する
- 型検査 ＝ 証明検査。これが型理論ベースの証明アシスタントの背骨
- λ計算・型理論・依存型理論へと、この対応が深まっていく
よくある質問
Curry–Howard 対応とは何か
論理と計算が同じ構造を持つという発見である。命題は型に、証明はその型を持つプログラム（項）に、証明の簡約は計算に対応する。「証明＝プログラム、命題＝型」と要約され、Coq・Lean・Agda など型理論ベースの証明アシスタントの背骨になっている。
「証明はプログラムである」とは具体的にどういうことか
「$A$ ならば $B$」($A \to B$) の証明は、$A$ の証明を受け取って $B$ の証明を返す手続き、すなわち型 $A \to B$ の関数に対応する。「$A$ かつ $B$」の証明は $A$ の証明と $B$ の証明のペアに対応する。証明を組み立てる操作が、そのままプログラムを組み立てる操作になっている。
Curry–Howard 対応はなぜ重要なのか
証明を書くこととプログラムを書くことが同一視でき、型検査がそのまま証明検査になる。型の正しいプログラムを構成できれば命題が証明されたことになり、計算機が型を機械的に検査することで証明の正しさを保証できる。型理論ベースの証明アシスタントが成立する根拠そのものである。