７．９ カリー＝ハワード同型対応
世の中には、言い方は違っているのだが、同じことを言っているということが往々にしてある。
前回の記事で、型定理と圏論は一対一に対応づけできると説明したが、その例の一つである。さらに、もう一つ対応するものがある。それは、型定理と論理だ。
論理、型定理、圏論の関係を示すと以下のようになる。
| 意味 | 論理 | 型定理 | 圏論 |
|---|---|---|---|
| 真(true) | \(True\) | \(()\) (ユニット) | 終対象 |
| 偽(false) | \(False\) | \(Void\) | 始対象 |
| 論理積(conjunction) | \(A \land B\) | \((a,b)\) (デカルト積) | \(A \times B\) (直積) |
| 論理和(disjunction) | \(A \lor B\) | \(Either \ a \ b\) | \(A + B\) (余積) |
| 含意(implication) | \(A \rightarrow B\) | \(a \rightarrow b\) (関数型) | \(B^A\) (指数対象) |
| 含意除去(modus ponens) | \((A \rightarrow B \land A) = B\) | \((a \rightarrow b,a) = b\) | \((B^A \times A) = B\) |
この関係が成り立つので、プログラムの証明が可能になるが、それについてはいずれかの機会にしたいと思う。ここでは、論理、型定理、圏論の関係を示すに止めておき、次回は、自然変換(natural transformation)の話題に移行する。
注：\(a \rightarrow b\)はこれまでは説明しなかった。これは、すでに説明した写像対象\(A \rightarrow B\)を型に変えたものである。そして、関数の形をとっているので、関数型と呼ばれる。
