Application of Logic to Programming Language Theory

逻辑在编程语言理论中的应用

• 批准号: 05808030
• 负责人: OKADA Mitsuhiro
• 金额: $ 1.22万
• 依托单位: Keio University, Faculty of Letters
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1993
• 资助国家: 日本
• 起止时间: 1993 至 1994
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-05808030/
• 关键词: Multi-paradigm programming; Higher order term rewriting; Proof theory; Algebraic specification; Type theory; Typed lambda calculus; Termination problem; Mobile linear logic; 項書き換えシステム; 高階等式言語; 論理的プログラム言語; プログラム検証

We established a logical computation model for a multi-paradigm programming language which combines the two programming paradigms, that for polymorphic typed fanctional language and that for algebraic (equational) specification language. For that purpose, we combined the two logical computation models, polymorphically typed lambda calculus on one hand a higher order and first order term rewrite system on the other hand. In particular, we established a termination criterion and a confluence criterion for the combined computation model. We also implemented the resulting combined programming language.We also studied mobile linear logic, which is an extension of the usual linear logic, in order to capture the paradigm of higher order concurrent programming. Here, our mobile linear logic has the expressive power of Milner's pi-calculus (a calculus for concurrency systems with mobile message passings) and its natural extension (with higher order mobile message passings). The higher order (strong) mobile message passing mechanism was realized by the logical language with self-referential predicates. Such a logical language was introduced by restricting the use of higher order abstract terms, which avoided Russell's paradox even though some sort of self-referential predicates was permitted.

本文建立了一种多范式程序设计语言的逻辑计算模型，它结合了多态类型函数语言和代数（方程）规约语言的两种程序设计范式。为此，我们结合了两个逻辑计算模型，一方面是多态类型的lambda演算，另一方面是高阶和一阶项重写系统。特别地，我们建立了一个终止准则和合流准则的组合计算模型。我们还研究了移动的线性逻辑，它是通常的线性逻辑的扩展，以捕捉高阶并发编程的范例。在这里，我们的移动的线性逻辑具有米尔纳的π演算（并发系统与移动的消息传递的演算）和它的自然扩展（与高阶移动的消息传递）的表达能力。高阶（强）移动的消息传递机制由具有自引用谓词的逻辑语言实现。这种逻辑语言是通过限制高阶抽象项的使用而引入的，这避免了罗素悖论，即使允许某种自指谓词。

项目成果

岡田 光弘: "A Note on the Strong Normalizability of self-referential Logic" Phylosophy(三田哲学会誌). 95. 1-14 (1993)

Mitsuhiro Okada：“关于自指逻辑的强规范化性的注释”哲学（三田哲学会杂志）95. 1-14 (1993)。

Okada: "Concurrent Computation Models Based on Linear Logic" Journal of Information Processing Society of Japan. (to appear.). (1995)

冈田：《基于线性逻辑的并发计算模型》日本信息处理学会杂志。

Okada: "A Note on the Strong Normalizability of the Self-Referential Logic" Philosophy 95 (1993), Mita Philosophical Society. 1-14

冈田：“关于自指逻辑的强规范化性的注释”哲学 95（1993），三田哲学会。

Gui-Okada: "System Description of LAMBDALG (with Y.Gui)" Proc.of Logic Programming and Automated Reasoning, Springer LNCS. (1993)

Gui-Okada：“LAMBDALG 的系统描述（使用 Y.Gui）”Proc.of 逻辑编程和自动推理，Springer LNCS。

岡田光弘: "Note on the Strong Normalizability of the Logic with Self‐Referential Predicates" Philosophy95(1993)Mita Philosophi cal Soc.95. 1-14 (1993)

Mitsuhiro Okada：“关于具有自指谓词的逻辑的强规范化性的注释”Philosophy95（1993）Mita Philosophi cal Soc.95（1993）。