Encapsulating data in Logic Programming via Categorical Constraints

Technical Report∗

James Lipton Robert McGrail Dept. of Mathematics Wesleyan University

                     http://www.cs.wesleyan.edu/

July 9, 1998

Abstract We define a framework for writing executable declarative specifications which incorporate categorical constraints on data, Horn Clauses and datatype specification over finite-product categories. We construct a generic extension of a base syntactic category of constraints in which arrows correspond to resolution proofs subject to the specified data constraints.

1 Introduction

Much of the research in logic programming is aimed at expanding the expressive power and efficiency of declarative languages without compromising the logical transparency commitment: programs should (almost) read like specifications. One approach is to place more expressive power and more of the control components into the logic itself, possibly by expanding the scope of the underlying mathematical formalism. This has been the goal of constraint logic programming (CLP, Set constraints, Prolog III), and extensions to higher-order and linear logic, to name a few such efforts. This paper is a step in this direction. Rather than expand the logic itself, we consider two extensions of the underlying syntactical foundation, using fairly simple categorical tools. Categorical syntax and proof theory for logic programming permits a powerful extension of conventional logic programming to be built in a manner that does not compromise declarity and that admits a similar semantical treatment to conventional logic programming.

The encoding dilemma. The main contribution of the paper is a new approach to defining syntactic extensions to specify data types and constraints as independent components, somewhat in the spirit of modules in functional programming.

This information is processed by extending the logic programming interpreter dynamically with new rules. In traditional logic programming, this kind of information is coded directly into the Horn logic, often very cleverly, in a way that may obscure the intended meaning of the code, despite the fact that it is logical. Soundness and completeness of the target logic says nothing about the correctness of the encoding. We propose expanding the specification formalism in a way that admits direct definitions of data and constraint information that are already mathematically clear, or verified elsewhere using appropriate tools. We consider a datatype defintion construct and a very liberal notion of constraint based on finite product categories, of which equational constraint systems are a special case. We make use of a categorical foundation developed in [9], and similar in spirit to, e.g. [1, 4, 5, 21]. Although the framework admits extensions to Hereditarily Harrop or Higher-order logic, we will only consider Horn logic here.

∗some of these results appeared in proc. ALP98, LNCS, Springer.

An Example: It will be useful to give an example of the kind of code that is admitted by the extensions discussed in this paper.

begin module "list"
 datatype 'a list =  nil | cons of 'a * 'a list
  begin
    fun length nil = (0:int)
     |  length (cons (a,t)) = 1 + length t
  end;
 even(0:int).
 even(X) :- even(X - 2).
 length_of(Z, length Z).
end module;
? - list even (cons(2,(cons(4,(cons(6,nil)))))).

- yes

? - pred[length](cons (2,(cons (4,(cons (5,nil))))),A).

- A = 3

? - length_of((cons (2,(cons (4,(cons (5,nil)))))),A).

- A = 3

It is assumed that a datatype int, together with operators +,*,- of type int -> int, constants 0,1,2,...:int and equational constraints are defined elsewhere.

The predicate pred[length] is not specified by the user, but is built up automatically from the function definition for length, whereas (for no good reason other that to illustrate the difference) length of is a predicate with the same meaning hand coded by the user^{1} The query

 ?-length_of((cons (2,(cons (4,(cons (5,nil)))))),A+2).
yields A=1 by unification of ((cons (2,(cons (4,(cons (5,nil)))))),A+2) with (Z,length Z) which

is carried out in the appropriate category by taking the pullback of the two corresponding arrows, as described below. The predicate list even is also not defined directly by the user, only even.

In this paper we show how to define a category with arrows corresponding to resolution proofs with a generalized notion of unification with constraints such as:

                 length of((cons (2,(cons (4,(cons (5,nil)))))),A+2) ⇝^{A=1} □.

and with new proof steps that incorporate data type information

         list X (cons(a,t))⇝ X(a),list X (cons(a,t))

which are treated as dynamic updates of the basic Horn clause interpreter.

What we will not discuss here are proof strategies: algorithms for searching the category of proofs or the category of non-deterministic resolutions defined in the paper, or for computing pullbacks. This is of course extremely relevant, and quite a harder matter to resolve than the subject matter of this paper. What we show here is that in principle a correct interpreter can be dynamically generated from constraint data expressed in a modular discipline that is both a specification at top level, and correctly executable code.

1The point of providing an automatically generated predicate pred[length] is that the function length could be made private to the data type. This is in keeping with the view that adding datatypes should not necessarily mean turning logic programming into a functional programming language.

Related Work: Module proposals, and data type definitions for logic programming have appeared since the early 1980’s, notably [12, 2]. Our contribution here is to introduce a new technique for lifting certain constraints on data to predicates on that data and proofs between them, in the general framework of a categorically defined constraint domain.

Categorical approaches to logic programming features appeared in the mid 1980’s in Rydeheard and Burstall’s categorical treatment of unification [24] based on ideas of Burstall and Goguen. Since then research using categories to analyze or generalize different facets of declarative programming has been carried out by Corradini, Asperti and Montanari [1, 5, 4], Panangaden, Scott, Seely, Saraswat, [19], Power and Kinoshita [21] Diaconescu [8], Pym [22], Orejas, Ehrig and Pino [18], and Finkelstein, Freyd and Lipton [9, 10].

2 Logic Programming Categories

In the remainder of this paper, we build on the basic categorical framework defined in [9], based on standard approaches to categorical logic, e.g. [16, 11]. It is briefly sketched here.

Categorical Logic: In a nutshell, the categorical representation of the syntax of logic programs is as follows: an FP category (category with finite products) ℂ is taken as a generalization of to the Herbrand Universe. It serves as a generalized program signature as well: it supplies the basic sorts (objects), function symbols of sort (σ, ρ) (arrows σ ^{f} ρ), and constants of sort ρ (arrows of the form 1 ^{a} ρ, where 1 is the terminal object). Since it is closed under allowed compositions, it supplies the terms as well. Often, only a distinguished class of arrows (closed under composition) interest us as program terms, and are so identified. Predicates are subobjects of their sort, with instances given by pulling back along term arrows. In order to make the right kind of subobjects available, special categories ℂ [X_{1}, …, X_{n}] or ℂ[σ] of generic predicates will be built on top of ℂ subject to different constraints depending on the extension we are trying to formalize. In these categories, predicates are functors generated by spans emanating from their sort.

We can recover traditional logic programming over the Herbrand universe in this framework, if we pick ℂ to be the so-called the Lawvere Algebraic Theory for a one-sorted signature with at least one constant (considered in e.g. [9]) and with no equations. Here, arrows correspond to (projections of vectors of) terms of the Herbrand Universe. We call this the Herbrand Category for the signature. The more general framework of arbitrary finite-product categories and generic predicate extensions allows us to build-in constraint information and data types into the syntax, as well as into the the structure of predicates. In such categories, unification of two arrows u and v with a common target (corresponding to two terms of the same sort which are standardized apart) amounts to finding a pair of substitutions (arrows) with a common source θ, ψ making a commuting square, i.e. such that ψv = θu.

