A Functorial Framework for Constraint Normal Logic Programming

The semantic constructions and results for definite programs do not extend when dealing with negation. The main problem is related to a well-known problem in the area of algebraic specification: if we fix a constraint domain as a given model, its free extension by means of a set of Horn clauses defining a set of new predicates is semicomputable. However, if the language of the extension is richer than Horn clauses its free extension (if it exists) is not necessarily semicomputable. In this paper we present a framework that allows us to deal with these problems in a novel way. This framework is based on two main ideas: a reformulation of the notion of constraint domain and a functorial presentation of our semantics. In particular, the semantics of a logic program P is defined in terms of three functors: that apply to constraint domains and provide the operational, the least fixpoint and the logical semantics of P, respectively. To be more concrete, the idea is that the application of to a specific constraint solver provides the operational semantics of P that uses this solver; the application of to a specific domain provides the least fixpoint of P over this domain; and, the application of to a theory of constraints provides the logic theory associated to P. In this context, we prove that these three functors are in some sense equivalent.