Logic Programming in Tau Categories ^{∗}

Stacy E. Finkelstein McGill University

       sef@triples.math.mcgill.ca

Peter Freyd University of Pennsylvania

                                     pjf@saul.cis.upenn.edu

James Lipton Wesleyan University

                  lipton@allegory.cs.wesleyan.edu

Abstract

Many features of current logic programming languages are not captured by conventional semantics. Their fundamentally non-ground character, and the uniform way in which such languages have been extended to typed domains, subject to constraints, suggest that a categorical treatment of constraint domains, of programming syntax and of semantics may be closer in spirit to what declarative programming is really about, than conventional settheoretic semantics.

We generalize the notion of a (many-sorted) logic program and of a resolution proof, by defining them both over a (not necessarily free) τ-category C , a category with products enriched with a mechanism for canonically manipulating n-ary relations [8]. Computing over this domain includes computing over the Herbrand Universe, and over equationally presented constraint domains as special cases. We give a categorical treatment of the fixpoint semantics of Kowalski and van Emden, which establishes completeness in a very general setting.

1 Introduction

Tau Categories are categories enriched with a mechanism for canonically manipulating n-ary relations. This τ-structure creates, through canonical limits, an ideal framework for formalizing an abstract syntax for logic programming with constraints. By defining the notions of resolution and unification over such a category, one is able to capture a quite general notion of constraint logic programming and establish a completeness theorem, based on a non-ground categorical generalization of fixed point semantics.

In previous work connecting category theory and logic programming, interpretation of logic in categories has followed a general pattern described by M. Makkai and G. Reyes [15]. The work by A. Corradini and U. Montanari [5] focused on the abstract computations of logic programs and the view of logic programs as structured transition systems. The work by A. Corradini and A. Asperti [4] builds on [5] and defines a model for a logic program as a family of monoidal categories indexed by sets of variables. In both of these works, the category-theoretic setting is semantical and is not used to describe details of the resolution process. The work of Asperti and Martini [2] involves a translation of some of the syntactic mechanisms of resolution along with the interpretation of logic programs in cartesian categories based on the concept of using projections as variables, and was a starting point for our work. The categorical framework can be further exploited to cover more general notions of programming syntax and resolution as well as a cleaner semantics that exploits and strengthens the fixed-point approach of Kowalski and van Emden [13].

∗From: Computer Science Logic ’94, Leszek Pacholski and Jerzy Tiuryn, eds., Lecture Notes in Computer Science 933, Springer, 1995.

Categorical interpretations are often limited by the fact that the main constructs such as products and pullbacks are only defined up to isomorphism, forcing arbitrary choices of representatives of a given isomorphism class. τ-categories, introduced by Peter Freyd in [7] and further explored in Categories, Allegories [8] are a uniform setting in which to work with nary relations and thus describe logic programs. They are finite limit categories enriched with τ-structure, a distinguished class of diagrams which provides canonical choices for limits, and guarantees associative equality and a strict unit for the product.

We begin by describing a categorical syntax for logic programs in an arbitrary τ-category as in [6].

2 τ-categories

We begin with an outline of the theory of τ-categories, described in detail in [8]. We depart slightly from the cited reference in that in this paper, τ-categories need only have all finite products, not all finite limits. The τ-structure guarantees that when finite limits do exist they are canonical. Also note that consideration of this class of categories is not overly restrictive since every small finite limit category is equivalent to a τ-category([8]).

The relevant definitions (of table, short column, compositions and τ-categories) are given in table 1.

An isomorphism class of tables is called a relation. any table is equivalent to a monic composed with a product table. In fact, this is a strong equivalence with regard to the τstructure, as a τ-monic composed with a product τ-table is exactly its equivalent τ-table.

Axiom 1 of the definition of a τ-category says that the class τ is a set of representatives for each isomorphism class of tables. It is this property which allows for a canonical choice of limits. We say that the product diagram ⟨A × B; p_{1}, p_{2}⟩ is canonical if it is a τ-table. Similarly, a pullback diagram is canonical if ⟨P; p_{1}, p_{2}⟩ ∈ τ (where p_{1} : P → A and p_{2} : P → B are the pullback arrows of f : A → C and g : B → C respectively.) These axioms also imply that the category has a unique terminal object.

Canonical limits in τ-categories enjoy several important properties ([8]). Canonical products are strictly associative. The terminator is strictly a two-sided unit. Also, if each of two horizontally adjacent pullback squares is a canonical pullback then so is the outer pullback rectangle they describe.

3 Logical Structure and Interpretation

The information contained in this section describes a τ-categorical syntax for logic programming and is given in greater detail in [6].

The basic translation of the first-order language L into the τ-category follows the usual interpretation as in [15], slightly augmented with the canonical choices allowed by the τ-structure. The relevant definitions are given in table 2. We first define an interpretation of terms, inductively, as arrows in A^{τ}, relative to a sequence of distinct variables containing all of the free variables in the term. We then extend this interpretation to predicates.

Table 1: Tables and τ-categories

Definition 2.1 A table is an object T with a monic finite sequence of morphisms x_{1}, …, x_{n} with T as a common source. We will denote such a table by ⟨T; x_{1}, …, x_{n}⟩.

Definition 2.2 Given a table ⟨T; x_{1}, …, x_{n}⟩ we say that x_{j} is a short column it does not contribute to the monic character of the table, in other words if for every f, g : X → T such that fx_{j} ≠ gx_{j} there exists i < j such that fx_{i} ≠ gx_{i}.

If x_{j} is a short column, then ⟨T; x_{1}, …, x̂_{j}, …, x_{n}⟩ will denote the table obtained by removing the arrow x_{j} from the sequence x_{1}, …, x_{n}.

Definition 2.3 Given tables ⟨T; x_{1}, …, x_{m}⟩ and ⟨T′; y_{1}, …, y_{n}⟩ where x_{j} : T → T′, we define their composition at j as ⟨T; x_{1}, …, x_{m}⟩ ∘_{j} ⟨T′; y_{1}, …, y_{n}⟩ = ⟨T; x_{1}, …, x_{j−1}, x_{j}y_{1}, …, x_{j}y_{n}, x_{j+1}, …, x_{m}⟩.

Definition 2.4 A τ-category is a category with all finite limits and a distinguished class of tables, denoted τ, such that

1. Every table is isomorphic to a unique table in τ.

2. ⟨T; 1_{T} ⟩ ∈ τ, all T.

3. If ⟨T; x_{1}, …, x_{m}⟩ ∈ τ and ⟨T′; y_{1}, …, y_{n}⟩ ∈ τ and x_{j} : T → T′, then

