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
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
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.