充実期を迎えた線形論理の進化とその応用に関する研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 15300008
• Research Category: Grant-in-Aid for Scientific Research (B)
• Research Institution: Keio University
• Principal Investigator: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• Co-Investigator(Kenkyū-buntansha): 田村 直之 神戸大学, 工学部, 助教授 (60207248) ; 照井 一成 国立情報学研究所, 助手 (70353422) ; 小林 直樹 東京工業大学, 情報理工学研究科, 助教授 (00262155)
• Keywords: 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論

Research Abstract

次の3点を中心に研究を進めた。
1.Reduction Paradigmによる計算モデルとProof-Search Paradigmによる計算モデルを統一的に分析できる論理的枠組の研究。
近年大きな発展を見せているLudics理論は線形論理の基礎概念をベースにしてこれまでのReduction Paradigm(関数型言語の論理計算モデル)とProof-Search Paradigm(論理型言語や証明構成の計算モデル)の内的な統合を可能にする新たな論理体系として注目を集めているが、この理論的な分析をGirardグループと共同で行なった。特にジラールグループが来日し今後の研究計画を立案した。
2.この統一的枠組の具体的応用のための基礎研究。
GirardのLudics理論は線形論理のタイプ推論を一般化して得られた一種の抽象的なタイプ理論であるが、その抽象性の故に具体的タイプ理論的言語との関係が見えにくい面があった。他方でLudicsの枠組は関数型言語の表示的意味論、論理型言語の(エルブランモデル等の)モデル論的意味論を特殊な場合として含み、かつゲーム論的(インターアクティヴな)意味論の側面を与えることも明らかにされている。このLudicsの意味論的方法論を保ちながら、実践的なプログラミング言語意味論の立場から有用な部分を抽出する方法を検討した。
3.この統一的枠組に対する表示的意味論の確立。
これまでに線形論理のPhase Semanticsが単に(線形論理に基づいた)論理型言語の外延的意味論であるばかりでなく、カット消去手続きや広い範囲の関数型言語で採用されているReduction Paradigmにおける証明の正規化(=タイプ論的プログラムの実行の停止性)の分析のための意味論としても適用できることを示してきたが、この定理を我々のLudicsの枠組で捉え直すことにより、プログラム停止性分析に対するより強力で一般的な意味論的手法を研究してきた。又この手法のタイプ付ラムダ計算言語への応用を考察した。

Research Products

• [Publications] H.Kushida, M.Okada: "A proof-theoretic study of the correspondence of classical logic and model logic"Journal of Symbolic Logic. 68・4. 1403-1414 (2003)
• [Publications] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)
• [Publications] K.Hasebe, J-P.Jouannaud, A.Kremer, M.Okada, R.Zumkeller: "Formal Verification of Dynamic Real-Time State-Transition Systems Using Linear Logic"日本ソフトウェア科学会第20回全国大会予稿集. (2003)
• [Publications] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)
• [Publications] H.Mairson, K.Terui: "On the Computational Complexity of Cut-Elimination in Linear Logic"Lecture Notes on Computer Science. 2841. 23-36 (2003)
• [Publications] 照井一成: "素朴集合論とコントラクション"科学哲学. 36・2. 49-64 (2003)
• [Publications] M.Okada, B.Pierce, A.Scedrov, H.Tokuda, A.Yonezawa: "Software Security, Proceedings of the International Symposium on Software Security, 2002"Springer, Hot-topic Series. (2003)