OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation
Journal of Logic and Computation
Volume 12, Issue 2, April 2002: pp. 321342
On Greatest Fixpoint Semantics of Logic Programming
Mathieu Jaume^{1}
^{1}KIP6SPI, Université Paris 6, 8 rue du Capitaine Scott, 75015 Paris, France. Email: Mathieu.Jaume@lip6.fr
The study of fixpoints has long been at the heart of logic programming. However, whereas least fixpoint semantics works well for SLDrefutations (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 coinductive definitions, we focus on this identification at a deeper level by considering infinite derivations as proofterms in a coinductive 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 onestepinference operator for the Csemantics corresponds to atoms that have a nonfailing fair derivation with the additional property that complete information over a variable is obtained after finitely many steps.
Keywords: Logic programming; infinite SLDderivations; coinductive definitions; fixpoint semantics
Table of Contents
FullText PDF (294 KB)