⟨T; x_{1}, …, x_{m}⟩ ∘_{j} ⟨T′; y_{1}, …, y_{n}⟩ ∈ τ

4. If ⟨T; x_{1}, …, x_{n}⟩∈ τ and x_{j} is a short column, then ⟨T; x_{1}, …, x̂_{j}, …, x_{n}⟩ ∈ τ

In the table, we will let L be a first order language, x⃗ = (x_{1}, …, x_{m}) be a sequence of distinct variables of sorts ρ_{1}, ρ_{2}, …, ρ_{m} and let M(x⃗) denote the canonical product M(ρ_{1}) × ⋯ × M(ρ_{m}) in A^{τ}.

It is important to note in the definition of Mx⃗(P t_{1} ⋯ t_{m}) that not only is the arrow p a monic arrow, by a property of pullbacks, but it is also a τ-monic arrow since the second leg of this canonical pullback is short.

3.1 Substitution and Unification in A^{τ}

Let θ = {x_{1} := t_{1}, …, x_{n} := t_{n}} be a substitution with the x_{i}’s all distinct. In addition, let y⃗ = (y_{1}, …, y_{m}) be a sequence of distinct variables containing all of the free variables of the terms t_{i}.

Then we may define a categorical substitution Θy⃗ in A^{τ} to be the morphism:

M(y⃗) \overline{\begin{matrix}⟨My⃗(t_{1}), …, My⃗(t_{n})⟩ \\  \end{matrix}}M(x⃗)

One may prove that for any term s, My⃗(sθ) = Mx⃗(s) ∘ Θy⃗ and thus that a categorical substitution may be applied to a term in this structure via ordinary composition of arrows in A^{τ}.

Definition 3.4 Assume θ and y⃗ are as described above. Given an atomic formula φ, we may define the application of a substitution to φ to be the arrow q which is the canonical pullback of Mx⃗(φ) M(x⃗) along the arrow Θy⃗.

For nonatomic formulae φ:= ∧_{i=1}^{m}A_{i}, one may extend the definition for atomic formulae by taking canonical pullbacks along each τ-monic of φ.

Table 2: Term structure in τ-categories

Terms

Definition 3.1 For any τ-category A^{τ}, an A^{τ} -structure M on the language L is a function M : L → A^{τ} such that for every sort σ in L , M(σ) is an object of A^{τ}, and for every operation symbol f in L of arity n, input sorts σ_{1}, σ_{2}, …, σ_{n}, and of sort ρ, M(f) : M(σ⃗) → M(ρ) is a morphism in A^{τ} where M(σ⃗) denotes the canonical product M(σ_{1}) × ⋯ × M(σ_{n}). (Constants will be thought of as functions of arity 0, and so for each constant c of sort ρ, M(c) : 1 → M(ρ) is a morphism in A^{τ}.)

Definition 3.2 For a term t of sort ρ, having all of its free variables among x⃗, Mx⃗(t) is defined to be a morphism M(x⃗) → M(ρ) in A^{τ} as follows: t:= x_{i} Mx⃗(x_{i}) is defined to be the canonical projection M(x⃗) → M(ρ_{i}) t:= c For a constant c of sort ρ, Mx⃗(c) is defined as the composition:

[figure: M(x⃗); !_{Mx⃗}; 1; M(c); M(ρ)]

t:= ft_{1} ⋯ t_{m} If each t_{i} is of sort σ_{i}, then Mx⃗(ft_{1} ⋯ t_{m}) is defined as the following composition:

[figure: M(x⃗); ⟨Mx⃗(t_{1}), …, Mx⃗(t_{m})⟩; M(σ⃗); M(f); M(ρ)]

Predicates

Definition 3.3 For every predicate symbol R in L with arity n and sorts σ_{1}, σ_{2}, …, σ_{n}, define M(R) to be a τ-monic M(R) → M(σ⃗). For a formula φ with all its free variables among x⃗, Mx⃗(φ) is defined as follows: φ:= Pt_{1} ⋯ t_{m} If each t_{i} is of sort σ_{i}, then Mx⃗(P t_{1} ⋯ t_{m}) is defined to be the τ-arrow p which

is the canonical pullback of M(P) M(σ⃗) along the arrow ⟨Mx⃗(t_{1}), …, Mx⃗(t_{m})⟩. φ:= ∧_{i=1}^{m}A_{i} If each A_{i} is an atom which has been interpreted as described above, then Mx⃗(φ) is

defined to be the m-tuple of τ-monic arrows Mx⃗(A_{i}) M(x⃗).

As in the definition of Mx⃗(P t_{1} ⋯ t_{m}), q will automatically be a τ-monic arrow in A^{τ}. Additionally, one may show for φ := P u_{1} ⋯ u_{k}, My⃗(φθ) = My⃗(P (u_{1}θ) ⋯ (u_{k}θ)).

In a logic programming language, the unifiability of formulae depends on the equality of the predicate symbols and the existence of a unifier, a substitution which unifies the terms appearing in the formulae. In a logic programming τ-category, the unifiability of formulae depends on the equality of the interpretation of the predicate symbol and the existence of a pullback for the terms. It is this ability to define formulae in terms of different lists of variables and then use a pullback to unify them that removes the need for any renaming of variables to avoid clashes.

Definition 3.5 Let φ:= Pt_{1} ⋯ t_{n} and ψ:= Rs_{1} ⋯ s_{m}. φ and ψ are said to be unifiable if the τ-monic arrows M(P) → M(σ⃗) and M(R) → M(ρ⃗) are equal and there exists a pair of substitution arrows ⟨Θy⃗, Φy⃗⟩ forming a commutative square, i.e., such that ⟨Mz⃗(s_{1}), …, Mz⃗(s_{n})⟩∘ Φy⃗ = ⟨Mx⃗(t_{1}), …, Mx⃗(t_{n})⟩ ∘ Θy⃗

In this case the pair ⟨Θy⃗, Φy⃗⟩ are said to unify the formulae φ and ψ. Note that the first condition implies in particular that n=m, M(σ⃗) = M(ρ⃗), and M(P) = M(R). Also note that the occur check is internal to this setting. Since all interpretations are made with respect to a list of variables and, in particular, the substitution arrows are made with respect to an ostensibly different list of variables than the terms to be unified, there can be no substitution of a variable with a term containing that variable unless a separate diagram specifies these to be equal.

In Horn clause logic programming, if unifiers of formulae exist, there are most general unifiers. The corresponding notion in a τ-category is that of canonical pullbacks.

Definition 3.6 Unifiers ⟨Θy⃗, Φy⃗⟩ are most general unifiers (mgu’s) iff the commutative square described in definition 3.5 is a pullback.

In many constraint domains (e.g. the set of closed terms in the lambda calculus), terms may be unifiable without having mgu’s. But if unifiers exist in a category, it is straightforward to add the appropriate pullback squares and form a new τ-category in which mgu’s exist. This is discussed in the last section of the paper.

Lemma 3.7 The two conditions in Definition 3.5 imply that the arrows My⃗(φθ) → M(y⃗) and My⃗(ψϕ) → M(y⃗) are equal when ⟨Θy⃗, Φy⃗⟩ is taken to be most general.

3.2 Resolution

Definition 3.8 Let C be the definite clause A_{1}, A_{2}, …, A_{n} ⊢ B, (for n≥0). Then a definite clause diagram, Mz⃗(C), is the following (n+1)-tuple of τ-monic arrows:

Mz⃗(A_{1})  ⋯  Mz⃗(A_{n})
[figure]
[figure: M(z⃗); Mz⃗(B)]

Definition 3.9 A definite τ-logic program P^{τ} is a finite set of definite clause diagrams Mz⃗(C).

Definition 3.10 Let G be the definite goal B_{1} ∧ B_{2} ∧ … ∧ B_{m}, (for m≥1). Then a definite goal diagram, Mx⃗(G) will be an m-tuple of τ-monic arrows Mx⃗(B_{i}) M(x⃗) to the base M(x⃗).

Definition 3.11 Let Mx⃗(G) be a definite goal diagram, and Mz⃗(C) be a definite clause diagram. Then a new definite goal diagram My⃗(G ′) is derived from Mx⃗(G) and Mz⃗(C) using ⟨Θy⃗, Φy⃗⟩ if the following conditions hold:

1. Mx⃗(B_{i}) → M(x⃗) is the selected τ-monic arrow of Mx⃗(G).

2. ⟨Θy⃗, Φy⃗⟩ is an mgu of Mx⃗(B_{i}) → M(x⃗) and Mz⃗(B) → M(z⃗).

3. My⃗(G ′) is the following definite goal diagram:

My⃗(B_{1}θ) ⋯My⃗(B_{i−1}θ) My⃗(A_{1}ϕ) ⋯ My⃗(A_{n}ϕ) My⃗(B_{i+1}θ)⋯ My⃗(B_{m}θ)
[figure]
M(y⃗)
where recall My⃗(B_{j}θ)  M(y⃗) is defined by a substitution pullback of Mx⃗(B_{j})  M(x⃗)

against Θy⃗.

Definition 3.12 Let A^{τ} be a τ-category, P^{τ} a definite τ-logic program and Mx⃗(G) a definite goal diagram. A τSLD-derivation of P^{τ} ⊢_{A^{τ}} Mx⃗(G) consists of a sequence (finite or infinite) Mx⃗(G), M_{}_{x′}(G_{1}), M_{}_{x′′}(G_{2}), … of definite goal diagrams, a sequence Mz⃗(C_{1}), M_{}_{z′}(C_{2}), … of definite program clauses of P^{τ} and a sequence ⟨Θ^{1}, Φ^{1}⟩ , ⟨Θ^{2}, Φ^{2}⟩ , … of most general unifiers such that each Ma⃗(G_{i+1}) is derived from Mb⃗(G_{i}) and Mc⃗(C_{i+1}) using ⟨Θi+1 ; a⃗, Φi+1 ; a⃗⟩ . A τSLDproof of {Mx⃗(G)} from P^{τ} is a finite τSLD-derivation of P^{τ} ⊢_{A^{τ}} Mx⃗(G) which has the empty diagram as the last definite goal diagram in the derivation.

Definition 3.13 Let P^{τ} be a definite τ-logic program and let Mx⃗(G) be a definite goal diagram. A τ-computed answer for P^{τ} ⊢_{A^{τ}} Mx⃗(G) is the substitution arrow Θ = Θ^{1} ∘ Θ^{2} ∘ ⋯ ∘ Θ^{r} where ⟨Θ^{1}, Φ^{1}⟩ , …, ⟨Θ^{r}, Φ^{r}⟩ is the sequence of most general unifiers used in a τSLD - proof of {Mx⃗(G)} from P^{τ}.

3.3 Models

Definition 3.14 An interpretation for a logic programming structure A^{τ} is a cartesian category D with an associated cartesian functor H : A^{τ} → D.

In the following section we shall only be considering semantic categories D which have the syntactic category as a subcategory. In this case, the functor H will be the obvious inclusion functor which preserves the logical structure.

Definition 3.15 The notion of validity in D (under H) for a formula φ is defined as follows:

1. A conjunction Mx⃗(φ) is valid in D iff H [l], where l: Lim → M(x⃗) is the canonical limit of the diagram Mx⃗(φ), is an isomorphism.

2. A definite clause diagram Mz⃗(A_{1}, A_{2}, …, A_{n} ⊢ B) is valid in D (under H) iff there exists a monic arrow m such that:

H [Lim][figure: m] H [Mx⃗(B)]
[figure: H [l]]
H [M(x⃗)]

where l is the limit of the diagram Mx⃗(ψ) for ψ = A_{1} ∧ A_{2} ∧ … ∧ A_{n}.

3. A logic program P^{τ} is valid in D iff every clause of P^{τ} is valid in D. In this case we say that D (under H) is a model of P^{τ}.

Notice that, for atomic formulas, validity in a model just means it is interpreted as an isomorphism. Also, this definition of validity does not distinguish between ground and nonground terms (the former being terms with source 1).

Theorem 3.16 (Soundness of τSLD-Resolution) Let P^{τ} be a definite τ-logic program and Mx⃗(G) a definite goal diagram. If Θy⃗ is a τ-computed answer for P^{τ} ⊢_{A^{τ}} Mx⃗(G), then it is the case that My⃗(Gθ) is valid in all models of P^{τ}.

4 Completeness of τSLD-Resolution

Let L be the language of the Horn-clause program P and L_{R} = {R_{1}, …, R_{n}} the set of relation symbols in the language, of sorts {σ_{1}, …, σ_{n}}. In order to establish completeness we begin with a category C with terminator and products, in which all sorts, constants and function symbols of L have been interpreted by a C -structure M. On this base category of constraints we create a syntactic category into which we translate logic programs and over which SLD resolution will take place. The syntactic category, (previously denoted A^{τ} in preceding sections) is obtained by freely adjoining indeterminate monics X_{i} B to C , so as to associate to each predicate in L_{R} an indeterminate monic, through which no arrows from C representing terms will factor.

