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：“抽象数据类型系统”理论计算机科学。