1997 Fiscal Year Annual Research Report
| Project/Area Number |
09480058
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Keywords | セマンティクス / タイプ理論 / 並行計算 / 高階論理 / 実現可能計算量 / 計算モデル / 線形論理 / 正規化定理 |
|---|
| Research Abstract |
証明の正規化定理に対する新しいセマンティカル(意味論的)な方法論を第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)の論理的分析、に対して申請者の新しい意味論的枠組を適用できることとなった。
|
-
[Publications] M.Okada: "Phase Semantics for Higher Order Completeness,Cut-Elimination and Normalization Proofs of Classical Linear Logic" Theoretical Computer Science. (to appear). (1998)
-
[Publications] M.Okada-K.Terui: "The Finite Model Property for Various Fragments of Intuitionistic Linear Logic" J.Symbolic Logic. (to appear). (1998)
-
[Publications] M.Hamano-M.Okada: "A Direct Independence Proof of Buhholz's Hydra Game" Archiev for Mathematical Logic. (to appear). (1998)
-
[Publications] J-P.Jouannaund, M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. 173. 349-391 (1997)
-
[Publications] 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)
-
[Publications] M.Kanobitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)
-
[Publications] M.Okada: "Types and Proofs(2chapters分担)" Mathematical Sciety of Japan(近刊), (1998)
-
[Publications] 岡田光弘: "情報科学のための論理学" 産業図書, 250 (1998)