In general, for any category C with terminator and products, and any object B in C , the category C_{B} (also called C[X_{i}] below) obtained by adjoining an indeterminate subobject X_{i} B is defined as follows. The objects of C_{B} are pairs ⟨A, s⟩ where A is an object of C and s is a finite set of morphisms A → B of C . We will let the morphisms ⟨A, s⟩ → ⟨A′, s′⟩ in C_{B} be those morphisms f : A → A′ of C such that for every morphism g : A′ → B in s′ it is the case that f; g : A → B is in s.

C_{B} has a terminal object, ⟨1, ∅⟩, and products for every pair of objects ⟨A, s⟩ and ⟨A′, s′⟩ given by ⟨A × A′, π_{1}s ∪ π_{2}s′⟩, where A × A′ is a product in C with projections π_{1} and π_{2}, and π_{1}s ∪ π_{2}s′ is the union of the sets π_{1}s = {π_{1}f : f ∈ s} and π_{2}s′ = {π_{1}f : f ∈ s′}. In addition, the embedding C ^{ι} C_{B} which sends f : A → A′ in C to f : ⟨A, ∅⟩ → ⟨A′, ∅⟩ in C_{B} is full and faithful and preserves existing limits. We may also consider an underlying functor U : C_{B} → C which sends f : ⟨A, s⟩ → ⟨A′, s′⟩ in C_{B} to its underlying arrow f : A → A′. It is through this functor that C_{B} inherits a τ-structure from C . We may define τ_{D_{B}} by letting a table be in τ_{D_{B}} iff its image under U is in τ_{D} . It is straightforward to verify that this definition of τ_{D_{B}} satisfies the axioms of a τ-category (definition 2.4).

The category C_{B} also has a generic subobject id_{C} : ⟨B, {id}⟩ → ⟨B, ∅⟩. This is our indeterminate monic X ι(B), and it is important to note that all pullbacks of this monic along arrows t from C (so-called “term arrows”) exist in C_{B} and are of the form ⟨A, {t}⟩ ^{id_{C}} ⟨A, ∅⟩ which cannot be an isomorphism in C_{B}.

To emphasize the fact that we are interpreting predicate letters as indeterminate monics, we use the notation C[X] ≡ C [X_{1}, …, X_{n}] for the category obtained from C by freely adjoining indeterminate monics X_{i} M(σ_{i}) one for each R_{i} ∈ L_{R}. We extend M to an interpretation (also called M) of the predicates in L_{R}, by defining M(R_{i}) = X_{i} (that is to say, M(R_{i}) is the monic X_{i} M(σ_{i})). Such a category, along with such a structure map, corresponds to the category A^{τ} and structure map (also denoted M) over which the proof theory has been discussed in previous sections. We shall call the category C[X] with its structure map a logic programming category (an LP-category). We now use the notation P^{τ} ⊢_{C} G to mean there is a τSLD-proof of G from P^{τ} in the category C[X].

Our ambient semantic category will be the topos Ĉgiven by the contravariant Yoneda embedding from C (ie: C Set^{C ^{op}}.) In Ĉwe are able to take unions and images. Hence, in particular, any predicate defined by resolution over C is representable as a monic in Ĉ. We will use this framework to define initial models for logic programs over C, as subcategories of Ĉ.

We will need to make use of a few elementary facts about the Yoneda embedding whose proofs can be found in e.g. [10, 8]. The embedding shown above is full and faithful. The objects B in C appear in Ĉas representable functors Hom( , B), although we will often abuse notation and refer to them by their original names B. All representable functors are coprime and projective. Thus, in particular, arrows from representables into unions of functors in Ĉmust factor through one of them. Also, up to isomorphism, we may take the subobject relation A ⊂ B between subobjects A, B of some object C to be pointwise inclusion of functors. That is to say, given a chain of subobjects of b in Ĉ such as the diagram on the left,

[figure: ⋯; E_{i}; E_{i+1}; ⋯; ⋯; F_{i}; ⊆; F_{i+1}; ⋯]
[figure: g_{1}^{∗}; g_{r}^{∗}; ⊆; ⊆]
b  b

there are isomorphic subobjects F_{i} ≃ E_{i} such that the diagram on the right commutes, with all arrows the canonical inclusions ^{⊆} induced by pointwise set-theoretic containment of functors: for each object X in C, F_{i}(X) ⊆ F_{i+1}(X).

To show completeness, we shall develop a category-theoretic generalization of the Kowalski-Van Emden T_{P} -operator ([13]). We will define an operator T_{P,C} on semantic categories D which builds a new category from D generated by the clauses of the program. By a process of iteration we construct a fixed point for T_{P,C}, an initial model for the program from which we may show completeness.

