Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue
 
home
browse
current
etoc
authors
subinfo
subscribers
samples

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 12, Issue 2, April 2002: pp. 321-342

On Greatest Fixpoint Semantics of Logic Programming

Mathieu Jaume1

1KIP6-SPI, Université Paris 6, 8 rue du Capitaine Scott, 75015 Paris, France. E-mail: 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 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.

Keywords: Logic programming; infinite SLD-derivations; co-inductive definitions; fixpoint semantics

Table of Contents   Full-Text PDF (294 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement