Skip Navigation

Journal of Logic and Computation 2002 12(2):321-342; doi:10.1093/logcom/12.2.321
© 2002 by Oxford University Press
This Article
Right arrow Full Text (PDF)
Right arrow Alert me when this article is cited
Right arrow Alert me if a correction is posted
Services
Right arrow Email this article to a friend
Right arrow Similar articles in this journal
Right arrow Similar articles in ISI Web of Science
Right arrow Alert me to new issues of the journal
Right arrow Add to My Personal Archive
Right arrow Download to citation manager
Right arrowRequest Permissions
Google Scholar
Right arrow Articles by Jaume, M.
Right arrow Search for Related Content
Social Bookmarking
Add to CiteULike   Add to Connotea   Add to Del.icio.us  
What's this?

Original Article

On Greatest Fixpoint Semantics of Logic Programming

Mathieu Jaume1

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

Received September 2000.


Add to CiteULike CiteULike   Add to Connotea Connotea   Add to Del.icio.us Del.icio.us    What's this?




Disclaimer:
Please note that abstracts for content published before 1996 were created through digital scanning and may therefore not exactly replicate the text of the original print issues. All efforts have been made to ensure accuracy, but the Publisher will not be held responsible for any remaining inaccuracies. If you require any further clarification, please contact our Customer Services Department.