カリー=ハワード同型対応にびっくり

知の教科書 論理の哲学 (講談社選書メチエ)

飯田隆(編)

講談社、2005

↑の本のいくつかの章をコピーして読んでいた。

照井一成「計算と論理」は、カリー=ハワード同型対応の解説。ほうほうと思って読んでたらこれがびっくり。

カリー=ハワード同型対応って、「論理学の証明と関数型言語のプログラムが一対一対応する」という定理らしいというのは知っていた。しかし知識として知っていただけで中身を知らなかったのだが、解説を読んでいくと非常におもしろい。

(正確に言うと自然演繹法と型付きラムダ計算の対応らしい)。

f: P→Q
a: P
f(a): Q

関数fの型を「P→Q」としよう。fはP型のデータを受け取ってQ型のデータを返す。

aの型をP型としよう。

fにaを適用したもの、つまり、f(a)の型は、「Pを受け取って、Qを返す関数」に「P」を適用したのだから、当然Q型になる。

論理学を勉強したことのある人はこれを見て何かを思い出すかもしれない。

「P→Q」そして「P」。すると「Q」。

モーダスポネンスと呼ばれる論証規則、数ある論理学の規則のなかでもとても基本的なものの1つだ。

つまり「関数適用ってモーダスポーネンスに似てね？」ということだ。それだけだったら「はいはい似てる似てる」で終わるただの思いつきなのだが、この対応関係はどこまでもつづき、ついには論理と計算(プログラム)の対応が証明されてしまうらしい。

すげー、おもしろいなーと思って解説論文を読んでいたのだが、以下はかなり衝撃的だった。

Lispの方言の一つにSchemeという関数型プログラミング言語がある。この言語にはLispの演算子に加えて、例外処理などのための大域脱出を可能にする継続呼び出し演算子call/ccが含まれている。一九九〇年、グリフィンという計算機科学者はラムダ計算にの継続呼び出し演算子を加えることが直観主義論理に背理法を加えることに相当するというセンセーショナルな結果を示した。ゆえに古典論理と直観主義論理の違いは、プログラミングの言葉でいえば、大域脱出ができるかできないかの違いだということになる。

p206

関数型言語にcall/ccを加えると古典論理になるらしい。call/ccって背理法だったらしいぞ！なんだってー！！

(ちょっと調べるとcall/ccの方が広いみたいだけど)。

つまりあれだ、二重否定除去とか背理法とかうさんくさいから止めて直観主義論理でいこうというのは「call/ccとか黒魔術だから使うのやめよう」というのに相当する(たぶん)。

あー、びっくりした。