1997 年度実績報告書

論理学のプログラム言語理論への応用

研究課題

研究課題/領域番号	09480058
研究機関	慶応義塾大学
研究代表者	岡田光弘慶應義塾大学, 文学部, 教授 (30224025)
キーワード	セマンティクス / タイプ理論 / 並行計算 / 高階論理 / 実現可能計算量 / 計算モデル / 線形論理 / 正規化定理
研究概要	証明の正規化定理に対する新しいセマンティカル(意味論的)な方法論を第1年度(平成9年度)において完成させた。伝統的論理(Horn節論理、直観主義論理/ラムダ計算、等式論理/項書換え系)をを線形論理に置き換えることにより、伝統的プログラミング言語の継起的計算モデルに代わる並行計算モデルが得られるわけであるが、この線形論理に基づく並行計算モデルの性質について分析しておくことが重要である。この観点から線形論理の正規化定理に基づく並行計算モデルの理論を確立した。まず、Girardの意味論は証明可能性概念を捉えるための伝統的な意味論の系譜に属していたが、申請者はこれをカット消去定理(証明の正規化定理)のための意味論に造り変えた(Higher Order Phase Semantics for Completeness,Cut-Elimination and Normalization Proofs,Theoretical Computer Science誌、Special Issue on Linear Logic(1998),近刊)この証明の正規化プロセスを表示し得る新しいPhase Semanticsを、(1)プロセス計算を表す線形論理の部分体系、および(2)Polynomial-Time計算量などの実現可能計算量を通した関数型言語の計算/評価(Evaluation)モデルの分析、を特徴付けるLinght Linear Logicなどの線形論理の部分体系、に適用した。このことにより、(1)線形論理の証明検索概念に基づいた高階並行論理プログラミングおよび並行計算モデルの分析、(2)Light Linear Logicと呼ばれる線形論理の部分体系を用いたPolynomial-Time Computation (多項式計算量)などの実現可能計算量(Feasible Computation)の論理的分析、に対して申請者の新しい意味論的枠組を適用できることとなった。

研究成果
(8件)

すべてその他

すべて文献書誌 (8件)

[文献書誌] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (to appear). (1998)
[文献書誌] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). (1998)
[文献書誌] M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)
[文献書誌] J-P.Jouannaund, M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)
[文献書誌] M.Hamano-M.Okada: "A Relationship Among Gentzen's Proof Reduction,Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)
[文献書誌] M.Kanobitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)
[文献書誌] M.Okada: "Types and Proofs(2chapters分担)" Mathematical Sciety of Japan(近刊), (1998)
[文献書誌] 岡田光弘: "情報科学のための論理学" 産業図書, 250 (1998)

1997 年度 実績報告書

論理学のプログラム言語理論への応用

研究代表者

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

研究成果

[文献書誌] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (to appear). (1998)

[文献書誌] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). (1998)

[文献書誌] M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)

[文献書誌] J-P.Jouannaund, M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)

[文献書誌] M.Hamano-M.Okada: "A Relationship Among Gentzen's Proof Reduction,Kirby-Paris Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)

[文献書誌] M.Kanobitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)

[文献書誌] M.Okada: "Types and Proofs(2chapters分担)" Mathematical Sciety of Japan(近刊), (1998)

[文献書誌] 岡田光弘: "情報科学のための論理学" 産業図書, 250 (1998)

1997 年度実績報告書

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