线性逻辑程序的有效不动点语义
摘要：线性逻辑程序底层语义的理论基础研究：基于带有常量1的语言LO的LinLog片段。我们使用约束来符号化和有限地表示可能无限的可证目标集合。我们基于Tp风格的新型约束操作符定义了一个基于不动点的语义。该不动点操作符的应用可以通过算法计算。作为终止的充分条件，我们证明了命题LO的不动点计算保证收敛。据我们所知，这是首次尝试为线性逻辑程序定义一种有效的不动点语义。作为我们框架的应用，我们还对LO和联合逻辑编程之间的关系进行了正式研究。使用基于抽象解释的方法，我们证明了DLP的不动点语义可以被视为我们LO语义的一个抽象。我们证明了所得到的抽象对于编码Petri网的一类有趣的LO程序是正确和完备的。
作者：Marco Bozzano, Giorgio Delzanno, Maurizio Martelli
论文ID：cs/0102025
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23