線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析

1998 年度 実績報告書

• 研究課題/領域番号: 09878062
• 研究機関: 慶応義塾大学
• 研究代表者: 岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
• キーワード: 線形論理 / 実現可能計算量 / 実時間システム / 相意味論 / 完全性定理 / カット消去定理 / 形式仕様 / プログラム形式検証

研究概要

J-Y.Girardによって1987年に導入された線形論理は計算資源の消費概念、計算状態の変移概念、並行計算概念などを直接論理的に表現し得るまったく新しい論理体系として注目されている。本研究では、実現可能計算量概念を内に含む論理体系としてGirardによって1996年に導入されたLight Linear Logicと呼ばれる線形論理の部分体系に対する意味論的分析の新しい方法論を確立した。これによって、これまで統語論的立場からのみ分析が可能であったLight Linear Logicの実現可能計算量(多項式時間計算量)概念に対して、純粋に意味論的立場からの分析が可能になった。特に、高階相意味論によるLight Linear Logicの完全性定理及び意味論的カット消去定理証明を与えることに成功した。
又、これまで研究されてきた線形論理による並行計算プログラミングの枠組に、実時間概念を導入することにより、実時間システムに対する仕様・検証理論を与え、この枠組に対する意味論を確立し、完全性定理を証明すると同時に、実時間システムの安全性等の検証問題がPSPACE決定可能なことを示した。

研究成果

• [文献書誌] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Prcofs of Slassical Linear Logic" Theoretical Computer Science. (近刊). (1999)
• [文献書誌] M.Okada-K.Terui: "Finite Model Property for Various Fragments of Intuiticnistic Linear Logic" Journal of Symbolic Logic. (近刊). (1999)
• [文献書誌] M.Okada: "An Introduction to Linear Logic : Phase Semantics and Expressiveness" Memoirs of Mathematical Society of Japan. 2. 255-295 (1998)
• [文献書誌] M.Kancvitch-M.Okada-A.Scedrov: "Phase Semantics for Light Lineay Logic" Theoretical Computer Science. (近刊). (1999)
• [文献書誌] M.Kanovitch-M.Okada -A.Scedrov: "Specifying Real-Time Finits State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16(1998). 1-14 (1998)
• [文献書誌] M.Hamano-M.Okada: "A Direct Independence Proof of Buchholz's Hydra Game" Archive for Mathematical Logic. 37. 67-89 (1998)
• [文献書誌] M.Takahashi-M.Okada.-M.Dezani(eds.): "Theories of Types and Proofs" Mathematical Society of JAPAN(日本数学会), 297 (1998)
• [文献書誌] J.-Y.Girard-M.Okada-A.Scedrov(eds.): "Linear Logic Special Volumes I,II of Theoretical Computer science(近刊)" Elsevier Science Publishing, (1999)