Throughout, we will denote by (f)^{#} : Sub(a) ⟶ Sub(b) the functor from the lattice of sub-objects of a in Ĉto that of b induced by pulling back along f : b → a, and by ℑ(f) its left adjoint in Ĉ. Notice that ℑ(id)(g) is the image of g in Ĉ.

Definition 4.1 A semantic category is a full subcategory D of Ĉwhich contains C and which is equipped with an extended structure (denoted [[ ]]D ) based on the structure already defined on C (previously denoted M). [[ ]]D will interpret sorts, constants and function symbols as prescribed by the C -structure M, and will assign to each predicate symbol a monic arrow of D.

Note that one may show using a straightforward induction on terms that for any term t, [[t]]D_{x⃗} = [[t]]C_{x⃗} . Thus we will often drop the superscripted categories from our notation when discussing interpretations of terms.

Given a program P let us denote by cl a clause A_{1}, A_{2}, …, A_{n} ⊢ B(t). We will then mean by hd_{cl} the predicate symbol B (the head of cl), by tm_{cl} the term t (associated with hd_{cl}), and by tl_{cl} the list A_{1}, …, A_{n} (the tail of cl). We then make the following categorical notational definitions.

Definition 4.2 Let P^{τ} be a definite τ-logic program in a semantic category D with extended structure [[ ]]D . Then denote by [[cl]]D the definite clause diagram associated with A_{1}, A_{2}, …, A_{n} ⊢ B(t). We will define [[hd_{cl}]]D to be [[B]]D , [[tm_{cl}]]D_{x⃗} to be [[t]]D_{x⃗} , and [[tl_{cl}]]D_{x⃗} to be the monic from the limit of the (definite goal) diagram consisting of the fan of arrows [[A_{i}]]D_{x⃗} [[x⃗]]D from the clause diagram above.

Definition 4.3 If [[t]]_{x⃗} : M(x⃗) → M(σ⃗) and [[r]]_{y⃗} : M(y⃗) → M(σ⃗) are terms, then [[t]]_{x⃗} is said to factor through [[r]]_{y⃗} in D if there exists an arrow θ in D such that the arrows id and θ are pullbacks of the arrows [[t]]_{x⃗} and [[r]]_{y⃗} respectively.

We remind the reader that the Yoneda embedding reflects factorizations, since it is full: if [[t]]_{x⃗} factors through [[r]]_{y⃗} in Ĉ, then it factors through in C .

In favt we have the following, which will be useful in proving completeness of resolution.

Proposition 4.4 Let C_{1}  ^{r} C_{2} and C_{0}  ^{t} C_{2} be arrows in C . If [[t]] factors through

ℑ( [[r]])(F) for some subobject F of [[C_{1} ]] in Ĉ, then t is an instance of r in C and [[t]] factors through F [[r]]. In particular, there is an arrow C_{0} ^{φ} C_{1} such that t = φr and [[φ]] factors through F.

Proof. Consider the diagram

[[C_{0} ]]

[figure: ......................................................; ϱ; u]

[figure: F̄; e; \overline{ℑ( [[r]])(F)}; ℑ( [[r]])(F); [[C_{2} ]]; [[t]]]

[figure: F; [[r]]]

[[C_{1} ]]

where e; ℑ( [[r]])(F) is an epi-monic image factorization of F [[r]] and each [[C_{i}]] is a representable functor in Ĉ, and therefore projective. The projectivity of [[C_{0} ]] implies that the arrow u (which exists by the hypothesis that [[t]] factors through ℑ( [[r]])(F)) lifts to an arrow ϱ making the diagram commute. Let f = ϱ F. The source and target of f are representable, so by the fullness of the Yoneda embedding, f = [[φ]] for some substitution φ, and [[φ]] [[r]] = [[t]]. By faithfulness of the Yoneda embedding, φr = t. □

Van Emden and Kowalski introduced an elegant semantics for Prolog in terms of fixed points of a continuous operator T_{P} on the power set of the Herbrand base B_{P} of a prolog program P [13]. The action of T_{p} on a subset S of B_{P} is given by:

T_{P} (S) = S ∪ {Q(t′) : A′_{1}, …, A′_{n} ⊢ Q(t′) is a ground
instance of a clause in P & A′_{1}, …, A′_{n} ∈ S}.

The least term model of P is precisely the least fixed point of T_{P} which we can think of as building the model as a (co-)limit of a chain. If we fix a predicate letter Q, we can think of each clause A_{i}, …, A_{n} ⊢ Q(t) in P as contributing to the extent of Q all ground instances of t corresponding to terms in the interpretation of the A_{i}. Because of the non-ground nature of categorical semantics we can define analogous operators E and T_{P,C} over our more general categorical models in many respects simpler their set-theoretic counterpart. The operator E adjoins finitely many arrows to the arrow interpreting the predicate Q in a category. The fact that this is done over an arbitrary category C with terminator and certain limits poses no difficulties. The main idea is as follows. We assume the predicate letter B has the interpretation [[B]]^{D} in some category D. Then if A_{1}, …, A_{n} ⊢ B(t) is a clause in P, let [[A_{1}, …, A_{n}]]D_{x⃗} be the limit of the clause diagram for A_{1}, …, A_{n} in D. Then we define E by

E( [[ ]]D , B) = [[B]]D ∪ ℑ( [[t]]D_{x⃗} )( [[A_{1}, …, A_{n}]]D_{x⃗} ) ∪ ⋯

where the remaining terms of the union, not shown, correspond to any remaining clauses in P whose head predicate letter is B, and where, we recall, ℑ( [[t]]D_{x⃗} ) is the image functor along t. We now give this definition in its full generality.

Definition 4.5 Let D be a semantic category as defined in definition 4.1 with extended structure [[ ]]D . Then for each predicate letter B ∈ L_{R} define the following

E( [[ ]]D , B) = [[B]]D ∪ [ ⋃_{hd_{cl}=B^{cl∈P}}{ℑ( [[tm_{cl}]]D_{x⃗} )( [[tl_{cl}]]D_{x⃗} )}]

For each term s in C , let

E( [[ ]]D , B, s) = ( [[s]]D_{y⃗} )^{#}(E( [[ ]]D , B))

Note that these arrows are in Ĉ, but not, in general, in D.

Now let T_{P,C}(D) be the full subcategory of Ĉgenerated by D, 0 ∈ Ĉ, E( [[ ]]D , B) for each predicate letter B ∈ L_{R}, and closed under finite limits. T_{P,C}(D) is then also a semantic category with extended structure defined by [[B]]^{T_{P,C}(D )} = E( [[ ]]D , B) for predicate symbols B ∈ L_{R}.

In particular, let C _{0} be the full subcategory of Ĉobtained by adjoining to the original category C the co-terminator 0 of Ĉand defining an extended interpretation [[ ]]^{0} given by [[B]]^{0} = the unique map 0 → [[b]]^{0} for predicate symbols B ∈ L_{R}, where b = sort of B. We may then define a sequence of categories C _{0}, C _{1}, …, C _{n}, … built by letting C _{i+1} = T_{P,C}(C _{i}), each with the extended interpretation [[B]]^{n} given in the definition of T_{P,C}(C _{i}).

Construct for each predicate symbol B ∈ L_{R} the filtered colimit in Ĉof the following diagram of inclusions

[figure: [[B]]^{0}; [[B]]^{1}; ⋯; [[B]]^{k}; ⋯]

Lemma 4.6 \underrightarrow{lim}\{ [[B]]^{n}\} ≅ ⋃_{n}\{ [[B]]^{n}\}

This follows easily from the facts about the Yoneda embedding at the beginning of the section. In particular, we may take the preceding diagram of inclusions to be pointwise containment of functors F_{n}. The pointwise union of this diagram is easily seen to be its colimit.

Definition 4.7 We define C^{∗} as the full subcategory of Ĉgenerated by the categories C _{k}, \underrightarrow{lim}\{ [[B]]^{n}\} for each predicate symbol B ∈ L_{R}, and closed under finite limits. For this category we then define an extended structure by [[B]]^{∗} = \underrightarrow{lim}\{ [[B]]^{n}\} for each predicate symbol B ∈ L_{R}.

Lemma 4.8 [[tl_{cl}]]∗ ; x⃗ = \underrightarrow{lim}\{ [[tl_{cl}]]k ; x⃗\}

Proof. Consider the clause diagram [[cl]]^{k} in C _{k} as defined in definition 4.2. Let [[A_{i}]]∗ ; x⃗ be given by [[A_{i}]]∗ ; x⃗ = ( [[u]]∗ ; x⃗)^{#} [[A′_{i}]]^{∗}, where A_{i} = A′_{i}(u). By definition [[A′_{i}]]^{∗} = \underrightarrow{lim}\{ [[A′_{i}]]^{k}\}. Hence, [[A_{i}]]∗ ; x⃗ = ( [[u]]∗ ; x⃗)^{#}(\underrightarrow{lim}\{ [[A′_{i}]]^{k}\}). So since (−)^{#} is also a left adjoint (in addition to being a right adjoint), we have [[A_{i}]]∗ ; x⃗ = \underrightarrow{lim}\{( [[u]]∗ ; x⃗)^{#} [[A′_{i}]]^{k}\}_{k}. But then, [[A_{i}]]∗ ; x⃗ = \underrightarrow{lim}\{( [[u]]k ; x⃗)^{#} [[A′_{i}]]^{k}\}_{k} = \underrightarrow{lim}\{ [[A_{i}]]^{k}\}_{k}. And so

[[tl_{cl}]]∗ ; x⃗ = \underleftarrow{lim}\{ [[A_{i}]]∗ ; x⃗\}_{i}
= \underleftarrow{lim}\{\underrightarrow{lim}\{ [[A_{i}]]^{k}\}_{k}\}_{i}
= \underrightarrow{lim}\{\underleftarrow{lim}\{ [[A_{i}]]^{k}\}_{i}\}_{k}
= \underrightarrow{lim}\{ [[tl_{cl}]]k ; x⃗\}_{k}

because filtered colimits commute with finite limits in a topos (eg [3]). □

Lemma 4.9 The category C^{∗} with interpretation H : C[X] ⟶ C^{∗} induced by evaluation H(X_{i}) = [[B]]^{∗} is a model of the program P.

Proof. We show that T_{P,C}(C^{∗} ) = C^{∗} , and, in particular, that E preserves colimits of subobject chains, ie.

[[B]]^{∗} = [[B]]^{∗} ∪ [ ⋃_{hd_{cl}=B^{cl∈P}}{ℑ( [[tm_{cl}]]_{x⃗})( [[tl_{cl}]]∗ ; x⃗)}]  (1)

for each predicate letter B ∈ L_{R}. It will suffice to show that for each clause such that hd_{cl} = B, ℑ( [[tm_{cl}]]_{x⃗})( [[tl_{cl}]]∗ ; x⃗) ⊆ [[B]]^{∗}. Then since ℑ( [[tm_{cl}]]_{x⃗}) is the left adjoint of ( [[tm_{cl}]]_{x⃗})^{#}, it suffices to show [[tl_{cl}]]∗ ; x⃗ ⊆ ( [[tm_{cl}]]_{x⃗})^{#} [[B]]^{∗}. We know by the definition of [[B]]^{k+1} that ℑ( [[tm_{cl}]]_{x⃗}) [[tl_{cl}]]k ; x⃗ ⊆ [[B]]^{k+1}. So since (-)^{#} is also a left adjoint, we have that for each k

[[tl_{cl}]]k ; x⃗ ⊆ ( [[tm_{cl}]]_{x⃗})^{#} [[B]]^{k+1}
⊆ \underrightarrow{lim}\{( [[tm_{cl}]]_{x⃗})^{#} [[B]]^{k}\}
= ( [[tm_{cl}]]_{x⃗})^{#}\underrightarrow{lim}\{ [[B]]^{k}\}
= ( [[tm_{cl}]]_{x⃗})^{#} [[B]]^{∗}

By lemma 4.8 we know that [[tl_{cl}]]∗ ; x⃗ = \underrightarrow{lim}\{ [[tl_{cl}]]k ; x⃗\}. Thus we may conclude by the universal property of colimits that

[[tl_{cl}]]∗ ; x⃗ = \underrightarrow{lim}\{ [[tl_{cl}]]k ; x⃗\} ⊆ ( [[tm_{cl}]]_{x⃗})^{#} [[B]]^{∗}  (2)

In fact it is the case that for any semantic category D, being a fixed point of T_{P,C} is equivalent to being a model of P. In the proof above, one sees that to show C^{∗} a fixed point of T_{P,C} (equation 1 for each predicate letter B), one may equivalently show that for each clause such that hd_{cl} = B, C^{∗} is a model of P (equation 2). □

Lemma 4.10 ( [[ ]]-monotonicity) If for every predicate letter A in L_{R}, [[A]]D ⊆ [[A]]D′ then for any predicate letter B ∈ L_{R} and any term t, E( [[ ]]D , B, t) ⊆ E( [[ ]]D′, B, t).

Proof. Since limits preserve containment, it suffices to show that for any predicate letter B ∈ L_{R}, E( [[ ]]D , B) ⊆ E( [[ ]]D′, B). By hypothesis, [[B]]D ⊆ [[B]]D′. Also, since [[A_{i}]]D_{x⃗} ⊆ [[A_{i}]]D′_{x⃗} for each [[A_{i}]]D_{x⃗} in [[tl_{cl}]]D_{x⃗} and each [[A_{i}]]D′_{x⃗} in [[tl_{cl}]]D′_{x⃗}, we have that [[tl_{cl}]]D_{x⃗} ⊆ [[tl_{cl}]]D′_{x⃗} for each clause cl ∈ P such that hd_{cl} = B. But since in any regular category the functor ℑ(s), for any arrow s, preserves containment of monics, it is the case that for each clause cl ∈ P such that hd_{cl} = B, ℑ( [[tm_{cl}]]D_{x⃗} )( [[tl_{cl}]]D_{x⃗} ) ⊆ ℑ( [[tm_{cl}]]D′_{x⃗})( [[tl_{cl}]]D′_{x⃗}). But now the required containment follows directly from elementary properties of unions. □

Lemma 4.11 C^{∗} is an initial model of P.

Proof. We want to show that for any model D of P (ie any semantic category D which is a fixed point of T_{P,C}), that validity in C^{∗} implies validity in D. In particular, it suffices to show that for any predicate letter B ∈ L_{R}, [[B]]^{∗} ⊆ [[B]]D .

We first show by induction on k that for all k, [[B]]^{k} ⊆ [[B]]D . Since [[B]]^{0} = the unique map 0 → [[b]]^{0} for b = sort of B, it is clear that [[B]]^{0} ⊆ [[B]]D . Now suppose that [[B]]^{k} ⊆ [[B]]D . By Lemma 4.10 and the fact that D is a fixed point of T_{P,C}, [[B]]^{k+1} = E( [[ ]]^{k}, B) ⊆ E( [[ ]]D , B) = [[B]]D .

It now follows by the definition of [[B]]^{∗} and Lemma 4.6 that [[B]]^{∗} = \underrightarrow{lim}\{ [[B]]^{n}\} ≅

⋃_{n}{ [[B]]^{n}} ⊆ [[B]]D . □

Definition 4.12 A clause A_{1}, A_{2}, …, A_{m} ⊢ B(r) is said to admit Q(t) if B = Q and [[t]]_{x⃗} factors through [[r]]_{y⃗}.

Lemma 4.13 If an atomic formula Q(t) is valid in all models of the program P, (i.e. is interpreted as an isomorphism) then some clause of P admits Q(t).

Proof. Consider the following model D of the program P. Adjoin to C the arrows (in Ĉ):

⋃_{hd_{cl}=Q^{cl∈P}} Im( [[tm_{cl}]]_{y⃗})

for each predicate letter Q ∈ P and close under finite limits. Let D be the full subcategory of Ĉgenerated by this. Now let the extended structure [[ ]]D be defined by

[[B]]D = ⋃_{hd_{cl}=Q^{cl∈P}} Im( [[tm_{cl}]]_{y⃗})

where by convention, if B ∉ P then [[B]]D (the empty union) shall be the unique arrow 0 → [[b]] for b = sort of B.

The category D with interpretation H : C[X] ⟶ D induced by evaluation H(X_{i}) = [[B]]D is a model of the program P since if A_{1}, A_{2}, …, A_{m} ⊢ B(r) is a clause cl of P, then [[r]]_{y⃗} factors

through Im( [[r]]_{y⃗}) and so through [[B]]D . Thus [[B(r) ]]D_{y⃗} is an isomorphism through which

[[tl_{cl}]]D_{y⃗} factors automatically.

Now, since Q(t) is valid in all models, [[Q(t) ]]D_{x⃗} is an isomorphism. In other words, [[t]]_{x⃗} factors through [[Q]]D = ⋃_{hd_{cl}=Q^{cl∈P}} Im( [[tm_{cl}]]_{y⃗}). But then, by coprimeness of representable

objects of Ĉ(i.e. images of objects of C under the Yoneda embedding) [[t]]_{x⃗} must factor through Im( [[r]]_{y⃗}) for some particular clause A_{1}, A_{2}, …, A_{m} ⊢ Q(r) in P. By proposition 4.4 then, [[t]]_{x⃗} must factor through [[r]]_{y⃗} and fullness of the Yoneda embedding, the factoring arrow must be in C . Thus, this clause of P admits Q(t). □

Lemma 4.14 Let G be an atomic formula. If [[G]]k ; x⃗ is an isomorphism, then there is a τSLDproof of M C[X] ; x⃗(G).

Proof. The proof will proceed by induction on k.

If k = 0, then the lemma holds vacuously since for all predicate letters B ∈ L_{R}, [[B]]^{0} : 0 → [[b]] where b is the sort of B, which cannot be an isomorphism. Now assume that the lemma is true for k = n. And suppose that [[G]]n+1 ; x⃗ is an isomorphism, where G = Q(t) for some predicate letter Q and term t. If [[Q(t) ]]n ; x⃗ is also an isomorphism, then the lemma holds by the induction hypothesis. So assume that [[Q(t) ]]n ; x⃗ is not an isomorphism. By definition

[[Q(t) ]]n+1 ; x⃗ = E( [[ ]]^{n}, Q, t) = ( [[t]]_{x⃗})^{#} ( [[Q]]^{n} ∪ [ ⋃_{hd_{cl}=Q^{cl∈P}}{ℑ( [[tm_{cl}]]_{y⃗})( [[tl_{cl}]]n ; y⃗)}])

Since this is an isomorphism, then [[t]]_{x⃗} factors through the union

( [[Q]]^{n} ∪ [ ⋃_{hd_{cl}=Q^{cl∈P}}{ℑ( [[tm_{cl}]]_{y⃗})( [[tl_{cl}]]n ; y⃗)}])

But then, since M(x⃗) (or, more precisely, its image in Ĉ) is coprime, it must be the case that [[t]]_{x⃗} factors through one of the members of the union. Since we have assumed that [[t]]_{x⃗} does not factor through [[Q]]^{n}, it must be the case that for some clause cl ∈ P such that hd_{cl} = Q (say the clause A_{1}, A_{2}, …, A_{m} ⊢ Q(r)) ( [[t]]_{x⃗})^{#}ℑ( [[r]]_{y⃗})( [[tl_{cl}]]n ; y⃗) is an isomorphism. In fact, by Lemmas 4.13 and 4.11 and 4.4, there is a substitution arrow Θx⃗ in C , corresponding to a substitution θ on terms, such that Θx⃗ [[r]]_{y⃗} = [[t]]_{x⃗} and such that Θx⃗ factors through [[tl_{cl}]]n ; x⃗, i.e. [[tl_{cl}θ]]n ; x⃗ is an isomorphism.

Thus, we have that for each i, [[A_{i}θ]]n ; x⃗ is an isomorphism. But then, by our induction hypothesis, there are τSLD-proofs of M C[X] ; x⃗(A_{i}θ) for each i.

We may then build a τSLD-proof of M C[X] ; x⃗(Q(t)) as follows. Using the clause diagram on the left below, we may take one τSLD-derivation step using ⟨id, θ⟩ as mgu. Then our new goal would be the diagram on the right below. But, as mentioned above, each of these has a (finite) τSLD-proof.

M C[X] ; y⃗(A_{1})  ⋯  M C[X] ; y⃗(A_{m})  M C[X] ; x⃗(A_{1}θ)  ⋯  M C[X] ; x⃗(A_{m}θ)
[figure]
[figure: M(y⃗); M C[X] ; y⃗(Q(r)); M(x⃗)]
□
Lemma 4.15 Suppose the pullback [[Bt]]∗ ; x⃗  [[x⃗]]^{∗} of the monic [[B]]^{∗}  b interpreting

Bt in C^{∗} is an isomorphism. Then, for some k so is the corresponding pullback [[Bt]]k ; x⃗ [[x⃗]]^{∗} interpreting Bt in C _{k}.

Proof. Suppose pulling back [[B]]^{∗} along t in C^{∗} gives rise to an isomorphism γ:

[figure: [[Bt]]∗ ; x⃗; β; [[B]]^{∗}; or equivalently; [[x⃗]]; γ^{−1}β; [[B]]^{∗}; [[x⃗]]; γ; [[t]]_{x⃗}; b; [[x⃗]]; id; [[t]]_{x⃗}; b]

Then [[x⃗]] ^{γ^{−1}β} [[B]]^{∗} is an arrow from an object in C , i.e. a representable functor in Ĉto [[B]]^{∗} ≃ ⋃ [[B]]^{n}. By the coprimeness of C -objects in Ĉ, γ^{−1}β factors through some [[B]]^{k} as [[x⃗]] ^{δ} [[B]]^{k} ⊂ [[B]]^{∗}. It is then straightforward to show that the arrows id and δ are pullbacks

of the arrows [[t]]_{x⃗} and [[B]]^{k}  b respectively.  □

Theorem 4.16 (Completeness of τSLD-Resolution) Let C be a category and C[X]a logic programming category with extended structure M : L → C[X] as described previously. Let P^{τ} be a τ-logic program in the language L and G a definite goal diagram. If G holds in every model of P^{τ}, then P ⊢_{C} G (ie: there is a τSLD-proof of G from P^{τ} in the category C[X]).

Proof. Let P^{τ} as described above have clause diagrams MC[X](cl^{1}), …, MC[X](cl^{m}) and let G be a definite goal diagram (ie diagram at left below) such that for every model of P^{τ}, G is true.

M C[X] ; y⃗(G_{1})  ⋯  M C[X] ; y⃗(G_{r})  [[G_{1} ]]∗ ; y⃗  ⋯  [[G_{r} ]]∗ ; y⃗
[figure: g_{1}^{∗}; g_{r}^{∗}]
M(y⃗)  [[y⃗]]

In particular then, for the model C^{∗} of P^{τ}, we have that H [ℓ], where ℓ is the limit of the diagram G at left above, is an isomorphism. Since by definition, H [ℓ] is the limit of the diagram at right above, if it is an isomorphism, then g_{j}^{∗} is an isomorphism for each j. But now by Lemma 4.15, g_{j}^{k} is an isomorphism for each j, so by Lemma 4.14 there is a τSLD-proof of M C[X] ; y⃗(G_{j}) for each j. □

5 Some Examples of Constraint Categories

Let L be the language of a one-sorted Horn clause program. Define H, the free category associated with L (also known as the empty algebraic theory for L) to be the small category with objects the natural numbers 0, 1, …, and arrows given by the following. For each nonzero pair of objects m, n with m ≤ n a projection map π_{m}^{n} : n → m, a diagonal arrow δ_{n}^{m} : m → n and, for each function symbol f of arity n in L an arrow f: n → 1. These arrows satisfy the equations for associativity as well as

π_{m}^{n}π_{k}^{m} = π_{k}^{n} and δ_{n}^{m}π_{m}^{n} = id_{m} = δ_{m}^{m} = π_{m}^{m}

This category has products and τ structure, as the reader can check. Furthermore there is a one-to-one correspondence between arrows in H and (tuples) of terms in the Herbrand universe over L. If we now give H the canonical interpretation that associates with each f in L the arrow f and let H[X_{1}, …, X_{n}] be the category obtained by adjoining indeterminates for each of the predicate letters in L, then H[X_{1}, …, X_{n}] captures logic programming in the sense made precise in the theorem below. Terminology is from [13].

Theorem 5.1 Let P be a Horn clause program, G a (possibly open) definite goal. Then there is an SLD proof P ⊢_{H}G over this category if and only if there is a computed answer for P ∪ {G}

This example is essentially the case studied in [2]. A straightforward adaptation of this construction gives the corresponding free category for many-sorted logic.

We can modify the preceding construction to capture equational constraints. Let L be a language, possibly many-sorted, and E an equational theory over L. By taking a quotient of the Herbrand category H/E we obtain the algebraic theory associated with E, containing the same objects as H and congruence classes of arrows of H as morphisms. The construction is well known (see e.g. [18]). We then add mgu’s by selectively completing this category by adjoining terminal cones (i.e. pullbacks) to all commutative syntactic squares, that is to say, to all diagrams consisting of interpretations of terms in L and their corresponding unifiers. We obtain a category in which a pullback of the arrows corresponding to two terms exists precisely when the terms are E-unifiable, that is to say, when there is a substitution θ such that E ⊧ sθ = tθ. SLD-resolution over this category corresponds to finding a computed answer with equational constraints from E.

Note that for domains with pairing or projection operations (see e.g. [19, 12]), first order constraints are equivalent to (variable-free) equational set constraints using the allegory-theoretic connectives ∩, ∪, ·/., ( )^{o} (and complementation in the case of classical logic). Thus first-order constraints can be captured with many-sorted equational categories of the type just discussed.

6 Conclusion

We have shown how a general notion of many-sorted, non-ground constraint logic programming can be captured by a categorical abstract syntax in which resolution takes place via pullbacks in a τ-category with canonical products, monics and limits. A categorical analogue of the T_{P} operator of Kowalski and Van Emden gives a completeness theorem for this notion in semantic categories defined via the Yoneda embedding.

This categorical framework opens the way for a categorical approach to the semantics of uniform proof systems and higher-order logic programming [16] and as well as for the formalization of control. It would be interesting to study connections with the hyperdoctrinal constraints of [17], and with the π domains and non-ground semantics of [1]. Also worth exploring in this context is a categorical theory of abstract interpretation based on adjunctions over the Yoneda category Ĉ.

References

[1] G. Levi A. Bossi, M. Gabbrielli and M. Martelli. The s-semantics approach: Theory and applications. Journal of Logic Programming, 19-20, 1994.

[2] A. Asperti and S. Martini. Projections instead of variables, a category theoretic interpretation of logic programs. In Proceedings of the 6^{th} International Conference on Logic Programming, pages 337–352. MIT Press, 1989.

[3] Michael Barr and Charles Wells. Toposes, Triples, and Theories. Springer-Verlag, 1985.

[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] A. Corradini and U. Montanari. An algebraic semantics of logic programs as structured transition systems. In Proceedings of the North American Conference on Logic Programming (NACLP ’90). MIT Press, 1990.

[6] Stacy E. Finkelstein. Tau Categories and Logic Programming. PhD thesis, University of Pennsylvania, 1994.

[7] Peter Freyd. On canonizing category theory or on functorializing model theory. A Pamphlet, March 1974.

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

[9] Joxan Jaffar and Jean-Louis Lassez. Constraint logic programming. In Proceedings of Symposium on Principles of Programming Languages. ACM, 1987.

[10] J. Lambek and P.J. Scott. Introduction to Higher Order Categorical Logic. Cambridge University Press, 1986.

[11] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic: a first introduction to topos theory. Springer-Verlag, 1992.

[12] James Lipton and Paul Broome. Combinatory logic programming: Computing in relation algebras and allegories. In Proceedings of 1994 the International Logic Programming Symposium. MIT Press, 1994.

[13] J. W. Lloyd. Foundations of Logic Programming. Springer Verlag, New York, 1987.

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

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

[16] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 1990.

[17] 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.

[18] Axel Poigne. Algebra categorically. In Category Theory and Computer Programming, LNCS 240. Springer-Verlag, 1986.

[19] Alfred Tarski and Steven Givant. A formalization of Set Theory without variables. American Mathematical Society, Providence, R.I., 1987.