Girard's Linear Logic and its Application

吉拉德的线性逻辑及其应用

• 批准号: 07808035
• 负责人: OKADA Mitsuhiro
• 金额: $ 1.34万
• 依托单位: Keio University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Scientific Research (C)
• 财政年份: 1995
• 资助国家: 日本
• 起止时间: 1995 至 1996
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-07808035/
• 关键词: Linear Logic; Phase Semantics; Concurrent Processes; Normalization; Cut-Elimination; Functional Programming; Logic Programming; Logical Computation Model; Phase Semantics; 証明論; 正規化定性; プログラミング言語

We established various computation models based on linear logic and their sematics. (1) In the framework of the proof-search paradigm we investigate a computation model for concurrent processes for a linear-logic based process calculus. We established semantic techniques for analysing the concurrent processes. For example, we modified the phase semantics to obtain a semantic characterization theorem for observable processes. (2) In the framework of the reduction paradigm we investigate a computation model for linear logic based typed functional programming languages. We established a new semantic framework to prove the strong normalization property. Our method is very powerful in the sense that the strong normalizability for various different logical systems are shown uniformly. (3) We applied the above semantic method to establish the semantics for Light Linear Logic, a special subsystem of Linear Logic which characterizes the polynomial-time computation. Then we investigated the polynomial computation model using this semantic framework.

建立了基于线性逻辑及其语义的各种计算模型。(1)在证明-搜索范式的框架下，我们研究了基于线性逻辑的进程演算的并发进程计算模型。我们建立了用于分析并发进程的语义技术。例如，我们对阶段语义进行了修改，得到了可观测过程的语义刻画定理。(2)在归约范式的框架下，研究了基于线性逻辑的类型化函数式程序设计语言的计算模型。我们建立了一个新的语义框架来证明强归一化性质。我们的方法是非常强大的，因为我们统一地证明了各种不同逻辑系统的强归一化能力。(3)应用上述语义方法建立了轻线性逻辑的语义，它是线性逻辑的一个特殊的子系统，具有多项式时间计算的特点。然后研究了基于该语义框架的多项式计算模型。

项目成果

岡田光弘(浜野正浩との共著): "A Relationship Among Gentzen's Proof Reduction,Kirby-Paris' Hydra Game and Buchhlz's Hydra Game" Mathematical Logic Quarterly. 43. 103-120 (1997)

Mitsuhiro Okada（与 Masahiro Hamano 合着）：“Gentzen 的证明还原、Kirby-Paris 的 Hydra Game 和 Buchhlz 的 Hydra Game 之间的关系”《数学逻辑季刊》43. 103-120 (1997)。

岡田光弘(永山との共著): "A Graph-theoretic characterization for non-commutative Multilicative Linear Logic" Electronic Notes of Theoretical Computer Science (ヨーロッパ理論情報学会). 3. 11 (1996)

Mitsuhiro Okada（与 Nagayama 合着）：“非交换乘法线性逻辑的图论表征”理论计算机科学电子笔记（欧洲理论信息学会）。

岡田光弘(M.Kanovitch,A.Scedrovとの共著): "In Proceedings of International Conference on the Mathematical Foundations of Programming Seunantics" Springer(近刊), (1997)

Mitsuhiro Okada（与 M.Kanovitch 和 A.Scedrov 合着）：“程序设计数学基础国际会议论文集”Springer（即将出版），（1997 年）

岡田光弘(浜野と共著): "Relationship Among Gentzen's Reduction, Kirby-Paris' Hydra Game and Buchholz's Hydra Game" Mathematical Logic Quarterly. 近刊. (1996)

Mitsuhiro Okada（与 Hamano 合着）：《Gentzen 的归约、Kirby-Paris 的 Hydra Game 和 Buchholz 的 Hydra Game 之间的关系》即将出版（Mathematical Logic Quarterly）（1996 年）。

J-P.Jouannaud and M.Okada: "Abstract Data Type Systems" Theoretical Computer Science. (to appear). (1997)

J-P.Jouannaud 和 M.Okada：“抽象数据类型系统”理论计算机科学。