Semantics of a logic program

The study of fixpoints has long been at the heart of logic programming.  However, whereas least fixpoint semantics works well for SLD-refutations (i.e. is sound and complete), there is no satisfactory (i.e. complete) fixpoint semantics for infinite derivations. In this paper, we focus on this problem. Standard approaches in this area consist in concentrating on infinite derivations that can be seen as computing, in the limit, some infinite object. This is usually done by extending the domain of computation with infinite elements and then defining the meaning of programs in terms of greatest fixpoints. The main drawback of these approaches is that the semantics defined is not complete. Hence, since defining a greatest fixpoint semantics for logic programs amounts to consider a program as a set of co-inductive definitions, we focus on this identification at a deeper level by considering infinite derivations as proof-terms in a co-inductive set. This reading leads into considering derivations as proofs rather than computations and allows one to show that for the subclass of infinite derivations over the domain of finite terms, a complete greatest fixpoint semantics can be obtained. Our main result is that the greatest fixpoint of the one-step-inference operator for the C-semantics corresponds to atoms that have a non-failing fair derivation with the additional property that complete information over a variable is obtained after finitely many steps

The variety of semantical approaches that have been invented for logic
programs is quite broad, drawing on classical and many-valued logic, lattice
theory, game theory, and topology. One source of this richness is
the inherent non-monotonicity of its negation, something that does not
have close parallels with the machinery of other programming paradigms.
Nonetheless, much of the work on logic programming semantics seems to
exist side by side with similar work done for imperative and functional
programming, with relatively minimal contact between communities.
In this paper we summarize one variety of approaches to the semantics
of logic programs: that based on ¯xpoint theory. We do not attempt to
cover much beyond this single area, which is already remarkably fruitful.
We hope readers will see parallels with, and the divergences from
the better known ¯xpoint treatments developed for other programming
methodologies.

1 Introduction
A logic program consists of formulas of logic, generally written using some
special, restricted syntax. One `runs' a logic program by asking it questions|
queries|and it is determined, by executing a proof engine, whether or not
these queries follow from the program. Queries may contain free variables, in
? I want to thank Howard Blair for a number of suggestions that improved the
presentation in this paper.
Preprint submitted to Elsevier Preprint 23 August 2000
which case the intention is to determine for what values of the variables the
queries follow from the program.
The preceding is a very general description, with much room for maneuver.
A particular choice of syntax can place serious restrictions on programs that
can be written or queries that can be asked. The choice of logic was left open
above. Classical ¯rst-order logic is an obvious candidate, but incompleteness
results tell us that, while we may be able to determine a query does follow,
we can not in general tell that it does not, and this a®ects the treatment of
negation. Consequently, subsystems of classical logic are of interest. In the
other direction, richer systems that permit numeric constraints or allow additional
operators, such as temporal ones, are also of much interest. And ¯nally,
what about a proof engine? Completeness, in the classical sense, may be less
important than e±ciency on `probable' queries. Thus a rich variety of systems
¯t into the general paradigm of logic programming. Prolog is the most familiar
logic programming system today, though others have been implemented and
experimented with.
The general description of logic programming above makes it clear that it is
related to database query languages. The machinery provided is richer than
is customary in that community, however. One piece of machinery that is
commonly available is negation. In a simple database language, negation is
not a problem (except possibly for e±ciency considerations). Either an item
is in a database, or it is not, and these facts can be reported no matter what.
But if a system is built on classical ¯rst-order logic, negation can be a serious
issue. Prolog without negation can, in a precise sense, compute exactly the
recursively enumerable relations. If negation is added we would expect to have
complements of recursively enumerable relations as well, and we know this is
impossible. Instead a weaker version of negation is used|negation as failure.
One concludes not X if X is not a consequence.
Negation as failure is inherently non-monotonic. If X is not a consequence
of a particular program, so that not X is a conclusion, then if X is added
to the program, the conclusion not X must be withdrawn. Moreover, it is
not decidable in general that something is not a consequence. As a result of
these considerations, more than one version of negation has been investigated.
Non-monotonic logic is now seen as a close relative of logic programming, and
developments in either area tend to a®ect both.
Since logic programming involves both logic and programming, it should not
be surprising that several varieties of semantics have been developed for it.
Some follow the model-theoretic approach of formal logic, and some are more
like the ¯xpoint approach originally developed for imperative and functional
programming. There are also game-theoretic approaches. The overall range of
proposed semantics is vast, and somewhat bewildering.
2
In this survey paper we will almost entirely con¯ne the discussion of logic
programming semantics to the ¯xpoint approach. We will try to emphasize
similarities with semantics developed for other programming paradigms. We
do not mean to be encyclopedic|by now it really would require an encyclopedia.
We will con¯ne things to developments that have been of particular
interest to the author. Others will have their own story to tell.