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

• Project/Area Number: 02J02624
• Research Category: Grant-in-Aid for JSPS Fellows
• Allocation Type: Single-year Grants
• Section: 国内
• Research Field: 計算機科学
• Research Institution: Tohoku University (2004); Chiba University (2002-2003)
• Principal Investigator: 菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
• Project Period (FY): 2002 – 2004
• Project Status: Completed (Fiscal Year 2004)
• Budget Amount: ¥3,400,000 (Direct Cost: ¥3,400,000); Fiscal Year 2004: ¥1,000,000 (Direct Cost: ¥1,000,000); Fiscal Year 2003: ¥1,200,000 (Direct Cost: ¥1,200,000); Fiscal Year 2002: ¥1,200,000 (Direct Cost: ¥1,200,000)
• Keywords: 数理論理学 / 理論計算機科学 / プログラム理論

Research Abstract

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

Research Products

• [Journal Article] Direct Proof of Strong Normalization for an Extended Herbelin's Calculus (2004)
  • Author(s): Kentaro Kikuchi
  • Journal Title: Lecture Notes in Computer Science Vol.2998 Pages: 244-259
• [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. (発表予定).
• [Publications] Kentaro Kikuchi, Katsumi Sasaki: "A Cut-Free Gentzen Formulation of Basic Propositional Calculus"Journal of Logic, Language and Information. (発表予定).