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 合着）：“非交换乘法线性逻辑的图论表征”理论计算机科学电子笔记（欧洲理论信息学会）。

岡田光弘(浜野と共著): "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 年）。

岡田光弘(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 年）

M.Nagayama and M.Okada: "A Graph Theoretic Characterization of Multiplicative Fragment of Non-Commutative Linear Logic" Electronic Notes of Theoretical Computer Science. vol.3. 13 (1996)

M.Nagayama 和 M.Okada：“非交换线性逻辑乘法片段的图论表征”理论计算机科学电子笔记。