本論文は、様相論理の上の証明と計算機プログラムとの間の自然なCurry-Howard対応を確立するものである。従来、このような対応は存在しないと予想されていたが、論文提出者は -strong monadと呼ぶ圏論的な構造を定義し、それがプログラム意味論と様相論理の意味論の両方のための枠組となることを示した。 1989年、Eugenio Moggiはstrong monadの概念に基づく圏論的なプログラム意味論の枠組を提案した。この枠組は非常に一般性のあるもので、これにより非決定性、副作用、例外、継続などを含む多様な計算の意味論を統一的に扱えるようになった。一方、(strongとは限らない)monadは様相論理の意味論に利用できることが以前より知られており、一見した所では、strong monadも様相論理の意味論に利用できるように見える。しかし、strong monadを用いた解釈では不自然な様相論理しか成立しない。つまり、プログラムを証明と見なしたとき、不自然な命題が証明を持つことになる。 ところが、strong monadの拡張である-strong monadという構造を用いれば、CS4という自然な構成的様相論理に対して健全かつ完全な意味論を展開できることを論文提出者は見出した。しかも同じ構造を用いてMoggiのプログラム意味論を健全性と完全性を保ったまま拡張することもできる。そしてMoggiの予想とは逆に、CS4の証明とプログラムの間に自然なCurry-Howard対応が成立することも見出した。 本論文では、-strong monadという構造が、第3章と第4章において導入される。次に、第5章において、様相論理CS4に対する実現可能性解釈(realizability interpretation)を与えられ、CS4の証明に実現子としてMoggiの型付き言語computational metalanguage(以下、metalanguageと記す)のプログラムを対応させられることが示されている。この対応は-strong monadを用いた意味論の特別な場合であることが証明される。また、CS4と論理的に同値な構成的型理論TCS4を定義する。TCS4はmetalanguageの拡張になっており、拡張部分を消去することで、TCS4の証明項からプログラムを得る写像(崩壊写像と呼ぶ)を定義できる。第6章において、この写像が、ちょうど実現子(realizer)を求める手続きになっていることが証明される。この手続きは、証明から、プログラム実行時には不要であるような情報を削り落とす操作であると考えられる。第8章では、さらに、この写像とは逆に、与えられたプログラムに対して証明項を対応させることにより、metalanguageをTCS4に埋め込めることも示す。この埋め込み写像は崩壊写像の右逆写像になることもわかる。しかも、埋め込み写像を-strong monadを用いたプログラム意味論の特別な場合として理解することもできる。 以上の結果に基づき、博士(理学)を授与できると認める。 |