arXivDaily arXiv每日学术速递 周一至周五更新
arXiv周末暂无论文更新,休息一下吧,周末愉快~~
arXiv cs/0102025cs.PL
收藏

一种有效的线性逻辑程序不动点语义

An Effective Fixpoint Semantics for Linear Logic Programs

Marco Bozzano, Giorgio Delzanno, Maurizio Martelli

摘要:

在本文中,我们调查的理论基础,一个新的自下而上的语义线性逻辑程序,更确切地说,为片段的LinLog,包括语言LO丰富的常数1。我们使用约束来象征性地和非象征性地表示可能无限的可证明目标的集合。我们基于TP处理约束风格的新运算符定义了不动点语义。不动点算子的应用可以通过算法来计算。作为终止的充分条件,我们证明了不动点计算是保证收敛命题LO。据我们所知,这是首次尝试为线性逻辑程序定义有效的不动点语义。作为我们的框架的应用,我们还提出了一个正式的调查LO和析取逻辑编程之间的关系。使用一种基于抽象解释的方法,我们表明,DLP不动点语义可以被视为我们的语义LO的抽象。我们证明,由此产生的抽象是正确的和完整的一个有趣的类LO程序编码Petri网。

英文摘要:

In this paper we investigate the theoretical foundation of a new bottom-up semantics for linear logic programs, and more precisely for the fragment of LinLog that consists of the language LO enriched with the constant 1. We use constraints to symbolically and finitely represent possibly infinite collections of provable goals. We define a fixpoint semantics based on a new operator in the style of Tp working over constraints. An application of the fixpoint operator can be computed algorithmically. As sufficient conditions for termination, we show that the fixpoint computation is guaranteed to converge for propositional LO. To our knowledge, this is the first attempt to define an effective fixpoint semantics for linear logic programs. As an application of our framework, we also present a formal investigation of the relations between LO and Disjunctive Logic Programming. Using an approach based on abstract interpretation, we show that DLP fixpoint semantics can be viewed as an abstraction of our semantics for LO. We prove that the resulting abstraction is correct and complete for an interesting class of LO programs encoding Petri Nets.

机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。

↑