線形論理の意味論的手法による並行計算概念および実行可能計算量概念の論理的分析

使用线性逻辑的语义方法对并行计算概念和可执行复杂性概念进行逻辑分析

• 批准号: 09878062
• 负责人: 岡田 光弘
• 金额: $ 1.22万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Exploratory Research
• 财政年份: 1997
• 资助国家: 日本
• 起止时间: 1997 至 1998
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-09878062/
• 关键词: 線形論理; 実現可能計算量; 実時間システム; 相意味論; 完全性定理; カット消去定理; 形式仕様; プログラム形式検証; セマンティクス; タイプ理論; 並行計算; 高階論理; 計算モデル; 正規化定理

J-Y.Girardによって1987年に導入された線形論理は計算資源の消費概念、計算状態の変移概念、並行計算概念などを直接論理的に表現し得るまったく新しい論理体系として注目されている。本研究では、実現可能計算量概念を内に含む論理体系としてGirardによって1996年に導入されたLight Linear Logicと呼ばれる線形論理の部分体系に対する意味論的分析の新しい方法論を確立した。これによって、これまで統語論的立場からのみ分析が可能であったLight Linear Logicの実現可能計算量(多項式時間計算量)概念に対して、純粋に意味論的立場からの分析が可能になった。特に、高階相意味論によるLight Linear Logicの完全性定理及び意味論的カット消去定理証明を与えることに成功した。又、これまで研究されてきた線形論理による並行計算プログラミングの枠組に、実時間概念を導入することにより、実時間システムに対する仕様・検証理論を与え、この枠組に対する意味論を確立し、完全性定理を証明すると同時に、実時間システムの安全性等の検証問題がPSPACE決定可能なことを示した。

由J-Y介绍。吉拉德（Girard）在1987年，线性逻辑正在作为一个全新的逻辑系统引起关注，可以直接从逻辑上表达消耗计算资源的概念，改变计算状态的概念以及平行计算计算的概念。这项研究建立了一种新方法，用于对线性逻辑子系统的语义分析，称为Light Linear Logic，该系统由Girard于1996年作为一个逻辑系统引入，其中包含可实现的复杂性概念。这使得可以分析光线线性逻辑可行计算复杂性（多项式时间计算复杂性）概念的纯粹语义视图，该逻辑以前仅允许从句法的角度进行分析。特别是，我们成功地提供了基于高阶语义的光线性逻辑定理和语义剪切消除定理。此外，通过将实时概念引入使用线性逻辑的平行计算编程框架，直到现在，我们为实时系统提供了规范和验证理论，为该框架建立语义，证明完美定理，并显示PSPACE可以确定PSPACE的验证问题，例如实时系统安全。

项目成果

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

M.Hamano-M.Okada：《布霍尔茨九头蛇博弈的直接独立性证明》Archiev，数学逻辑。

M.Kanovitch-M.Okada -A.Scedrov: "Specifying Real-Time Finits State Systems by Linear Logic" Electronic Notes of Theoretical Computer Science. 16(1998). 1-14 (1998)

M.Kanovitch-M.Okada -A.Scedrov：“通过线性逻辑指定实时有限状态系统”理论计算机科学电子笔记。

M.Okada: "An Introduction to Linear Logic : Phase Semantics and Expressiveness" Memoirs of Mathematical Society of Japan. 2. 255-295 (1998)

M.Okada：“线性逻辑导论：相位语义和表现力”日本数学会回忆录。

M.Kanovitch,M.Okada,A.Scedrov: "Phase Semantics for Light Linear Logic" Electronic Notes of Theoretical Computer Science. 6. 1-14 (1997)

M.Kanovitch、M.Okada、A.Scedrov：“轻线性逻辑的相位语义”理论计算机科学电子笔记。

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

M.Okada-K.Terui：“直觉线性逻辑各种片段的有限模型属性”J.Symbolic Logic。