|
Abstract : |
The operational semantics of linear logic programming languages is given in terms of goal-driven sequent calculi. 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 xpoint operator. The bottomup xpoint semantics is important in applications like active databases, and, more in general, for program analysis and veri cation. As a rst case-study, we consider Andreoli and Pareschi's LO [4] enriched with the constant 1. For this language, we give a xpoint semantics based on an operator de ned in the style of TP. We give an algorithm to compute a single application of the xpoint operator where constraints are used to represent in a nite way possibly in nite sets of provable goals. Furthermore, we show that the xpoint semantics for propositional LO without the constant 1 can be computed after nitely many steps. To our knowledge, this is the rst attempt to dene an eective xpoint semantics for LO. We hope that our work will open interesting perspectives for the analysis and verication of linear logic programming languages., |
