非古典論理によるソフトウェア記述へのアプローチ

点击翻译按钮获取中文摘要

本研究の目的は、非古典論理の分野で発達した証明論あるいは意味論の手法を用いて、ソフトウェア記述システムを分析、設計するための基礎理論を確立することである。昨年度までの研究により、直観主義論理に対するsequent計算の体系と明示的代入計算の間の関係についての結果が得られた。具体的には、型付きラムダ計算のベータ簡約が、直観主義論理に対するsequent計算の体系においてどのような簡約に対応するのかを理解し、そのうえで、明示的代入計算の手法を用いて、簡約の強正規化性を証明した。本年度は、この結果をまとめた論文を「The Seventh International Symposium on Functional and Logic Programming (FLOPS 2004)」で発表し、海外からの参加者からもコメントを頂いた。この結果は、sequent計算に基づく型システムに対する最も基本なものであるため、様々な方向へ拡張することが可能である。現在、特にインターセクション型システムへの拡張と、古典論理・ラムダミュー計算への拡張について検討している。一方、博士論文の研究で開発した部分直観主義論理に対するsequent計算の体系を、tree sequentの手法を用いて述語論理へ拡張し、それを通してヒルベルト流の公理系の完全性を証明した。部分直観主義論理の述語論理に対する公理系を与えることは未解決問題となっていたが、完全な公理系を与えたのは本研究が初めてである。