A Bottom-up Semantics for LO

Marco Bozzano, Giorgio Delzanno and Maurizio Martelli

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

Abstract

The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi for fragments of the logic. The proof-theoretic presentation is the natural counterpart of the top-down semantics of traditional logic programs. In this paper we investigate the theoretical foundation of an alternative operational semantics based on a bottom-up evaluation of linear logic programs via a fixpoint operator. The bottom-up fixpoint semantics is important in applications like active databases, and, more in general, for program analysis and verification.

As a first case-study, we consider Andreoli and Pareschi's LO enriched with the connective 1 (one). For this language, we give a fixpoint semantics based on an operator defined in the style of Tp We give an algorithm to compute a single application of the fixpoint operator where constraints are used to represent in a finite way possibly infinite sets of provable goals. Furthermore, we show that the fixpoint semantics for propositional LO without the connective 1 can be computed after finitely many steps.

To our knowledge, this is the first attempt to define an effective fixpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verification of linear logic programming languages.