| 研究課題/領域番号 |
09878062
|
|---|
| 研究種目 |
萌芽的研究
|
| 配分区分 | 補助金 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 慶応義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| 研究期間 (年度) |
1997 – 1998
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
1,900千円 (直接経費: 1,900千円)
1998年度: 800千円 (直接経費: 800千円)
1997年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | 線形論理 / 実現可能計算量 / 実時間システム / 相意味論 / 完全性定理 / カット消去定理 / 形式仕様 / プログラム形式検証 / セマンティクス / タイプ理論 / 並行計算 / 高階論理 / 計算モデル / 正規化定理 |
|---|
| 研究概要 |
J-Y.Girardによって1987年に導入された線形論理は計算資源の消費概念、計算状態の変移概念、並行計算概念などを直接論理的に表現し得るまったく新しい論理体系として注目されている。本研究では、実現可能計算量概念を内に含む論理体系としてGirardによって1996年に導入されたLight Linear Logicと呼ばれる線形論理の部分体系に対する意味論的分析の新しい方法論を確立した。これによって、これまで統語論的立場からのみ分析が可能であったLight Linear Logicの実現可能計算量(多項式時間計算量)概念に対して、純粋に意味論的立場からの分析が可能になった。特に、高階相意味論によるLight Linear Logicの完全性定理及び意味論的カット消去定理証明を与えることに成功した。
又、これまで研究されてきた線形論理による並行計算プログラミングの枠組に、実時間概念を導入することにより、実時間システムに対する仕様・検証理論を与え、この枠組に対する意味論を確立し、完全性定理を証明すると同時に、実時間システムの安全性等の検証問題がPSPACE決定可能なことを示した。
|
