2003 年度実績報告書

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

研究課題

研究課題/領域番号	15300008
研究種目	基盤研究(B)
研究機関	慶應義塾大学
研究代表者	岡田光弘慶應義塾大学, 文学部, 教授 (30224025)
研究分担者	田村直之神戸大学, 工学部, 助教授 (60207248) 照井一成国立情報学研究所, 助手 (70353422) 小林直樹東京工業大学, 情報理工学研究科, 助教授 (00262155)
キーワード	論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論
研究概要	次の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の枠組で捉え直すことにより、プログラム停止性分析に対するより強力で一般的な意味論的手法を研究してきた。又この手法のタイプ付ラムダ計算言語への応用を考察した。

研究成果

(7件)

すべてその他

すべて文献書誌 (7件)

[文献書誌] 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)
[文献書誌] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)
[文献書誌] 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)
[文献書誌] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)
[文献書誌] H.Mairson, K.Terui: "On the Computational Complexity of Cut-Elimination in Linear Logic"Lecture Notes on Computer Science. 2841. 23-36 (2003)
[文献書誌] 照井一成: "素朴集合論とコントラクション"科学哲学. 36・2. 49-64 (2003)
[文献書誌] 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)

2003 年度 実績報告書

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

研究代表者

岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)

研究成果

[文献書誌] 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)

[文献書誌] Mitsuhiro Okada: "Linear Logic and Intuitionistic Logic"La revue internationale de philosophie. (近刊). (2004)

[文献書誌] 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)

[文献書誌] 岡田光弘: "矛盾は矛盾か"科学哲学. 36・2. 79-102 (2004)

[文献書誌] H.Mairson, K.Terui: "On the Computational Complexity of Cut-Elimination in Linear Logic"Lecture Notes on Computer Science. 2841. 23-36 (2003)

[文献書誌] 照井一成: "素朴集合論とコントラクション"科学哲学. 36・2. 49-64 (2003)

[文献書誌] 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)

2003 年度実績報告書

岡田光弘慶應義塾大学, 文学部, 教授 (30224025)