Most general unifiers yield pullback diagrams, when they exist. Note that separating the domains of terms u and v is what standardizes them apart^{2}. In extensions of Horn logic, such as λ-prolog, queries and programs may share variables, which requires explicit sharing of domains. Unification then reduces to equalizing the arrows (see [10])

For basic concepts of category theory, we refer the reader to [11], and for the elements of indexed category theory, see [6]. We note that compositions of arrows are written in diagrammatic order: A ^{f} B composed with B ^{g} C is A ^{fg} C.

2If the ambient category is the Herbrand Category, the occurs-check will be automatically enforced.

2.1 Generic Predicates and Unordered Goals

A predicate symbol R of type σ may be modelled in a category with finite products by a monic arrow with target σ. Instantiation (and hence, substitution) by terms of sort σ can be modelled by pullbacks along the appropriate arrow:

[figure: R(t); R; α; t; σ]

Any distinguished family of monics can play the role of predicates in a logic program, but if they are to make sense in logic program syntax such a collection should be closed under pullbacks^{3} and they should not be chosen to conflict with the meaning of the logic program in which they will be used. Unlerss one wishes to constrain program predicates in advance (a question we will take up subsequently), the predicate A should not be true of any instance A(t) in the syntactic category, until information about the program is somehow incorporated into the categorical structure. In short: they should behave like second-order predicate variables. We thus seek a notion of generic or freely adjoined predicate.

Definition 1 (Generic Predicates) Let X be a subobject of some object b in a finite product category ℂ, and let D be a family of arrows in ℂ targeted at b. We say X is a generic subobject of b with respect to the maps D if

