カリー・ハワード対応で有名なハワードの論文を今更ながら読んでみたので簡単に解説する。この著作は1980年のカリーへの記念論文集で出版されているが元々は1969年にmanuscriptとして読まれ引用されていたものである。1980年版では1969年版(未読)にほとんど手を加えていないと書いている。これほど重要な結果がなぜ出版されなかったのかということについてはWadler,"Propositions as Types", 20151に載っているハワードからの長文の返信メールで説明されている。先行する結果としてCurry(1958)のpositive implicational propositional logicとbasic combinatorとの対応に関する考察とTait(1965)のカット除去とラムダ項簡約の対応が挙げられている(pp.479-480)。 タイトルに書かれている"construction"というのはterm(項)のことである(p.481)。この用語法はいわゆるBHK解釈に則ったものである2。 1980年版での回想では
The ultimate goad was to develop a notion of construction suitable for the interpretation of intuitionistic mathematics (最終的な目標は直観主義数学の解釈に相応しい構成の概念を発展させることであった) (p.479)
と述べられている。証明論的なので計算機科学の文脈でカリーハワードに馴染みがある場合、ハワードのオリジナルな論文がこのような壮大な目標のために書かれたという記述は少し面食らうのではないかと思う。実際この論文ではハイティング算術の範囲まで論理とラムダ計算の対応が扱われているが、本人はタイトルは適切ではなかったと回顧している(p.479)。
この論文の特徴についてであるが、読む前はカリーハワード対応のアイデアが言葉で説明されているのかと思っていたが、実際は堅実に定義と証明が繰り返されるスタイルの技術的な論文である。とてもストイックなスタイルで意義が言葉で説明されているというようなことはない。技術的に重要な点はカリーハワード対応は現在では典型的には自然演繹と型付ラムダ計算の間の対応として紹介されるが、この論文ではそうなっていない。具体的には自然演繹ではなくシーケント計算が用いられている。なぜ自然演繹が用いられなかったのかということであるがPrawitz(1965)の本によって自然演繹が発展したので1969年では自然演繹はメジャーな選択肢ではなかったのだろうかと思われる3。
より詳しくは以下の通りである4。第1章第5節までは直観主義論理のimplicational fragmentが考察される。最初に提示される体系はシーケント計算スタイルの自然演繹である。公理、弱化規則、交換規則、縮約規則を備えているが含意は導入則と除去則の形をしている。論理体系と型付ラムダ計算がそれぞれ定義され、Theorem 1では証明とラムダ項が対応することが示される。しかしシーケント計算スタイルにした影響で第5節で項の正規化とカット除去の対応を考えようとした際、自然演繹のような推論規則では左規則がなくカットが行えない。そこで推論規則が導入/除去からシーケント計算の右規則/左規則に置き換えられる(5.2, 5.3)。そしてTheorem2でカット除去と正規化の対応が述べられる。第6節では否定,連言, 選言が体系に追加される。注意すべきはが
と定義される点である(
は後件に来て欲しい)。否定の導入は含意の左規則によってなされる。このように定義した理由はよくわからない。1979年の回顧ではP. Martin-Löfの指摘によってシーケント計算のカット除去ではこの定義は適当でなかったと述べている(p.484)。Theoremとなっているのは正規形についてである。
第2章ではハイティング算術に対応が拡張される。このセッティングでは型が項を含み、型変数に対する量化を行うことができる。つまり依存型が扱われている事になる。
- https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf↩
- (Wadler, 2015)での本人のコメントからやり取りをしていたKreiselの影響であろう。↩
- Howardは(Wadler, 2015)でこう述べている。 "I was not familiar with Prawitz's results (or, if at all, then only vaguely)."↩
- 以下は技術的に細かい話になるので興味がない場合は読み飛ばしてください。↩
