数学における定理の構成的証明と計算機におけるプログラムとの間には"proofs as programs"と呼ばれる対応が存在していることが知られている。つまり、数学での「定理」はプログラムの「仕様」と考えることができ、その定理の「構成的証明」は、その仕様を満たす「プログラム」と見なすことができるという考え方である。数学での定理の証明は、その正当性を機械的に検証することができる形式的な枠組の中で遂行することが可能で、この形式的証明からは計算機プログラムを機械的に抽出することができる。この抽出されたプログラムが与えられた仕様を満たすことは、論理的命題の解釈に対する形式系の健全性によって保証される。現在までにこのようなパラダイムを基礎とした形式的プログラム開発の試みがいくつか行なわれてきた。

　しかし従来の研究は「構成的数学の証明からプログラムを抽出する」という、適当な構成的論理体系をプログラミングへ応用するというアプローチが中心となっており、証明することのできる定理のクラス、つまり実現可能な仕様のクラスに対しての関心に比べると、その証明のクラスの大きさ、つまり一つの仕様を満足するプログラムのクラスの大きさについて関心が払われることは少なかった。そのため、現実のプログラミングのいくつかの重要な局面が見過ごされる傾向があった。つまり、"proofs as programs"というパラダイムを現実のプログラミングに応用することを考えた場合には、プログラマが行なうプログラムの構築がその形式系の上で自然に実行できるかという問題が残されている。このような問題を検討するためには、単に「一つの論理体系を"proofs as programs"によってプログラミングに応用する」というアプローチだけでなく、逆に「現実のプログラミングからそれに対応する論理体系を考える」というアプローチが不可欠と考えられる。

　本論文は、いくつかの実用的なプログラミング言語で提供されてる「キャッチアンドスロー機構」という仕組みと、それを用いた「例外処理の技法」に着目し、そこに見られる論理的構造を一つの構成的な論理として形式化し、これを"proofs as programs"の枠組の中に取り込むことを目的とする。

　まず、キャッチアンドスロー機構を持つ簡単なプログラミング言語を導入する。その文法の概略は以下のようなものである。

　ここで<項>がプログラムに対応する。この言語の操作的意味は以下のような書き換え規則で定義される。

　ただし、CやC’は、値呼びによる評価コンテクストであり、xは変数、uはタグ、Mは任意の項、Vはすでに評価を終えた値を表している。このような言語に対して、以下のような形に表記される「型づけ」を考える。

　ただし、A_i,C,E_jはある型を表している。この型づけの素朴な意味は、A₁,...,A_mという仕様を満たすプログラムx₁,...,x_mが与えられれば、プログラムMは仕様Cを満たす、ただし、場合によってはMの実行の過程で、u₁,...,u_nのいずれかのタグに対するthrow操作がおきることがあり、その時throwされる値は、そのタグに対応するE_jを満たす、

　と考えれば良い。このような解釈を念頭に型づけ系を導入する。の推論規則の概略は次のようになる。

　この形式系は論理体系としては通常の直観主義論理と等価であるが、キャッチアンドスローによる例外処理の技法を自然に反映した証明の構築が可能となる。これはでは主要な結論の他に複数個の例外的な結論が許されるているためである。先に紹介した型づけの素朴な解釈は、言語の操作的意味論を用いて厳密に定式化することができ、これは通常の直観主義論理に対する実現可能解釈の自然な拡張となる。また、この解釈に対するの健全性を証明することが可能であり、の証明がキャッチアンドスロー機構によって効率的な例外処理を行なうプログラムに自然に対応していることが明らかになる。

　ここでは項に対する一連の書き換え規則によって操作的意味論を与えたが、この意味論は、現実のプログラミング言語でのスタックによるキャッチアンドスロー機構の実現をそのまま定式化することによって得られる意味論と等価であることが示される。この機構の実現に評価コンテクストの複製・保存が必要ないことも導かれる。また、さきに定式化した実現可能性解釈は、このスタックによる実現を反映した意味論を用いて直接的に表現することも可能である。

　論理体系としてのの特徴を分析するために、これをsequent calculusとして再構成しGentzenのLKやLJと比較すると、は論理系としては単にLJのもう一つの定式化であることが分かる。またはLKにおける(→⊃)規則に対して「上式の右に複数の論理式が現れない」という制限を加えたものに他ならない。この時catchというプログラム構成子はLKにおける右のcontraction規則に対応し、throwは同じく右のweakening規則に対応する。このsequent calculusに対してはcut除去定理が成立する。

　最後に、評価戦略を固定しないキャッチアンドスロー機構について考察する。項に対する書き換え規則を以下のように拡張する。