• For every arrow t in D the pullback t^{#}(X) exists.

• No such pullback is an isomorphism.

Definition 2 Let ℂ be an FP category and b⃗ = b_{1}, …, b_{n} a sequence of objects of ℂ. Then ℂ [X_{1}, …, X_{n}], the category obtained from ℂ by freely adjoining indeterminate subobjects of b⃗ is defined as follows:

objects: pairs ⟨A, S⟩ where A ∈ |ℂ| and S is a sequence S_{1}, …, S_{n} of finite sets S_{i} ⊂ Hom_{ℂ} (A, b_{i}),

arrows: are triples ⟨A, S⟩ ^{f} ⟨B, T ⟩ where A ^{f} B is an arrow in ℂand fT ⊂ S, that is to say, for every i, (1 ≤ i ≤ n) and every t ∈ T_{i}, ft_{i} ∈ S_{i}. The arrow f in ℂ is called the label of ⟨A, S⟩ ^{f} ⟨B, T ⟩. Composition of arrows is inherited from ℂ. Two arrows ⟨A, S⟩ ^{f} ⟨B, T ⟩ and ⟨A′, S′⟩ ^{f′} ⟨B′, T′⟩ are equal if they have the same domain and range and if f = f′ in ℂ.

Given an object ⟨A, S⟩ we will use the notation tS, where t is an arrow in ℂ with target A, to mean the sequence tS_{1}, …, tS_{n} where tS_{i} = {ts : s ∈ S_{i}}. Notice that an arrow in ℂ [X_{1}, …, X_{n}], may have an identity arrow in ℂ as a label, and not even be an isomorphism in ℂ [X_{1}, …, X_{n}]. We will be paying special attention to a certain class of such arrows.

Theorem 3 Let ℂ be a finite product category. The category ℂ [X_{1}, …, X_{n}] has

• a terminal object ⟨1,∅⟩, where ∅ is the sequence ∅, …, ∅ of length n,

• products: ⟨A, S⟩ × ⟨B, T ⟩ = ⟨A × B, π_{1}S ∪ π_{2}T ⟩ where A ^{π_{1}} A × B ^{π_{2}} B is a product in ℂ.

Furthermore, the functor ℂ ^{ι} ℂ [X_{1}, …, X_{n}] given by mapping objects A to ⟨A,∅⟩ and arrows A ^{f} B to ⟨A,∅⟩ ^{f} ⟨B,∅⟩, is a limit-preserving, full embedding.

3If the predicates are not stable under pullbacks of arrows designated as program terms, then certain instances may not even exist in the syntax, which is a rather unusual form of failure for a logic program query.

Limit preservation follows from the fact that ι has a left adjoint, namely the forgetful functor U taking objects ⟨A, S⟩ to A and arrows to their labels.

Lemma 4 Addition of indeterminate subobjects simultaneously, sequentially, or in permuted order results in isomorphic categories. More precisely:

1. ℂ [X_{1}, …, X_{n}] ≃ ℂ [X_{1}] ⋯ [X_{n}].

2. Let σ be a permutation of the first n positive integers. Then

ℂ [X_{1}, …, X_{n}] ≃ ℂ [X_{σ(1)}, …, X_{σ(n)}]

.

Proof. Straightforward. □

Definition 5 In ℂ [X_{1}, …, X_{n}] define the indeterminate subobjects X_{1}, …, X_{n} of sorts b_{1}, …, b_{n}

respectively, to be the subobjects ⟨b_{i}, J^{i}⟩ ^{id_{b_{i}}} ⟨b,∅⟩, where the J^{i} are the “basis vectors”

(J^{i})_{k} = \{ \begin{matrix}∅ & if & i ≠ k \\ \{id_{b_{i}}\} & o.w. \end{matrix}

Theorem 6 The indeterminate subobjects X_{i} of b_{i} are generic with respect to the maps (targeted at ⟨b_{i}, ∅⟩) in the image of ℂ ^{ι} ℂ [X_{1}, …, X_{n}].

Proof. The following diagram is a pullback for any arrow ⟨A,∅⟩ ^{t} ⟨b_{i},∅⟩:

[figure: ⟨A, tJ^{i}⟩; t; ⟨b_{i}, {id}⟩; ⟨A,∅⟩; id_{A}; t; ⟨b_{i},∅⟩; id_{b_{i}}]

so X(t) = ⟨A, tJ^{i}⟩ ^{id_{A}} ⟨A,∅⟩ exists for all appropriate t. This arrow cannot be an isomorphism in ℂ [X_{1}, …, X_{n}]: its inverse, which would have to be labelled with id_{A}, would have to satisfy id_{A}t ∈ ∅. □

Objects of the form X(t) = ⟨A, tJ^{i}⟩ will be called atomic predicates. If A is an object of ℂ, we say that the monic ⟨B, S⟩ ^{f} ⟨A,∅⟩ is a canonical (representative of a) subobject of ⟨A,∅⟩ if B is A and the monic f is id_{A}. Observe that every object ⟨A, S⟩ of ℂ [X_{1}, …, X_{n}] is a canonical subobject of “its sort” ⟨A,∅⟩. This allows us to define a natural indexed structure [6] for ℂ [X_{1}, …, X_{n}] over ℂ.

Definition 7 For each object A of ℂ, let ℂ_{A}[X_{1}, …, X_{n}] be the category whose objects are arrows in ℂ [X_{1}, …, X_{n}] of the form ⟨A, S⟩ ^{id_{A}} ⟨A,∅⟩, and with morphisms given by arrows between their sources labelled by the identity on A in ℂ. Then let p : ℂ ℂ𝔸𝕋 be the strict indexed category given by

• p(A) = ℂ_{A}[X_{1}, …, X_{n}]

• p(A ^{f} B) = f^{#} : ℂ_{B}[X_{1}, …, X_{n}] ℂ_{A}[X_{1}, …, X_{n}]

Notice that the pullback operation referred to by f^{#} maps ⟨B, S⟩ ^{id_{B}} ⟨B,∅⟩ to ⟨A, fS⟩ ^{id_{A}} ⟨A,∅⟩. Thus (fg)^{#} is precisely g^{#}f^{#} on the nose. Now we define a “canonical intersection” functor for the indexed category p:

Definition 8 Let ∩ : p × p p be defined by ⟨A, S⟩ ∩_{A} ⟨A, T ⟩ = ⟨A, S ∪ T ⟩.

By the remarks immediately preceding the definition, it is immediate that ∩ commutes with pullback, i.e. is a natural transformation.

The following theorems make precise the fact that ℂ [X_{1}, …, X_{n}] is called the category obtained by freely adjoining the indeterminate subobjects of the sorts b_{1}, …, b_{n}.

Lemma 9 Every object ⟨A, S⟩ is representable as (i.e. equal on the nose to) the canonical intersection

⋂{t^{#}(X_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n}

where the pullbacks are canonical: t^{#}(X_{i}) = ⟨A, tJ^{i}⟩ = ⟨A, ∅ ⋯ ∅ \underbrace{\{t\}}_{i} ∅ ⋯ ∅⟩.

Proof. Immediate: Since S = ⋃{{t} : t ∈ S}, the indicated canonical intersection is precisely ⟨A, S⟩. □

Theorem 10 (Universal Mapping Property) Suppose F : ℂ ⟶ 𝔻 is a limit preserving functor from the finite-product category ℂ to the finitely complete category 𝔻, and that F (b_{i}) = d_{i} for 1 ≤ i ≤ n. Furthermore, let B_{1}, …, B_{n} be a sequence of subobjects of d_{1}, …, d_{n} respectively, in 𝔻. Then there is a limit-preserving functor FB⃗ : ℂ [X_{1}, …, X_{n}] ⟶ 𝔻, unique up to isomorphism, such that the following diagram commutes.

ℂ[X_{1}, …, X_{n}]
[figure: ι; FB⃗]
ℂ  \overline{_{F}} 𝔻

FB⃗ is called the evaluation functor induced by the B_{i}.

Proof. Define FB⃗ on objects by FB⃗(⟨A, S⟩) = \underleftarrow{lim}\{F (t)^{#}(B_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n\}. The univer-

sal mapping property of limits gives us the action on arrows: if ⟨A, S⟩ ^{f} ⟨A′, S′⟩ is an arrow in ℂ [X_{1}, …, X_{n}] then FB⃗(⟨A, S⟩), the limit of the family of monics {F (t)^{#}(B_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n} tar-

geted at F A, is also, by composing with F (A ^{f} B) and using properties of pullbacks and of arrows in ℂ [X_{1}, …, X_{n}], a cone over the family of monics {F (t)^{#}(B_{i}) : t ∈ S′_{i}, 1 ≤ i ≤ n}. There is therefore a unique induced arrow F ⟨A, S⟩ ^{θ} F ⟨A′, S′⟩ which is the value of F (⟨A, S⟩ ^{f} ⟨A′, S′⟩). The details, and those of the proof of limit preservation, are left to the perseverant reader. □

We are interested in a category 𝔻 with richer structure, in which case we are able to sharpen this result a bit.

Corollary 11 Assume the category 𝔻 in the preceding theorem is Set^{ℂ^{o}} and that F is the Yoneda embedding. Choose the sequence of subobjects B_{i} of F b_{i} = Hom_{ℂ} ( , b_{i}) to be canonical, that is to say, pointwise subsets of F b_{i}, and take limits in Set^{ℂ^{o}} to be given pointwise (not just up to isomorphism, but on the nose). Then the evaluation functor FB⃗ of the preceding theorem is unique.

2.1.1 Unordered Goals

The most elementary notion of query, or of state in a logic program, is that of a conjunction of atoms

X_{i_{1}}(t_{1}), …, X_{i_{n}}(t_{n})  (1)

where the X_{i_{j}} are program predicate symbols. We call these basic goals.

A first approximation to syntactic goals is already present in the category ℂ [X_{1}, …, X_{n}] whose objects are effectively unordered goals. By the representation lemma (9) above, every object ⟨A, S⟩ in ℂ [X_{1}, …, X_{n}] is an intersection

⋂{t^{#}(X_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n}.  (2)

and can be thought of as a non-deterministic image of the corresponding ordered goal (1) above.

These intersections are free in the sense that one can recover all components t^{#}(X_{i}) from them, i.e. by reading off the arrows in the S_{i}, and in the sense of theorem 10. Since the S_{i} are sets, they cannot capture order or repititions of atoms within goals. An ordered counterpart will be defined below.

Definition 12 Let ℂ be a finite product category, and X_{1}, …, X_{n} a sequence of generic predicates over ℂ of sorts b_{1}, …, b_{n}. An interpretation is an evaluation functor extending the Yoneda embedding, assigning to each X_{i} some canonical subobject B_{i} of Hom_{ℂ} ( , b_{i}) as in corollary 11.

In other words, an interpretation is a functor

[[ ]] : ℂ [X_{1}, …, X_{n}] ⟶ Set^{ℂ^{o}}

• agreeing with the Yoneda embedding on ℂ, and

• mapping ⟨A, S⟩ to ⋂{( [[t]])^{#}(B_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n},

where [[t]] means the Yoneda image of t.

It is easy to check that interpretations form a complete lattice under the pointwise order.

2.2 Two Proof-theoretic Categories

Fix a sequence of sorts σ = σ_{1}, …, σ_{n}, σ_{i} ∈ |ℂ | and a family X_{1}, …, X_{n} of generic predicates X_{1}, …, X_{n} with X_{i} of sort σ_{i}, as in the construction of the categories in the preceding section. We will refer to objects X_{i}(t_{i}) = t_{i}J^{i} of sort A, where A _{t} σ_{i} is an arrow in ℂ, as atomic goals or predicates (of sort A), objects ⟨A, S⟩ of ℂ [X_{1}, …, X_{n}] as unordered (or non-deterministic) goals (of sort A), and sequences X_{i_{1}}(t_{1}), …, X_{i_{m}}(t_{m}), where each atomic predicate X_{i_{j}}(t_{j}) is of sort A, as ordered goals of sort A.

Note that there is a “forgetful” function β which takes ordered goals to the underlying unordered ones:

β(X_{i_{1}}(t_{1}), …, X_{i_{m}}(t_{m})) = ⟨A, S⟩,  (3)

where S_{k} = {t_{j} : i_{j} = k} that is to say, the set of all terms occurring as arguments to the kth generic predicate, wherever it occurs (0 or more times) in X_{i_{1}}(t_{1}), …, X_{i_{m}}(t_{m}). Thus ⟨A, S⟩ = ⋂{t^{#}(X_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n} as discussed in the previous section.

It will be convenient below to describe the following operation on ordered and unordered goals, both given the same name del_{t}^{k}, which removes one occurrence (the first one, in the ordered case) of the atomic goal X_{k}(t) if it exists, and returns the original goal unchanged, otherwise. More formally, in the unordered case: del_{t}^{k}⟨A, S⟩ = ⟨A, T ⟩ where T_{i} = S_{i} if i ≠ k and T_{k} = S_{k} \ {t}.

Definition 13 A Horn Program over ℂ (in the predicates X_{1}, …, X_{n}) is a finite set of triples ⟨A, G, X(t)⟩ where G is an ordered goal, and X(t) an atomic goal, both of sort A. An unordered Horn program is a similar set of triples ⟨A, G, X(t)⟩, but where G is unordered. The triples are called (ordered or unordered) clauses, and may be written G ⇒ X(t) when the sort is understood from context.

Note that the “forgetful” function β in (3) extends naturally to a map from ordered clauses to unordered ones.

Definition 14 Let P be a Horn program. A P-SLD proof step between ordered goals G_{1} and G_{2}, of sorts A_{1} and A_{2}, respectively, with substitution θ, and program clause c = ⟨A, H, X_{k}(u)⟩, denoted

G_{1} ⇝^{θ,c} G_{2}

is a 4-ary relation (relating G_{1}, θ, c, G_{2}) defined by:

• A_{2} ^{θ} A_{1} is an arrow in ℂ, and

• there is an arrow A_{1} _{t} σ_{k} in ℂ, such that X_{k}(t) is an atomic subgoal of G_{1}, that is to say, G_{1} = G, X_{k}(t), G′,

• there is an arrow A_{2}rT o^{ψ}A such that θt = ψu and

• G_{2} = θG, ψH, θG′.

If ⟨A_{1}, S⟩, ⟨A_{2}, T ⟩ are unordered goals, an sld-step ⟨A_{1}, S⟩ ⇝^{θ,c} ⟨A_{2}, T ⟩ between them exists when a clause c and unifying arrows θ and ψ exist, as above, and T = θ(del_{t}^{k}S) ∩ ψH. In both the ordered and unordered cases, the arrow θ is called the substitution of the SLD step, and c its clause.

We define an SLD-sequence between goals, G⇝ ⋯^{θ} ⇝G′ to be the ternary relation that obtains when there is a sequence of goals G = G_{0}, …, G_{n} = G′ and SLD-steps between each G_{i−1} and G_{i} with substitution θ_{i}, and θ is the composition θ_{n} ⋯ θ_{1}. The “reflexive case”n = 0 and θ = id is allowed.

Definition 15 The category ℂP^{SLD} of unordered SLD proofs over program P has the objects of

ℂ [X_{1}, …, X_{n}] as its objects, and arrows ⟨A, S⟩ ^{θ} ⟨B, T ⟩ where ⟨B, T ⟩⇝ ⋯^{θ} ⇝⟨A, S⟩ is an

SLD sequence. We call A ^{θ} B in ℂ the label of this arrow of ℂP^{SLD}.

2.2.1 The Operational Category ℂ_{P}

We now modify the generic predicate construction ℂ [X_{1}, …, X_{n}] to produce a category of predicates ℂ_{P}which are generic modulo the clauses in program P. ℂ_{P} is a categorical (and constraint-sensitive) counterpart to the operational C-semantics of Levi et. al. [15], in the sense that objects are goals modulo operational equivalence, and arrows are open substitutions between them. Later we will study how datatype information acts on both ℂ_{P} and ℂP^{SLD} to produce dynamically updated predicates, operational semantics and proofs.

Definition 16 Let A be an object in ℂ, and T a monotone operator on sets of arrows with a common source in ℂ. Then a family S of arrows with source A is said to be closed under T if T (S) = S. S is T -generated by a family of arrows emanating from A if S = T (U). We will also write ⟨U⟩ for T (U) when the closure operator is understood from context.

Definition 17 Let ℂ be a finite-product category, and P a Horn clause program over ℂ [X_{1}, …, X_{n}]. The category ℂ_{P} is given by the following data:

objects: Pairs (A, S) where A is an object of ℂ, and S is a sequence S_{1}, …, S_{n}, where each S_{i} is a set of arrows from A to σ_{i}, closed with respect to the following clausal closure condition: For each clause of sort α in P

X_{i_{1}}(t_{1}), …, X_{i_{n}}(t_{n}) ⇒ X(t)  (4)

where X, X_{i_{k}} are generic predicates of sort σ_{j}, σ_{i_{k}}, α ^{t} σ and α ^{t_{k}} σ_{i_{k}} arrows in ℂ, and for each arrow A ^{φ} α satisfying

φt_{1} ∈ S_{i_{1}}, …, φt_{n} ∈ S_{i_{n}}  (5)

we must have φt ∈ S_{j}.

arrows are triples (A, S) ^{f} (B, V) such that A ^{f} B (the label) is an arrow in ℂ, and fV ⊂ S. Composition is defined by composing labels.

If we let T_{P}^{A} be the operator on sets of arrows with a common source A given by

T_{P}^{A}(S) = ⋃_{c∈P}{φt : A ^{φ} α and φt_{1} …, φt_{n} ∈ S}

then the requirement on S in the preceding definition is equivalent to being T_{P}^{A}-generated.

Lemma 18 There is a faithful functor ι_{P} : ℂ [X_{1}, …, X_{n}] ℂ_{P} given by (A, U) ↦ (A, ⟨U⟩) on objects, and which preserves labels of arrows.

Proof. Since the closure operator T_{P}^{A} is monotone, ι_{P} maps arrows to arrows. Fidelity and functoriality is immediate. □

2.3 Semantics

Let P be a program, G^{P}the collection of ordered goals over P, and [[ ]] an interpretation into Set^{ℂ^{o}} as in definition (12), and β the forgetful map from ordered to unordered goals. Then observe that β [[ ]] is a function G^{P} ⟶ Set^{ℂ^{o}}. We sometimes overload the symbol [[ ]] to denote β [[ ]], since context will always make clear what is meant. We call the composition βι_{P} : G^{P} ⟶ ℂ_{P} the representation of goals in the category ℂ_{P}.

Note that by corollary (11), the value of [[ ]] on goals is completely determined by its value on generic predicates.

We now give a quick sketch of some results on semantics from [9, 10]. We give a categorical analogue of the Kowalski-van Emden bottom-up semantics. Proofs can be founded in the cited references, and are, for the most part, omitted.

Definition 19 An interpretation [[ ]] is a model of program P if for every clause tl_{cl} ⇒ hd_{cl} we have [[tl]] ⊂ [[hd]]. A goal G of sort α is said to be true in the interpretation if the image [[β(G) ]] ∈ Set^{ℂ^{o}} of the monic

β(G) ^{id_{α}} (α, ∅)

is an isomorphism.

In the following discussion we will use the notation cl ∈ P to refer to the fact that cl is an ordered clause in the program P. We also refer to the empty goal of sort σ by □_{σ}. The image of this goal in ℂ [X_{1}, …, X_{n}] under β is (σ, ∅), which is the entire subobject (σ, ∅) = (σ, ∅). Since functors preserve identity arrows, it must be mapped by any interpretation to the identity ℂ ( , σ) = ℂ ( , σ).

Lemma 20 (Soundness) Let [[ ]] be a model of program P, and G_{1} and G_{2} goals of sorts α_{1}, α_{2}

respectively, and G_{1}⇝ ⋯^{θ,c} ⇝G_{2} a resolution proof with answer substitution α_{2} ^{θ} α_{1}. Then [[G_{2} ]] ⊂ [[θG_{1} ]]. In particular, if G_{2} is □_{α_{2}} then θG_{1} is true in the model.

We now define a categorical analogue of the T_{P} operator of Kowalski and Van Emden, an operator E_{P} on the lattice of interpretations.

Definition 21 Let [[ ]] be an interpretation and X_{1}, …, X_{n} the sequence of generic predicates in program P. Then

E_{P} ( [[ ]])(X_{i}) = ⋃_{tl⇒X_{i}(t)∈P} Im_{[[t ]]} ( [[tl_{cl} ]])

where, for each t occurring in the head of a clause in P of the form tl ⇒ X_{i}(t), Im_{[[t ]]} denotes the image along the arrow [[t]] in Set^{ℂ^{o}}.

In [9, 10] it is shown that E_{P} is a continuous operator on the lattice of interpretations, with a least fixed point [[ ]]^{∗} (called the Herbrand interpretation for P).

Lemma 22 An interpretation [[ ]] is a model of program P if and only if it is a pre-fixed point of E_{P} (that is to say, E_{P} ( [[ ]]) ⊆ [[ ]]) and hence, if and only if [[ ]]^{∗} ⊆ [[ ]].

The following is established in [9, 10]

Theorem 23 (Completeness) If P is a program, [[ ]]^{∗} its Herbrand interpretation and G a goal,

[[G]]^{∗} is an isomorphism if and only if there is an SLD proof G⇝ ⋯^{id} ⇝□

We now establish some properties of the category ℂ_{P}. Since it is a finite-product category, arrows in ℂ_{P} are not, strictly speaking, SLD proof steps (in reverse), but a bit more. Arrows in ℂ_{P} correspond to extended resolution steps that include weakening of goals and instantiation of goals, as well as products of basic SLD sequences that can be thought of as parallel resolutions of multiple goals. But the present category suffices for our purposes, since the only global proofs □_{α} ^{θ} βι_{P}(G)

correspond to real SLD proofs G⇝ ⋯^{θ} ⇝□_{α}.

Theorem 24 (Soundness of β ∘ ι_{P}) Let G_{1}⇝ ⋯^{θ} ⇝G_{2} be an SLD sequence, and let (α_{1}, ⟨U_{1}⟩) and (α_{2}, ⟨U_{2}⟩) be the images in ℂ_{P} of G_{1} and G_{2} under β ∘ ι_{P}. Then G_{2} ^{θ} G_{1} is an arrow in ℂ_{P}.

Proof. Observe that the closure condition (5) of definition (17) guarantees that for each clause tl ⇒ hd of P, the arrow (α, ⟨S_{tl}⟩) ^{id_{α}} (α, ⟨S_{hd}⟩) is in ℂ_{P}, for βι_{P}(hd) = (α, ⟨S_{hd}⟩) and βι_{P}(tl) = (α, ⟨S_{tl}⟩), the requirement for arrows in ℂ_{P} being S_{tl} ⊆ S_{hd} which is precisely the closure condition (5). This proves the claim for the trivial one-step resolution from the head of a clause to its tail. Using the fact that for any arrow θ targeted at α (α, θ⟨S_{tl}⟩) ^{id_{α}} (α, θ⟨S_{hd}⟩) is also in ℂ_{P}, and that

G_{1}⇝ ⋯^{θ} ⇝G_{2} implies θG_{1}⇝ ⋯^{id} ⇝G_{2}, it is straightforward to show that any resolution sequence with answer substitution θ maps to an arrow with label θ in the opposite direction. □

Theorem 25 (Completeness of β ∘ ι_{P}) If □_{α} ^{θ} βι_{P}G is an arrow in ℂ_{P}, then there is an

SLD proof G⇝ ⋯^{θ} ⇝□_{α}.

Proof. The empty goal of sort α is represented by the object (α, ⟨∅⟩) in ℂ_{P}. Suppose βι_{P}G = (γ, ⟨U⟩). That is to say G is of the form X_{i_{1}}(t_{1}), …, X_{i_{n}}(t_{n}) and U is

⋂{t^{#}(X_{i}) : t ∈ U_{i}, 1 ≤ i ≤ n}.  (6)

Then if □_{α} ^{θ} βι_{P}G is an arrow in ℂ_{P}, θ⟨U⟩ ⊆ ⟨∅⟩, that is to say, by the remarks about T_{P} following definition (17), every X_{i_{j}}(t_{j}) is true in the Herbrand interpretation [[ ]]^{∗} of P for (1 ≤ j ≤ n). By completeness for [[ ]]^{∗} (theorem 23) there is an SLD proof of θG from P, hence a proof of G with computed answer substitution θ. □

3 The Categories ℂ[σ], ℂ_{P}[σ] and ℂP^{SLD}[σ]

Next, we generalize definition 2 so that the resultant construction will allow lifting of functorial datatypes and certain diagrams from the base category to the category of predicates. For the duration of this section ℂ is an FP category, 𝔻 is a complete category, 𝕁 is a category, and D is a collection of product diagrams in 𝕁, which we will call distinguished products, or D-products.

Definition 26 (D-Product Preservation) We will say that the functor H : J 𝔹 preserves D-products if H sends each D-product to a product diagram in 𝔹.

For the rest of this paper σ : 𝕁 ℂ will be a functor that preserves D-products and σ_{i} will denote the ℂ-object σ(i).

Definition 27 (D-Closure) Let A ∈ |ℂ |, and D be a set of product diagrams in ℂ. A subfunctor S of ℂ (A, σ(−)) is D-closed if it preserves D-products. In other words, for every D-product diagram for i_{1} ×…×i_{n}, if there are arrows f_{k} ∈ S(i_{k}) for each k = 1, …, n, then ⟨f_{1}, …, f_{n}⟩ ∈ S(i_{1} ×…×i_{n}).

In particular, if 1_{𝕁} ∈ D, then σ_{1_{𝕁}} = 1_{ℂ} and S(1_{𝕁}) = {!_{A}}.

Definition 28 (D-Generating Sets) Let Y be a collection of arrows emanating from A, each with target in the range of σ. Y is said to D-generate S if S is the smallest D-closed subfunctor of ℂ (A, σ(−)) containing all the arrows of Y. In that case we write ≪ Y ≫ for S, and call it the D-closure of Y.

Definition 29 Let ℂ[σ] be defined as follows.

objects: pairs ⟨A, S⟩ where A ∈ |ℂ | and S is a D-closed subfunctor of ℂ (A, σ(−)).

arrows: are triples ⟨A, S⟩ ^{h} ⟨B, T ⟩ where A ^{h} B is an arrow in ℂ and hT ⊂ S, i.e. for any j ∈ |𝕁| and f ∈ T (j), hf ∈ S(j). Again, we define a label as before, and compostion is inherited from ℂ .

Observe that the functors S are no longer finitely generated.

A routine verification shows that if 𝕁 is the discrete category on the set {1, …, n} and D = ∅ then ℂ[σ] = ℂ [X_{1}, …, X_{n}]. Hence Definition 2 is a special case of Definition 29.

Proposition 30 If ℂ is an FP category [resp. cartesian] then ℂ[σ] is an FP category [resp. cartesian] and the functor ℂ ^{ι} ℂ[σ] given by mapping objects A to ⟨A, ≪ ∅ ≫⟩, and arrows A ^{f} B to ⟨A, ≪ ∅ ≫⟩ ^{f} ⟨B, ≪ ∅ ≫⟩, is a full and faithful limit-preserving embedding.

The proof is straightforward, but lengthy. The reader is referred to [17] for details.

Definition 31 Let ℂ(σ) stand for the full subcategory of ℂ[σ] whose objects are

|ι(ℂ)| ⋃{⟨σ_{j}, ≪ Id_{σ_{j}} ≫⟩|j ∈ |𝕁|}.

Also, let X : 𝕁 ℂ(σ) be the functor taking objects j ∈ |𝕁| to the pair ⟨σ_{j}, ≪ Id_{σ_{j}} ≫⟩ and

arrows i ^{h} j to ⟨σ_{i}, ≪ Id_{σ_{i}} ≫⟩ ^{σ_{h}} ⟨σ_{j}, ≪ Id_{σ_{j}} ≫⟩.

Finally, let m : X ι ∘ σ be the natural transformation defined by m_{j} ≡ X_{j} ^{id_{σ_{j}}} ι(σ_{j}) where j ∈ |𝕁|.

It is straightforward to show the composite functor 𝕁 ^{X} ℂ(σ) ^{⊂} ℂ[σ] preserves D-products.

The monic m_{j} (and by abuse of language, its source X_{j}) will be called the generic predicate of sort σ_{j} since the family m exhibits similar characteristics to the generic predicates of Definition 1. In particular, for every j ∈ |𝕁|, t ∈ ℂ (A, σ_{j}) the diagram

[figure: ⟨A, ≪ t ≫⟩; t; X_{j}; ⟨A, ≪ ∅ ≫⟩; Id_{A}; t; ισ_{j}; ∩; m_{j}]

is a pullback in ℂ[σ]. However, it may be the case that some of these pullbacks are indeed isomorphisms: the constraint information contained in σ may make some generic predicates true.

For example, suppose 1_{𝕁} is in D. Then it follows that X_{1_{𝕁}} = σ_{1_{𝕁}} = 1_{ℂ} so that X_{1_{𝕁}} ^{m_{1_{𝕁}}} σ_{1_{𝕁}} is iso. The “genericity” of the family m is made precise in the following theorem.

Theorem 32 (Universal Mapping Property II) Let 𝔻 be a complete category and suppose that F : ℂ(σ) 𝔻 is a functor such that

• F ∘ ι : ℂ 𝔻 is a cartesian representation;

• F ∘X : 𝕁 𝔻 preserves D-products; and

• F (m) : F ∘X F ∘ ι(σ) is a monic natural transformation.

Then there exists a cartesian functor F̄ : ℂ[σ] 𝔻 unique up to isomorphism making the triangle

ℂ[σ]

[figure: F̄]

ℂ(σ)  \overline{F} 𝔻

commute.

Proof(sketch). For A ^{t} σ_{j}, let F̃(t) be the pullback of X_{j} ^{F m_{j}} F ισ_{j} along F ι(A) _{F (t)} F ισ_{j}.

Define F̄⟨A, S⟩ on objects by F̄⟨A, S⟩ = ⋂{F̃(t)|t ∈ S(j), j ∈ |𝕁|}. F̄ on arrows is just a consequence of the limit definition of F̄ on objects. It follows that F̄ has the stated properties. We refer the reader to [17] for the details. □

Corollary 33 Assume the category 𝔻 in Theorem 32 is Set^{ℂ^{o}} and that F ∘ι is the Yoneda embedding. Also, for each i ∈ |𝕁| take F (X_{i}) ^{F (m_{i})} F (σ_{i}) to be a pointwise subset of F (σ_{i}), and take limits in Set^{ℂ^{o}} to be given pointwise. Then the functor F̄ of Theorem 32 is unique. In this case we call the functor a σ-interpretation by analogy with definition 12, and write it [[ ]].

The category ℂ_{P}[σ]: We have given two constructions, one yielding a category ℂ_{P} of substitutions corresponding to proofs with respect to program P, and one yielding arrows that serve as proof steps for data information encapsulated in the index category 𝕁 and the functor σ. Finally we define a category of σ-proofs ℂ_{P}[σ] by merging the two constructions. The objects are pairs (A, S), A in |ℂ | and S a subfunctor of ℂ (A, σ(−)) closed under both the conditions 5 of definition 17 (clausal closure) and that of definition 27 (D-closure). Arrows are induced by labels from ℂ as before.

The category ℂP^{SLD}[σ]: Given the data ℂ, 𝕁 and σ, we define an (unordered) σ-goal to be an object of ℂ[σ], a σ-clause to be a triple ⟨A, G, X(t)⟩, where X(t) is an atomic σ-goal (a pullback of a generic σ-predicate) and G a σ-goal, both of sort A ∈ |ℂ |, and a σ-program P a set of σ-clauses. We can construct a category of generalized resolution proofs directly from ℂ_{P}[σ] and P by taking, as objects, the objects of ℂ[σ], and as arrows, triples

⟨A, S⟩ ^{h} ⟨B, T ⟩

where ⟨A, ⟨S⟩_{D}⟩ ^{h} ⟨B, ⟨T ⟩_{D}⟩ is an arrow in ℂ_{P}[σ], (⟨S⟩_{D} being the D-closure of S), and composition is given by composition of labels from ℂ. In other words, ℂP^{SLD}[σ] is the object part of the comma category (κ, κ) induced by the functor κ : ℂ[σ] ℂ_{P}[σ] which maps objects ⟨A, S⟩ to ⟨A, ⟨S⟩_{D}⟩ and labels to themselves. In this category, arrows correspond to SLD-resolutions induced by program P, weakening, and proof steps induced by the datatype information encoded in σ. We then have soundness and completeness in the following sense

Theorem 34 Let P be a σ-program and G be a σ-goal. [[G]] is true for every σ-interpretation [[ ]]

that is a model of P if and only if there is an arrow □_{A} ^{id_{A}} G in ℂP^{SLD}[σ].

Proof[. sketch We sketch the completeness half of the theorem. Soundness is a straightforward but lengthy induction on the stages of the closure conditions defining objects in ℂP^{SLD}[σ].

Let [[ ]]^{s}ℂ[σ] Set^{ℂ^{o}} be defined by

[[(A, S) ]]^{s}(B) = {B ^{θ} A ∈ ℂ |□_{B} ^{θ} (A, S) ∈ ℂP^{SLD}[σ]}

where □_{B} is the object ⟨B, ≪ ∅ ≫⟩, and on arrows [[(A, S) ]]^{s}(B ^{f} B′) = ℂ ( , f). Then [[ ]]^{s} ∘ ι is the Yoneda embedding. [[ ]]^{s} is also a model of the program P. If G ⇒ X(t) is a clause of sort A then G ^{id_{A}} X(t) is an arrow in ℂP^{SLD}[σ], hence if □_{B} ^{θ} G is in ℂ_{P}[σ], θ is a label in [[X(t) ]]^{s}(B), so [[G]]^{s}(B) ⊆ [[X(t) ]]^{s}(B). Let G be a goal of sort A, i. e. an object (A, S) of ℂ[σ]. If [[G]] is true for every σ-interpretation [[ ]] that is a model of P, then [[G]]^{s} = ℂ ( , A), s, in particular

A = A ∈ [[G]]^{s}(A) and □_{A} ^{id_{A}} is in ℂP^{SLD}[σ].

□

4 Lifting Data Types to Predicates and Proofs

In this section we give several examples of the use of the machinery developed in preceding sections to incorprate datatype definitions into logic programs.

We take the following syntax for a datatype declaration.

  datatype 'a foo = c0|c1 ... |k1 of E 1('a)| ... |kn of E n('a)

with 'a possibly a sequence of variables, and where each E_{i}('a) is a type term, e.g. 'a * 'a list, and ki the appropriate constructor (e.g. cons).

The category ℂ: We assume a finite product category ℂ of data has been specified with objects corresponding to all required sorts together with an endofunctor foo: ℂ ℂ and endofunctors E_{1}, …, E_{n} induced by the type terms E_{i} in the datatype declaration (e.g. λX.X × list (X)) such that:

1. For each constant c_{i} in the datatype declaration there is a natural transformation λX.1 ^{(c_{i})} id.

2. For each constructor k_{i} there is a natural transformation k_{i} from E_{i} to foo

3. The object D(α) = 1 + … + 1 + E_{1}(α) + … E_{n}(α) exists (as a coproduct) in ℂ, for every object α of ℂ.

4. The arrow

D(foo α) ^{[c_{0}···c_{m} k_{1}···k_{n}]_{foo α}} foo α

is an initial algebra in ℂfor every object α.

The techniques for building the appropriate category ℂ are well known, and discussed in the literature, so we will not dwell upon this question here. The reader should consult e.g. [20, 13, 14, 23, 3].

Definition 35 (The Index category 𝕁) Let S = {γ_{1}, …, γ_{n}} be the multi-set of sorts of predicates in the program (some sorts may be repeated) and let ℕ be the preorder on the set {1, …, n} such that there is precisely one arrow of each type, i.e. all objects of ℕ are isomorphic. 𝕁 will be the smallest subcategory of ℂ × ℕ subject to the following conditions:

1. (1_{ℂ}, l), (γ_{l}, l) ∈ |𝕁| for all l = 1, …, n;

2. for each (α, l) ∈ |𝕁| and l′ = 1, …, n, we have

!_{(α,l)} ∈ 𝕁((α, l), (1_{ℂ}, l′));

3. for each (h, f) ∈ 𝕁((α, l), (β, l′)) , the following diagrams are included in 𝕁;

(foo(α), l) \overline{\begin{matrix}(foo(h), f) \\  \end{matrix}}(foo(β), l′)  (7)

4. for each constant ci in the declaration, (α, l) ∈ |𝕁|, and l′ = 1, …, n_{j},

(ci, l′ ⇒ l) ∈ 𝕁((1_{ℂ}, l′), (foo(α), l)),

where l′ ⇒ l is the unique arrow in ℕ(l′, l);

5. for each constructor kj in the datatype declaration and object (α, l) ∈ |𝕁|, all product diagrams

(Ej(α), l) ^{π_{k}} (Ej^{(k)}(α), l)  (1 ≤ k ≤ n_{j})  (8)

are included in 𝕁.

Given a 𝕁-span

[figure: f_{1}; f_{n_{j}}]_{(Ej^{(1)}(α), l)  …  (Ej^{(n_{j})}(α), l)}^{(β, l′)}  (9)

it must be the case that

⟨f_{1}, …, f_{n_{J}} ⟩ ∈ 𝕁((β, l′), (Ej(α), l)).

The special products in D are precisely:

1. the terminators (1_{ℂ}, l); and

2. the products of Diagram 8.

Let σ : 𝕁 ℂ be the projection functor onto the first coordinate.

The construction implements the appropriate extension of SLD resolution in the following sense.

Theorem 36 Given the data 𝕁 ^{σ} ℂ described above, the category ℂ_{P}[σ] contains all instances of the following arrows, for γ ∈ S and each constructor k_{i}:

• X_{E_{i}(γ)} ^{(k_{i})_{γ}} foo(X_{γ}) (where k_{i} is a label from ℂ)

• X_{E_{i}(γ)}(⟨t_{1}, …, t_{n}⟩) ^{id_{γ}} foo X_{γ}(k_{i}(t_{1}, …, t_{n}))

• All SLD proofs over the Horn Clauses in P.

Observe that the predicate foo(X_{γ}) means X_{fooγ}, which in the category ℂ_{P}[σ] is (fooγ, ≪ id_{fooγ} ≫). It is easily shown foo extends to an endofunctor on ℂ_{P}[σ] (The case where foo is a monad is studied in [17]).

In the case of e.g. the list datatype, the arrow X_{E_{1}(γ)} ^{k_{1}} foo X_{γ} becomes

X_{γ×list(γ)} ^{cons} list(X_{γ}) and X_{E_{i}(γ)}(⟨t_{1}, …, t_{n}⟩) ^{id_{γ}} foo(X_{γ})(k_{i}(t_{1}, …, t_{n})) becomes

X_{γ×list(γ)}(⟨t_{1}, t_{2}⟩) ^{cons} list(X_{γ})(cons(t1, t2)) which corresponds to the the proof rule

list(X_{γ})(cons(t1, t2)) ⇝^{id} X_{γ}(t1), list(X_{γ})(t_{2})

4.1 Encapsulation

Finally we show how to lift a datatype definition with member functions

datatype 'a foo = c0|c1 ... |k1 of E 1('a)| ... |kn of
  E n('a)
begin
  fun f1 ...
  ...
end

where the functions between the begin...end are arrows α ^{f} ρ in the original term category ℂ.

All we need to change is the definition of 𝕁, which now must be a disjoint union of the 𝕁_{γ} and the

diagrams α×α ^{id_{α}×f} α×ρ. The generic predicate m_{j} ≡ X_{j} _{Id_{σ_{j}}} (α×ρ ≪ id_{α×ρ} ≫) resulting from this extra component of 𝕁 is called pred[f] in the program syntax. It will automatically satisfy the condition that pred[f](X,f(X)) is an isomorphism in the categories ℂ_{P}[σ] and ℂP^{SLD}[σ]. That is to say, the construction “hard-wires” the graph of the function f into the binary relation pred[f]. This makes it possible for an implementation to supply the predicate without supplying the function, which would remain hidden. When interpreted in any model pred[f](X,f(X)) will be true, and in any resolution proof in ℂP^{SLD}[σ] this goal is isomorphic to the empty goal of its sort. We illustrate with an example based on the code in the introduction. We consider the length function given in the fragment

begin module "list"
datatype 'a list =  nil | cons of 'a * 'a list
  begin
    fun length nil = (0:int)
     |  length (cons (a,t)) = 1 + length t
  end;

which will give rise to an arrow list(γ) ^{length} int in 𝕁 (and in ℂ), and to the arrow

list(γ) ^{⟨id,length⟩} list(γ) × int

in 𝕁, mapped by σ to itself in ℂ_{P}[σ]. The objects in category ℂ_{P}[σ] are pairs (A, S) where S must satisfy the closure requirement:

for every arrowA ^{φ} list(γ), φ ∘ ⟨id, length⟩ is in S(list(γ) × int)  (10)

since S is a subfunctor of ℂ (A, σ( )). The predicate pred[length] is represented in ℂ_{P}[σ] and in ℂP^{SLD}[σ] as the generic

(list(γ) × int, ≪ id ≫) _{id} (listγ × int, ≪ ∅ ≫)

Its instantiation (pullback) along ⟨id, length⟩ is

(list(γ), ≪ ⟨id, length⟩ ≫) _{id} (listγ, ≪ ∅ ≫)

which has the inverse (list(γ), ≪ ⟨id, length⟩ ≫) _{id} (listγ, ≪ ∅ ≫) since, perhaps suprisingly at first, ≪ ⟨id, length⟩ ≫⊆≪ ∅ ≫ by condition (10) with A = list(γ) and φ the identity. Therefore the (reverse SLD step corresponding to the) arrow □_{σ} ^{id} pred[length](⟨id, length⟩) is in ℂP^{SLD}[σ].

5 Conclusion and future work

We have described a construction of a category of predicates over a base category ℂ, generic up to satisfaction of program clauses and datatype definitions, which gives a category of non-deterministic resolution proofs that implement extended resolution steps capturing program, datatype and basecategory information. The framework is proposed here as a blueprint for incorporating certain types of extensions into constraint logic programming. It has been used elsewhere to extend Hereditarily Harrop logic programming with constraints on terms [10, 7] and with monads [17]. We hope it will prove a natural vehicle for declarative approach to the limited amounts of control and state that are needed in logic programming as well.

Conspicuously absent in this study is a systematic approach to a deterministic implementation of an abstract machine based on this framework, a set of categorical narrowing rules for execution of the code, and reduction rules for computation of pullbacks (or a canonical choice of unifiers) in the base category ℂ, when ℂ is suitably chosen (for example with recursively enumerable pullbacks).

References

[1] A. Asperti and S. Martini. Projections instead of variables, a category theoretic interpretation of logic programs. In Proc. 6^{th} ICLP, pages 337–352. MIT Press, 1989.

[2] R. Barbuti, M Bellia, and G. Levi. Leaf: a Language which Integrates Logic Equations and Functions. Prentice-Hall, 1984.

[3] Michael Barr and Charles F. Wells. Category Theory for Computing Science. Prentice-Hall International, Englewood Cliffs, NJ, USA, 1990.

[4] A. Corradini and A. Asperti. A categorical model for logic programs: Indexed monoidal categories. In Proceedings REX Workshop ’92. Springer Lecture Notes in Computer Science, 1992.

[5] Andrea Corradini and Ugo Montanari. An algebraic semantics for structured transition systems and its application to logic programs. Theoretical Computer Science, 103:51–106, 1992.

[6] Roy Crole. Categories for Types. Cambridge University Press, 1993.

[7] Mary de Marco. Dynamic Constraints and Hereditarily Harrop Programming. PhD thesis, Wesleyan University, 1999.

[8] R. Diaconescu. Category Semantics for Equational and Constraint Logic Programming. PhD thesis, Oxford University, 1994.

[9] Stacy E. Finkelstein, Peter Freyd, and James Lipton. Logic programming in tau categories. In Computer Science Logic ’94, LNCS 933. Springer, 1995.

[10] Stacy E. Finkelstein, Peter Freyd, and James Lipton. A new framework for declara-

tive programming.  Theoretical Computer Science, To appear.  Technical report available as

www.cs.wesleyan.edu/~lipton/jftp/dist96-nfdp.ps.

[11] Peter Freyd and Andre Scedrov. Categories, Allegories. North-Holland, 1990.

[12] Joseph Goguen and José Meseguer. Equality Types and Generic Modules for Logic Programming. Prentice-Hall, 1984.

[13] Tatsuya Hagino. A Category Theoretic Approach to Data Types. PhD thesis, University of Edinburgh, Department of Computer Science, 1987. CST-47-87 (also published as ECS-LFCS-87-38).

[14] Bart Jacobs and Jacob Rutten. A Tutorial on (Co)algebras and (Co)induction, volume 62, pages 222–259. 1997.

[15] M. Martelli M. Falaschi, G. Levi and C. Palamidessi. Declarative modeling of the operational behavior of logic languages. TCS, 69(3), 1989.

[16] Michael Makkai and Gonzalo Reyes. First Order Categorical Logic, volume 611 of Lecture Notes in Mathematics. Springer-Verlag, 1977.

[17] R. McGrail. Modules,Monads and Control in Logic Programming. PhD thesis, Wesleyan University, 1998. To appear.

[18] F. Orejas, E. Pino, and H. Ehrig. Algebraic methods in the compositional analysis of logic programs. In P. Ruzicka I. Privara, B. Rovan, editor, Proc. MFCS 94, volume 841 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

[19] P. Panangaden, V. Saraswat, P.J. Scott, and R.A.G. Seely. A hyperdoctrinal view of constraint systems. In Lecture Notes in Computer Science 666. Springer Verlag, 1993.

[20] A. Poigné. Algebra categorically. In Category Theory and Computer Programming. Springer, 1986.

[21] J. Power and Y. Kinoshita. A new foundation for logic programming. In Extensions of Logic Programming ’96. Springer Verlag, 1996.

[22] D. Pym. Functorial kripke models of the λπ-calculus. Lecture at Newton Institute Semantics Programme, Workshop on Category Theory and Logic Programming, Cambridge, September 1995, 1995.

[23] H. Reichel. Initial Computability, Algebraic Specifications, and Partial Algebras. Oxford University Press, 1987.

[24] D.E. Rydeheard and R.M. Burstall. A categorical unification algorithm. In Category Theory and Computer Programming, 1985.