私が最初に BHK 解釈というものを学んだのは、佐藤雅彦先生の文章からだったと思う。
日本語で書かれた解説で、どこかの商業誌に発表されていたものだったはずだ。
その文章のタイトルにも「BHK 解釈」という言葉が入っていたと思う。
そこで部屋の中の copy の山の一部を引っくり返して調べてみたのだが、見当たらない。
Internet で調べてみたが、見当たらない。
記憶違いだったかもしれないと思ったが、以下の文献を図書館でひも解くと、あった。
- 佐藤雅彦 「数学の未解決問題 21世紀に向けて 4: 証明とプログラムの統一」、『数理科学』、437号、1999年11月
探していたのはこれであった。タイトルに「BHK 解釈」という言葉は入っていないが、確かにこれを読んで「BHK 解釈」というものを知ったのだった。
ただし、ちゃんと理解できた訳ではないし、今もってちゃんと理解できていない。いずれにせよ復習したいので、またこの解説を拝読させていただきます。という訳で、改めてこの解説を入手。
昨晩布団の上で何となく『数理科学』の1994年11月号の目次 copy を眺めていると、とても目の魅かれる論文タイトルがあることに気が付く。
以前に私はこの号の別の論考を copy して、加えて目次も copy して取っておいたのだが、上記小林先生の文章は見過ごしていた。しかし今回布団の上で、先生の文章のタイトルを見て、すぐに何の話が書かれているか、わかった。そこでこれはすぐに入手しなければならないと思い、翌日の今日、先生の文章を確保した次第。また勉強させていただきます。
さらに、この号に載っている次の文章も入手させていただいた。
- 竹内外史 「計算の複雑さとロジック」、『数理科学』、377号、1994年11月
この他に以下を入手。
- 佐藤雅彦 「情報科学と論理学」、『数学セミナー』、vol. 29, no. 1, 1990年1月
- 同上 「論理学とコンピュ-タ」、『理想』、607号、1983年12月
- 林晋 「証明とプログラム: もう一つの論理プログラミング」、『数理科学』、257号、1984年11月
- 岩本敦 「証明と理解」、『論集』、東京大学大学院人文社会系研究科哲学研究室、20号、2002年
- 大木島徹 「自然演繹についての諸考察 (III)」、『論集』、東京大学大学院人文社会系研究科哲学研究室、21号、2003年
このうち1本目の佐藤先生の文は読んだ覚えがある。しかし内容は完全に覚えていない。やれやれ…。
最後に、次のPR誌を例年通り入手。
- 『みすず』、2008年読書アンケート、no. 568, 2009年1・2月合併号
早速某先生のアンケートを拝読。なるほど、そうですか、わたしもそうです、ふむふむ。
他の先生方のアンケートも後日ゆっくりコーヒーでも飲みながら、拝見致します。
おやすみなさい。
