線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析
| Project/Area Number |
09878062
|
|---|
| Research Category |
Grant-in-Aid for Exploratory Research
|
| Allocation Type | Single-year Grants |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Project Period (FY) |
1997 – 1998
|
| Project Status |
Completed (Fiscal Year 1998)
|
| Budget Amount *help |
¥1,900,000 (Direct Cost: ¥1,900,000)
Fiscal Year 1998: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1997: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | 線形論理 / 実現可能計算量 / 実時間システム / 相意味論 / 完全性定理 / カット消去定理 / 形式仕様 / プログラム形式検証 / セマンティクス / タイプ理論 / 並行計算 / 高階論理 / 計算モデル / 正規化定理 |
|---|
| Research Abstract |
J-Y.Girardによって1987年に導入された線形論理は計算資源の消費概念、計算状態の変移概念、並行計算概念などを直接論理的に表現し得るまったく新しい論理体系として注目されている。本研究では、実現可能計算量概念を内に含む論理体系としてGirardによって1996年に導入されたLight Linear Logicと呼ばれる線形論理の部分体系に対する意味論的分析の新しい方法論を確立した。これによって、これまで統語論的立場からのみ分析が可能であったLight Linear Logicの実現可能計算量(多項式時間計算量)概念に対して、純粋に意味論的立場からの分析が可能になった。特に、高階相意味論によるLight Linear Logicの完全性定理及び意味論的カット消去定理証明を与えることに成功した。
又、これまで研究されてきた線形論理による並行計算プログラミングの枠組に、実時間概念を導入することにより、実時間システムに対する仕様・検証理論を与え、この枠組に対する意味論を確立し、完全性定理を証明すると同時に、実時間システムの安全性等の検証問題がPSPACE決定可能なことを示した。
|
Report
(2 results)
Research Products
(16 results)