　ただしCは任意のコンテクストであり、特に値呼びの評価コンテクストである必要はない。またFV(M)はMに自由に出現する変数およびタグの集合を表すものとする。この書き換え規則の拡張は項の評価に非決定性を導入する。例えば、

　というプログラムMを考えると、

　のような三通りの評価が可能になる。このような非決定性を許した場合の"proofs as programs"が問題となってくるが、に適当な拡張を加えた体系L_c/tを考えることによって、項の書き換えが型を保存することが示される。また実現可能性解釈の方も自然に拡張することでL_c/tの健全性が得られる。さらにL_c/tで型づけ可能な項はすべてstrongly normalizabeであることが示される。このような結果はL_c/tのterm modelを構築することで得られる。

　本論文は、いくつかの実用的なプログラミング言語で提供されてる「キャッチアンドスロー機構」という仕組みと、それを用いた「例外処理の技法」に着目し、そこに見られる論理的構造を一つの構成的な論理として形式化し、これを"proofs as programs"の枠組の中に取り込むことを目的としたものである。

　まず、キャッチアンドスロー機構を持つ簡単なプログラミング言語が導入される。その文法の概略は以下のようたものである。

　$212428f08.gif$

　ここで<項>がプログラムに対応する。この言語の操作的意味は以下のような書き換え規則で定義される。

　$212428f09.gif$

　ただし、CやC’は、値呼びによる評価コンテクストであり、xは変数、uはタグ、Mは任意の項、Vはすでに評価を終えた値を表している。このようた言語に対して、以下のような形に表記される「型づけ」が与えられる。

　$212428f10.gif$

　ただし、A_i,C,E_jはある型を表している。この型づけの素朴な意味は、A₁,...,A_mという仕様を満たすプログラムx₁,...,x_mが与えられれば、プログラムMは仕様Cを満たす、ただし、場合によってはMの実行の過程で、u₁,...,u_nのいずれかのタグに対するthrow操作がおきることがあり、その時throwされる値は、そのタグに対応するE_jを満たす、

　と考えられる。このような解釈を念頭に型づけ系が導入される。の推論規則の概略は次のようになる。

　$212428f11.gif$

　この形式系は論理体系としては通常の直観主義論理と等価であるが、キャッチアンドスローによる例外処理の技法を自然に反映した証明の構築が可能となる。これはでは主要な結論の他に複数個の例外的な結論が許されるているためである。先に紹介した型づけの素朴な解釈は、言語の操作的意味論を用いて厳密に定式化することができ、これは通常の直観主義論理に対する実現可能解釈の自然な拡張となる。また、この解釈に対するの健全性を証明することが可能であり、の証明がキャッチアンドスロー機構によって効率的な例外処理を行なうプログラムに自然に対応していることが明らかになる。

　ここでは項に対する一連の書き換え規則によって操作的意味論を与えられたが、この意味論は、現実のプログラミング言語でのスタックによるキャッチアンドスロー機構の実現をそのまま定式化することによって得られる意味論と等価であることが示される。この機構の実現に評価コンテクストの複製・保存が必要ないことも導かれる。また、さきに定式化した実現可能性解釈は、このスタックによる実現を反映した意味論を用いて直接的に表現することも可能である。

　論理体系としてのの特徴を分析するために、これをsequent calculusとして再構成しGentzenのLKやLJと比較すると、は論理系としては単にLJのもう一つの定式化であることが分かる。またはLKにおける(→⊃)規則に対して「上式の右に複数の論理式が現れない」という制限を加えたものに他ならない。この時catchというプログラム構成子はLKにおける右のcontraction規則に対応し、throwは同じく右のweakening規則に対応する。このsequent calculusに対してはcut除去定理が成立する。

　最後に、評価戦略を固定しないキャッチアンドスロー機構について考察されている。項に対する書き換え規則は以下のように拡張される。

　$212428f12.gif$

　ただしCは任意のコンテクストであり、特に値呼びの評価コンテクストである必要はない。またFV(M)はMに自由に出現する変数およびタグの集合を表すものである。この書き換え規則の拡張は項の評価に非決定性を導入する。例えば、

　$212428f13.gif$

　というプログラムMを考えると、

　$212428f14.gif$

　のような三通りの評価が可能になる。このような非決定性を許した場合の"proofs as programs"が問題となってくるが、に適当な拡張を加えた体系L_c/tを考えることによって、項の書き換えが型を保存することが示される。また実現可能性解釈の方も自然に拡張することでL_c/tの健全性が得られる。さらにL_c/tで型づけ可能な項はすべてstrongly normalizabeであることが示される。このような結果はL_c/tのterm modelを構築することで得られる。

　よって本審査委員会委員は、全員一致で本論文が博士(理学)の学位を授与できるものと認める。