2004 Fiscal Year Annual Research Report
充実期を迎えた線形論理の進化とその応用に関する研究
| Project/Area Number |
15300008
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小林 直樹 東北大学, 大学院・情報科学研究科, 教授 (00262155)
照井 一成 国立情報学研究所, 助手 (70353422)
田村 直之 神戸大学, 工学部, 教授 (60207248)
|
|---|
| Keywords | 論理的手法 / 線形論理 / 形式仕様 / 形式検証 / 実時間システム / 証明論 |
|---|
| Research Abstract |
次の3点を中心に研究を進めた。
1.線形論理のSimple Logic的観点による分析。
線形論理の基礎を成す部分体系Simple Logicが単純Phase modelsに対して完全であることを示し、又これを種々な観点から改良した(主に岡田グループと照井との共同研究)。又、Simple Logicに基づいて、線形論理のProof-search及びProof-reductionsの分析を開始した。又、直観主義線形論理のPhase Semanticsに対する分析を行った(照井、岡田)。
2.線形論理的枠組を用いた具体的応用のための基礎研究。
消費概念と非消費概念の区別を顕在化する線形論理の観点を用いて、証明論的手法の形式仕様・形式検証理論への応用を進めた。特に、実時間計算システム及びセキュリティプロトコル検証システムへの応用を行った(岡田グループと田村グループの共同研究)。消費概念等のプログラミング言語理論への応用を進めた(岡田グループ、小林グループ)。
3.統一的枠組に対する表示的意味論の確立。
これまでに線形論理のPhase Semanticsが単に(線形論理に基づいた)論理型言語の外延的意味論であるばかりでなく、カット消去手続きや広い範囲の関数型言語で採用されているReduction Paradigmにおける証明の正規化(=タイプ論的プログラムの実行の停止性)の分析のための意味論としても適用できることを示してきたが、今年度は特に直観主義論理及び線形論理の具体的な部分体系に対してPhase Semanticsによる正規化定理を研究した。
|
