线性逻辑程序的有效固定点语义
编程语言
2007-05-23 v2
摘要
本文我们研究一种新的底向语义的理论基础，具体来说是 LinLog 片段的语义，即由常数 1 丰富的 LO 语言。我们使用约束来符号地和有限地表示可能的无限可证目标集合。我们基于一种新的算子定义固定点语义，类似于 Tp 在约束上工作。固定点算子的应用可以算法地计算。作为充分条件，我们表明对于命题 LO，固定点计算保证收敛。鉴于目前所知，这是对线性逻辑程序定义有效固定点语义的第一次尝试。作为本框架的应用，我们还提出了一个关于 LO 与 Disjunctive Logic Programming 关系的形式化调查。我们使用基于抽象解释的ethods，我们表明 DLP 固定点语义可以视为我们对 LO 语义的一个抽象。我们证明了该抽象对编码有用 Petri 网的 LO 程序的一个有趣类是正确且完整的。
引用
@article{arxiv.cs/0102025,
title = {An Effective Fixpoint Semantics for Linear Logic Programs},
author = {Marco Bozzano and Giorgio Delzanno and Maurizio Martelli},
journal= {arXiv preprint arXiv:cs/0102025},
year = {2007}
}
备注
39 pages, 5 figures. To appear in Theory and Practice of Logic Programming