bitterharvest’s diary

A Bitter Harvestは小説の題名。作者は豪州のPeter Yeldham。苦闘の末に勝ちえた偏見からの解放は命との引換になったという悲しい物語

写像対象-カリー=ハワード同型対応

7.9 カリー=ハワード同型対応

世の中には、言い方は違っているのだが、同じことを言っているということが往々にしてある。

前回の記事で、型定理と圏論は一対一に対応づけできると説明したが、その例の一つである。さらに、もう一つ対応するものがある。それは、型定理と論理だ。

論理、型定理、圏論の関係を示すと以下のようになる。

意味 論理 型定理 圏論
真(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\)を型に変えたものである。そして、関数の形をとっているので、関数型と呼ばれる。