The analogy between mathematical logic and typed λ-calculi has been formu-lated as formal correspondence between the theory of intuitionistic propositional logic and simply typed λ-calculus, known as Curry-Howard isomorphism. It maps formulas, proofs, and reductions of proofs in intuitionistic propositional logic into types, λ-terms, and reductions of λ-terms, respectively. As extensions are made to intuitionistic propositional logic to increase its expressibility, resulting in predi-cate logic, second-order logic, etc., simply typed λ-calculus has also been extended and corresponding λ-calculi have been formulated. In particular, the extension of simply typed λ-calculus corresponding to predicate logic is called λP.

In this thesis, according to Curry-Howard isomorphism, we construct an ex-tension of simply typed λ-calculus, called strong λD, which corresponds to an in-tuitionistic fragment of the minimal modal logic based on the notion of necessity. The extended λ-calculus can represent the so-called staged computation, where modalities correspond to different stages of computation.

Having various extensions of the theory of propositional logic and simply typed A-calculus, it is of extreme interest to compare the expressive power of the exten-sions. In this thesis, we focus on correspondence between first-order predicate logic and modal logic. In mathematical logic, a translation from modal formulas into formulas in predicate logic is defined and the image of modal formulas by the translation is characterized by bisimulations. In this way, the notion of universality in predicate logic is shown to subsume the notion of necessity in modal logic.

On the analogy of this correspondence, we studied correspondence between proofs in first-order predicate logic and proofs in modal logic. In the thesis, we give a complete and full translation from strong λ□ into λP. A translation between two calculi is said to be complete when the translation preserves equations in the source calculus, and equations in the image of the translation can be pulled back to equations in the source calculus. Furthermore, it is called full if the translation does not add any junk. The existence of a complete and full translation means that the structure of the source calculus is preserved in the target calculus. Our result is about proofs which have not been dealt with in mathematical logic, i.e., the notion of universality is shown to subsume the notion of necessity more strongly. In this sense our result is a refinement of the above traditional result in mathematic In addition, by observing the image of other kinds of modalities in λP, such as intuitionistic T, K4, and S4, we obtain knowledge on those modalities in general.

We also investigated existing typed λ-calculi corresponding to modal logics, and focused on that there exist two kinds of context formulations for construction of such calculi. One is formulated by single contexts, e.g., λsS4, and the other is formulated by multi contexts, e.g., λMS4 We gave sound and complete translations between λss4 and λMS4, and claimed that the difference of context formulations raises no essential difference.

数理論理体系と型つきラムダ計算との関係は古くから理論計算機科学者の関心事であり、特に、「ラムダ項は論理式の証明」であるということを定式化したカリー=ハワード同型は有名である。最も単純な論理体系である命題論理と、単純型つきラムダ計算とのカリー=ハワード同型は古くから知られていたが、近年、より拡張された論理体系(例えば述語論理や二階論理など)と、それに対応するラムダ計算を探求する研究が盛んに行われている。

今回提出された安部達也君の博士論文は、その一環として、とくに様相論理に対応するラムダ計算を探求することを目的としている。まず第一の貢献として、様相論理のもっとも基本的な体系といわれる「K」に対するラムダ計算として、「strong λ□」を提案した。そして、この計算系が、Kの証明を自然に表せるだけではなく、ある種のカテゴリ意味論を与えることができることから妥当であることを示した。

第二の貢献として、strongλ□を利用し、様相論理と述語論理の表現力の比較を行った。古くから、様相論理の「論理式」から述語論理の「論理式」へは、自然な変換が可能であることは知られていたが、本論文では、様相論理の「証明」から述語論理の「証明」への変換を示すことにより、この二つの体系のさらなる「緊密」な関係を示すことに成功した。より具体的には、様相論理の証明としてstrongλ□の項を採用し、また述語論理の証明として「依存型」つきのラムダ計算λPの項を採用し、strongλ□の項からλPの項への変換を与えた。そしてこの変換の「健全性」「完全性」「全体性」を示すことにより、これら二つの体系が非常に密接に繋がっていることを証明した。

第三に、様相論理に対応するラムダ計算を定式化する手法に関して、技術的な貢献も行った。具体的には、ラムダ項の型を与えるための「文脈」の扱いに、二つの方法論があり、「単一文脈」と「多重文脈」といわれる。本論文では主に単一文脈を用いて定式化されていたが、他の研究では多重文脈を用いることも少なくない。本論文では、それらが数学的に同一であることを証明し、両方法論に本質的な相違点はないことを示した。

以上を総合し、様相論理とそれに対応するラムダ計算に関する、広範囲な知見を本論文によって得ることができたといえる。よって本論文は博士(情報理工学)の学位請求論文として合格と認められる。