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

2003 Fiscal Year Annual Research Report

• Project/Area Number: 02J02624
• Research Institution: Chiba University
• Principal Investigator: 菊池 健太郎 千葉大学, 理学部, 特別研究員(PD) (40396528)
• Keywords: 数理論理学 / 理論計算機科学 / プログラム理論

Research Abstract

本研究の目的は、非古典論理の分野で発達した証明論あるいは意味論の手法を用いて、ソフトウェア記述システムを分析、設計するための基礎理論を確立することである。昨年度の研究により、直観主義論理に対するsequent計算の体系と明示的代入計算との間の関係について結果が得られた。具体的には、型付きラムダ計算のベータ簡約が、直観主義論理に対するsequent計算の体系においてどのような簡約に対応するのかを理解し、そのうえで、明示的代入計算の手法を用いて、簡約の強正規化性を証明した。今年度の前半には、ドレスデン工科大学で開かれたProof Theory, Computation and Complexityワークショップに参加し、この内容に密接に関連する研究者であるRoy Dyckhoff氏、Stephane Lengrand氏から貴重なコメントをいただいた。その後、証明の改善に努め、論文にまとめた。この結果は、「The Seventh International Symposium on Functional and Logic Programming(FLOPS2004)」で発表する予定となっている。また、「第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)」でも発表し、参加者からコメントを頂いた。
今年度の後半には、上記の体系をインターセクション型システムに拡張し強正規化性を特徴付けることを目指した。これは、通常のラムダ計算に対する縮約可能性法を用いない強制規化性の証明とも関連しており、その証明をsequent計算の体系を用いて与えることに成功した。さらに、この方法は強正規化性以外の様々な性質に対しても適用することができ、特に論理的近似定理の簡単な証明を与えることができた。現在、これらの手法を古典論理とラムダ・ミュー計算に拡張することを検討している。

Research Products

• [Publications] Kentaro Kikuchi, Katsumi Sasaki: "A Cut-Free Gentzen Formulation of Basic Propositional Calculus"Journal of Logic, Language and Information. 12・2. 213-225 (2003)
• [Publications] Kentaro Kikuchi: "A Direct Proof of Strong Normalization for an Extended Herbelin's Calculus"Proceedings of 7th International Symposium on Functional and Logic Programming. (発表予定).