Logic Programming, Substitutions and Finite Computability

Abstract

Apt and van Emden have studied the semantics of logic programming by means of fixed point methods. From a model theoretic point of view, their formalisation is very nice. Least and greatest fixed points correspond to least and greatest Herbrand-models respectively.

Viewed operationally, there is an ugly asymmetry. The least fixed point expresses finite computability, but the greatest fixed point denotes negation by trans-finite failure, i.e. the underlying operator is not omega-continuous for decreasing chains in general.

We use the notion of finite computability inherent in Scott domains to build a domainlike construction (the cd-domain) that offers omega-continuity for increasing and decreasing chains equally. On this basis negation by finite failure is expressed in terms of a fixed point.

The fixed point semantics of Apt and van Emden is very abstract concerning the concept of substitution, although it is fundamental for any implementation. Hence it becomes quite tedious to prove the correctness of a concrete resolution algorithm. The fixed point semantics of this paper offers an intermediate step in this respect. Any commitments to specific resolution strategies are avoided, and the semantics may be the basis of sequential and parallel implementations equally. Simultaneously the set of substitution dataobjects is structured by a Scott information theoretic partial order, namely the cd-domain.