A New Framework for Declarative Programming

Stacy E. Finkelstein McGill University and University of Ottawa

          sef@triples.math.mcgill.ca

Peter Freyd University of Pennsylvania

                                             pjf@saul.cis.upenn.edu

James Lipton Wesleyan University

                    lipton@allegory.cs.wesleyan.edu

Contents

1 Introduction 2

2 Syntax over a categorical signature 4 2.1 Categorical Signatures and Categorical Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 τ-Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 2.3 Interpreting Conventional Logical Structure over a Category . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.3.1 Interpretation of the Terms and Formulae . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.3.2 Notation and Shared Data . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

2.4 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

3 Horn Logic Programming Categories 12

3.1 Generic Predicates and unordered goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

3.1.1 Generic Predicate Diagrams . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 3.2 Predicates via indexed categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.3 From Formula Diagrams to Generalized Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.3.1 Unordered Goals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

4 Program Syntax 22 4.1 Uniform Programming Categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 4.2 Programs as Sets of Formal Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 4.3 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

5 Operational Semantics 28 5.1 The Operational Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 5.2 Indexing over state information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 5.3 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 5.4 The Semantic Operator E_{P}: the WHH case . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 5.5 The Approximate Interpretations and their Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 5.6 The Kowalski-van Emden model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 5.7 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39

6 Topos Semantics 44

6.1 First-order Logic over a Finite Product Category . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 6.1.1 Expanding the signature . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 6.1.2 A Sequent Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46

6.2 Henkin Interpretations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 6.3 The Canonical Henkin Interpretation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49

7 Examples and Conclusion 51 7.1 Perspectives on Uniform proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 7.2 Directions for future work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54

A Proofs of Theorems 54

B A Sketch of the Grothendieck Construction 63

Abstract

We propose a new framework for the syntax and semantics of Weak Hereditarily Harrop logic programming with constraints, based on resolution over τ-categories: finite product categories with canonical structure.

Constraint information is directly built-in to the notion of signature via categorical syntax. Many-sorted equational constraints are a special case of the formalism which combines features of uniform logic programming languages (modules and hypothetical implication) with those of constraint logic programming. Using the canonical structure supplied by τ-categories, we define a diagrammatic generalization of formulas, goals, programs and resolution proofs up to equality (rather than just up to isomorphism).

We extend the Kowalski-van Emden fixed point interpretation, a cornerstone of declarative semantics, to an operational, non-ground, categorical semantics based on indexing over sorts and programs.

We also introduce a topos-theoretic declarative semantics and show soundness and completeness of resolution proofs and of a sequent calculus over the categorical signature. We conclude with a discussion of semantic perspectives on uniform logic programming.

1 Introduction

Logic programming is based, in principle if not in practice, on the declarative paradigm of programming with executable specifications, that is to say, with code whose text has independent mathematical meaning consistent with its input-output behavior. Originally the specifications were taken to be first-order Horn theories, with a restricted proof search, resolution, as the computational engine.

However, the demand for more expressive power and efficiency has led language designers to consider logical extensions to the original Horn Clause core [26, 48, 51, 50, 46, 28]) and to add control features and constructs drawn from other language paradigms (e.g. types [55, 32, 49], partial evaluation [31] and constraints [10, 29, 30], to name just a few). The effect has been to expand the boundaries of the subject and of the very notion of declarative content of a program. A more general syntax and semantics is needed to model these new features and provide criteria for good language design.

Furthermore, there is a substantial gap between semantic methods in the functional, imperative and declarative programming communities. It is therefore hard to evaluate the effectiveness of proposals to add imported features to logic programming within an agreed-upon common framework. A categorical foundation for logic programming seems to be an essential tool in this endeavor. This paper is an effort to provide such a foundation.

Categories and Logic Programming Categorical tools in programming syntax and semantics have enjoyed widespread use for over a decade [56]. Categorical models have been used to give clean, implementation-independent approaches to side effects and state [47, 62, 68, 52], non-determinism [53], type disciplines [15, 33] and other logics for computation [7, 63]. The mathematical treatment of some features, such as parametricity and polymorphism, have required categorical tools [57, 21].

Logic programming, however, has developed within a different semantic tradition than that of functional or imperative programming. The divide has narrowed in the last ten years, with the development of new denotational, operational, and abstract interpretations for logic programs [11, 39, 40, 14, 31, 38]. There has been a growing interest in a categorical formulation of these ideas, essentially for the same reasons they proved of interest in other programming paradigms.

Categorical approaches to logic programming features appeared in the mid 1980’s in Rydeheard and Burstall’s treatment of unification [61], also developed independently by Goguen. In 1989, Asperti and Martini [4] formalized the syntax of Horn clause programming over the Herbrand Universe using first-order categorical logic as developed in e.g. [41] and gave a topos-theoretic semantics. In 1992, Corradini, Asperti and Montanari gave a categorical analysis of logic program transitions [13] and of logic program structure using indexed monoidal categories [12]. In [54] Panangaden, Scott, Seely, Saraswat, gave a categorical formulation of concurrent constraints for logic programming. In 1994 Diaconescu [19] formalized equational constraint Horn Clause programming using categories and institutions. In 1995 the authors gave a new syntax and a categorical generalization of the fixed point semantics for the Horn case. The following year Power and Kinoshita [59] gave an indexed category description of Horn Clause resolution, and more recently, Pym [60] has developed a categorical formulation of Horn clause program evaluation within a typed, realizability-style metamathematical framework.

Our contribution in this paper is a new categorical syntax with canonical structure supplied by finite product τ-categories, a definition of resolution over such categories for Weak Hereditarily Harrop programs, and an operational(fixed point) and declarative categorical semantics, with respect to which resolution and a categorical sequent calculus are shown sound and complete.

Our operational model theory is a generalization of the Kowalski-Van Emden fixed-point semantics based on indexing not just over sorts but programs. We show how indexing of local logic programming fibers over a state category places substitution, program augmentation and state change within a single framework.

Outline of the Paper The following section is devoted to a description of categorical syntax for logic programming. We begin with a definition of formula diagrams over a categorical signature that builds-in constraint information. We then define finite-product τ-categories and state some of their properties. We define categorical substitution and unification along the lines already familiar from the literature. In the next sections we give a new construction for adjoining predicates freely to a categorical signature and define programs and clauses over generic atomic predicates. The last two sections are devoted to a treatment of operational (fixed point) interpretations and declarative (topos-theoretic) semantics. We give soundness and completeness of two notions of proof for both and conclude with some examples and a discussion of the implications of our work for a semantics-based notion of the declarative paradigm.

Notational Conventions

The categorical background required in this paper can be found in the first few chapters of most category theory texts. The reader should know what limits, colimits and adjoints are. Some notational conventions are taken from [23]. Compositions of morphisms are given in diagrammatic order: the composition

A ^{f} B ^{g} C

is denoted fg. Cartesian Categories are categories with all finite limits. Categories with all finite products (and terminator) are called FP categories. The pullback of a monic arrow A ^{t} B along a co-terminal arrow C ^{f} B (to an arrow whose target is C) is denoted f^{#}(t):

[figure: D; A; C; f^{#}(t); f; B; t]

We sometimes denote the source D of the pulled back arrow f^{#}(t) by f^{#}(A).

A subobject of an object B is the equivalence class of all monics with target B under the equivalence relation

A ^{t} B ∼ A′ ^{t′} B iff there is an iso A ^{i} A′.

We will introduce the notion of τ-categories (fully treated in [23]) in order to obtain a notion of canonical representatives of subobjects.

The basic notions of indexed categories required here are introduced in the paper.

2 Syntax over a categorical signature

2.1 Categorical Signatures and Categorical Formulae

In order to combine constraint information with proof search in uniform systems, we wish to generalize the notion of signature to an arbitrary finite product category.

We begin by defining the notion of a categorical signature and continue with the notion of categorical formulae.

Definition 2.1 A categorical signature is a triple (𝕂, D, B) where 𝕂 is a category with finite products, D a family of arrows in 𝕂 and B a distinguished class of monics in 𝕂 satisfying the following property: the pullback of any m in B along any coterminal arrow in D exists.

Objects in (occurring as sources and targets of) D are sorts, and arrows f : σ ρ of D are called terms of insort σ and outsort ρ. An arrow whose source is the terminal object and whose target is a sort σ is called a constant of sort σ. Members of B are called predicate tokens. The target of a predicate token is its sort.

The maps in D, sometimes called display maps, are a distinguished class of arrows that formalize terms of interest.

When this class of maps is clear from context, we may omit its mention. It will sometimes be useful, for finite sets of predicate tokens, to replace B by a specific sequence of its members.

Predicate tokens are used to build first-order categorical formulae or formula diagrams over the signature.

Definition 2.2 Let (𝕂, D, B) be a categorical signature. A formula diagram P of sort σ over (𝕂, D, B) is a labelled diagram with a distinguished object σ of D. For the purposes of this definition, such diagrams will be displayed as a bubble over a distinguished sort, as follows

σ P

to remind the reader that they are not necessarily individual arrows. The class F (𝕂, D, B) of formula diagrams over (𝕂, D, B) is given by the following inductive definition.

• For any object σ in K, the identity arrow σ = σ is a formula diagram of sort σ, called ⊤_{σ}.

• The pullback along an arrow σ ^{t} ρ in D of any predicate token of sort ρ is a formula diagram of sort σ. It is (a fortiori) monic, and is called an atomic formula diagram.

• If P and Q are formula diagrams of sort σ (shown on the left), then so is the labelled diagram P ⊛ Q (shown on the right) below,

σ P  σ Q  σ P  Q ⊛

where ∗ is either the label ⇒, or ∨ or ∧.

• If P is a formula diagram of sort ρ and ρ ^{f} σ is an arrow in D, then the diagrams

[figure: ρ; P; σ; f, ∃; ρ; P; f, ∀; σ]

are formula diagrams of sort σ, referred to as ∃_{f}P and ∀_{f}P respectively.

• If P is a formula diagram of sort ρ and if α ^{t} ρ is an arrow in D, then the formal pullback (t)^{#}(P) is a formula diagram of sort σ, given by the following inductive definition:

1. if A is a predicate token then (t)^{#}(A) is just the normal pullback of A along t in 𝕂.

2. (t)^{#}(P ⊛ Q) = (t)^{#}(P) ⊛ (t)^{#}(Q)

3. (t)^{#}(∃_{f}P) = ∃_{g}((u)^{#}(P)) where the bottom square in the following diagram is a (labelled) pullback:

[figure: η; u^{#}P; α; g, ∃; ρ; P; f, ∃; σ; t; u]

In other words, to pull back (along t) a quantified diagram ∃_{f}P, first pull back the quantifier arrow f along t, creating the pair of arrows u, g shown, then pull back the formula P along u, and quantify the resulting formula diagram along g (by adding the label ∃ to g).

The ∀ definition is similar.

The formula diagram (t)^{#}(P) will also be denoted P (t), and called the t-instantiation of the formula diagram P.

If the quantifying arrow ρ ^{f} σ in ∀_{f}P or ∃_{f}P is of the form σ × α ^{π} σ, i.e. a projection out of a product, then the quantifier ∀_{f} is often written ∀_{x:α}, as it coincides with the conventional notion of quantification in logic.

Henceforth, we shall drop the bubble representation of formula diagrams and display them as monics over a distinguished sort.

Definition 2.3 (Theories) Let σ be an object of 𝕂. We define a σ-theory to be a set of formula diagrams of the sort σ.

If ρ ^{t} σ is an arrow in 𝕂, and P is a σ-theory, then the formal pullback t^{#}(P) is the ρ-theory obtained by taking the pullback along t of each formula diagram in P.

When it is not necessary to name σ explicitly, we will simply refer to such a set as a theory. We can think of a σ-theory as a labelled diagram consisting of formula diagrams of sort σ all displayed over a single occurrence of the distinguished sort σ with commas as labels in between playing the role of an extra top-level binary connective. As our use of the word set indicates, we do not distinguish between theories displayed in different order, or those with repetitions of formula diagrams.

Remark 2.4 (sort extension) Any formula diagram P over sort ρ may be thought of as a formula diagram (π)^{#}(P) over (the larger) sort ρ × σ by taking its formal pullback (if it exists) along the projection map ρ × σ ^{π} ρ. This extension of sort (denoted π^{#}P or P (π)) which corresponds in logic to the addition of “dummy” variables to a formula, will be used repeatedly and tacitly in our resolution rules and semantics in order to guarantee that a program and a goal always have a common sort.

Definition 2.5 A formula diagram is called ground if its sort is 1, the terminal object. Otherwise it is called open.

Predicate diagrams are, in a sense, variable-free entities. For example, the formula diagram P (f) for ρ ^{f} σ an arrow in 𝕂 and P a predicate (formula diagram) of sort σ corresponds to the formula P (f(x)) in conventional syntactic logic. Only the sort allows us to distinguish between open and ground formulas. Ground predicates play no special role in our treatment. This is a fundamental characteristic of categorical logic, and it leads us in a natural way to a non-ground semantics of logic programming.

2.2 τ-Categories

In developing a categorical notion of syntax, one wishes to interpret sorts and formulas in the category in such a manner as to represent them with particular objects or arrows of the category. In general, however, categorical constructions are only defined up to isomorphism, so natural proof-theoretic operations, such as instantiation, may involve arbitrary choices at each step. Such a problem would occur, for example, in the interpretation of product sorts since n-ary products in a category are defined only up to isomorphism, and so are not strictly associative (the associativity map is only required to be an isomorphism instead of an identity).

As a solution, one may work in τ-categories. τ-categories are a special class of finite-product categories in which there is a canonical cartesian structure. This canonical structure allows one to make non-arbitrary choices when interpreting sorts, formulas and proofs. In such categories, since products are strictly associative, there is a unique, canonical n-fold product. There is also a unique terminator, as well as a canonical set of monic arrows which are closed under (canonical) pullbacks.

τ-categories are described in detail in [23], but we present here the relevant definitions and properties for use in categorical syntax. Note, however, that 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 τ-categories is not especially restrictive since every small finite limit category is equivalent to a τ-category ([23]), thus one can always take a finite-limit completion of a base category and pass to the equivalent τ-category.

We begin by defining the notion of table, which is a certain family of arrows with a common source. One should think of a table (up to isomorphism) as denoting a relation. Any table is equivalent to a monic composed with a product diagram.

Definition 2.6 A table is an object T together 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}⟩.

Or diagramatically, a table is given by:

T
[figure: x_{1}; x_{2}; x_{n}]
A_{1}  A_{2}  ⋯  A_{n}

The following two technical definitions are necessary for the definition of τ-categories. The first defines what it means for an arrow to not contribute to the monic nature of the table and the second defines a composition of tables.

Definition 2.7 Given a table ⟨T; x_{1}, …, x_{n}⟩ we say that x_{j} is a short column if for every f, g : X → T such that fx_{j} ≠ gx_{j} there exists i < j such that fx_{i} ≠ gx_{i}.

In other words, ⟨x_{1}, …, x_{j−1}⟩ is as monic as ⟨x_{1}, …, x_{j−1}, x_{j}⟩. 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.8 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.9 A τ-category is a category with all finite products and a distinguished class of tables, denoted τ, such that

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

2. ⟨T; id_{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}⟩ ∈ τ

Axiom 1 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; π_{l}, π_{r}⟩ is canonical if it is a τ-table. Similarly, a pullback diagram

[figure: P; p_{2}; B; A; p_{1}; C]

is canonical if ⟨P; p_{1}, p_{2}⟩ ∈ τ. These axioms also imply that the category has a unique terminal object.

In addition to guaranteeing a canonical choice of limits, these axioms ensure that those canonical limits satisfy several important properties ([23]).

Lemma 2.10

1. Canonical products are strictly associative.

2. The terminator is strictly a two-sided unit.

3. If each square in

[figure: A; B; C; D; E; F]

is a canonical pullback then so is the rectangle.

The following properties are essential for formalizing syntax in a canonical way in a τ-category.

Lemma 2.11

1. The canonical pullback of a τ-monic along any arrow is a τ-monic.

2. The canonical pullback of a left projection from a τ-product table along any arrow is also a left projection from a τ-product table.

In other words, the canonical nature of formula diagrams is preserved under canonical pullbacks. For the remainder of the paper we assume all syntax is defined over a τ-category.

2.3 Interpreting Conventional Logical Structure over a Category

The notion of categorical signature given in definition 2.1, generalizes the conventional notion of a first-order, many-sorted language. By combining this notion with that of τ-categories, or more precisely, by requiring that a categorical signature (𝕂, D, B) consist of a τ-category 𝕂 and a distinguished class B of τ-monics, we may give a canonical generalization of a language, as well as a strict interpretation of conventional logic into this τ-categorical signature.

Definition 2.12 Let (𝕂, D, B) be a τ-categorical signature. A pre-interpretation of the language L into (𝕂, D, B) is a function M : L → 𝕂 such that:

1. for every sort σ in L, M(σ) is an object of D

2. for every operation symbol f in Lof input sort σ_{1}σ_{2} ⋯ σ_{n}, and of output sort ρ,

M(f) : M(σ⃗) → M(ρ)

is a morphism in D. Constants are to be thought of as functions of arity 0, and so for each constant c of sort ρ, M(c) : 1 → M(ρ) is a morphism in D.

3. M maps each relation symbol R of sort σ of L to a morphism M(R) M(σ) of B.

M(σ⃗) denotes the canonical product M(σ_{1}) × ⋯ × M(σ_{n}).

2.3.1 Interpretation of the Terms and Formulae

Given a (𝕂, D, B)-pre-interpretation M defining the symbols of the language L in the category 𝕂, we may then interpret the terms inductively as described below. The definition describes each term as an arrow in 𝕂 relative to a sequence of distinct variables containing all of the free variables in the term. M is called an interpretation if the image of every term lies in the class of display maps D.

Let x⃗ = (x_{1}, …, x_{m}) be a sequence of distinct variables of sorts ρ_{1}, ρ_{2}, …, ρ_{m} (respectively). In order to remind us which variable sequence is under consideration we will adopt the convention of denoting by M(x⃗) the product M(ρ_{1}) × ⋯ × M(ρ_{m}) in 𝕂. Thus, we will drop specific reference to the sorts of the x_{i}’s unless needed in a particular instance.

Definition 2.13 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 𝕂 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_{n} If each t_{i} is of sort σ_{i}, then Mx⃗(ft_{1} ⋯ t_{n}) is defined as the following composition:

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

Definition 2.14 Let (𝕂, D, B) be a categorical signature, and M an interpretation of the language L into (𝕂, D, B). We say M is surjective if every object of 𝕂 is the image of a sort in L, full if every arrow in 𝕂 between images of sorts in L is the image of some term in L, and faithful if distinct terms are interpreted as distinct arrows.

The interpretation M also extends to a (partial) mapping from L-formulas to formula diagrams over (𝕂, D, B).

Definition 2.15 Let A be an L-formula of sort σ with free variables among x⃗ = (x_{1}, …, x_{m}). Then Mx⃗(A) is the following diagram in F (𝕂, D, B):

\underline{A = B(t) for B a relation symbol in L:} Mx⃗(A) is the pullback (t)^{#}(M(B)) provided it exists.

\underline{A = B ∗ C:} Mx⃗(A) is the formula diagram Mx⃗(B) ⊛ Mx⃗(C). (∗ ∈ \{∨, ∧ ⇒\}).

\underline{A = ∃_{y:ρ}B} Mx⃗(A) = ∃_{π_{ℓ}}M_{x⃗·y}(B).

\underline{A = ∀_{y:ρ}B} Mx⃗(A) = ∀_{π_{ℓ}}M_{x⃗·y}(B).

where · denotes concatenation and π_{ℓ} is the left projection

M(σ) × M(ρ) M(σ).

Notice that since M(B) is a member of Π, and so a τ-monic, Mx⃗(B(t)) will also be a τ-monic by lemma 2.11.

2.3.2 Notation and Shared Data

In the preceding section we saw how conventional syntactic formulae are interpreted into a categorical signature and, in particular, how variables are replaced by projection arrows. It is important to note therefore how sharing of variables is captured in such a framework. It is formalized entirely through projections and sort information. If P is a predicate token, the diagrams P (x) and P (y) are indistinguishable, since they are both pullbacks of the predicate P along the identity arrow. However, in any context in which the two formulas appear together, such as their conjunction, sort information will tell us whether the arguments are shared or distinct. In such a case, if x and y are distinct, the sorts of P (x) and P (y) must be extended to σ × σ along the left and right projections into σ since the sort information must name all the free variables included in a discussion. If we wish to combine P (x) and P (x) (or P (x) and Q(x) for any other predicate Q of sort σ) we will retain the original sort σ. The following diagram illustrates the way the two notions are captured in formula diagrams, where π_{o} and π_{1} are the left and right projections along σ × σ σ respectively.

P (id)  ⊛  Q(id)  P (π_{o})  ⊛  Q(π_{1})
[figure]
σ  σ × σ

P (x) ∗ Q(x)  P (x) ∗ Q(y)

2.4 Substitution

Let θ = {x_{1} := t_{1}, …, x_{n} := t_{n}} be a substitution for the distinct variables in the sequence x⃗ = (x_{1}, …, x_{n}). 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 𝕂 to be the morphism:

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

The following lemma illustrates the fact that a categorical substitution may be applied to the interpretation of a term via ordinary composition of arrows in 𝕂.

Lemma 2.16 Assume θ, x⃗ and y⃗ are as described above. Then My⃗(sθ) = Mx⃗(s) ∘ Θy⃗.

The application of a substitution to the interpretation of a formula may now be defined to be the result of taking a (canonical) pullback. As in the definition of formulae, this resulting arrow will automatically be a τ-monic arrow. This definition is then shown to satisfy an intuitive notion of substitution for formulas. Explicitly, for atomic formulae, the application of the substitution via pullback should result in the same arrow as that given by the interpretation of the previously instantiated formula.

Definition 2.17 Assume θ and y⃗ are as described above. Given an atomic formula φ, define My⃗ (φθ) to be the arrow q in the following canonical pullback:

[figure: My⃗(φθ); Mx⃗(φ); M(y⃗); q; Θy⃗; M(x⃗)]

Lemma 2.18 For φ:= Pu_{1} ⋯ u_{k}, My⃗(φθ) = My⃗(P (u_{1}θ) ⋯ (u_{k}θ)).

3 Horn Logic Programming Categories

3.1 Generic Predicates and unordered goals

Any distinguished family of predicates (monics) can play the role of predicates in a logic program, but such a collection should be carefully chosen. If the predicates are not stable under pullbacks of arrows designated as program terms (the display maps D) then certain instances may not even exist in the syntax, which is a rather unusual form of failure for a logic program query.

More importantly, in logic programming, atomic queries A(t) should be true or false in relation to the ambient program. Unless one wishes to constrain it in advance of its use in any program a program predicate A should not be true at any instance A(t) in the syntactic category.

For example, consider the program

  conn(X,X).
  conn(X,Y) :- edge(X,Z),conn(Z,Y).
  edge(a,b).
  edge(a,c).

A category of predicates should supply the syntactic raw material of the program: predicate tokens B = {conn, edge} of some sort σ × σ, and a subcategory of display maps containing 1 ^{a} σ, 1 ^{b} σ, 1 ^{c} σ and closed under products (so that the predicates, e.g. conn(X, a) may be formed). It should not make any instance (pullback) of the predicate true (i.e. an isomorphism onto its sort), since no predicate should evaluate to true a priori, that is to say, prior to execution of the program.

We thus seek a notion of generic or freely adjoined predicate. We will now make this idea precise, and show how to construct them.

Definition 3.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 ℂ.

We say X is a generic subobject of b with respect to the (display) maps D if

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

• No such pullback is an isomorphism.

Definition 3.2 (The category ℂ [X_{1}, …, X_{n}]) 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: 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 ℂ.

We also call ℂ [X_{1}, …, X_{n}]the category of generic predicates of sort b⃗.

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.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 and faithful embedding.

Functoriality, faithfulness and fullness is obvious from the definition of morphism, composition and equality in ℂ [X_{1}, …, X_{n}]. 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 3.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 3.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}

The following theorem says that the X_{i} are generic with respect to the class of (images of) arrows from ℂ, which thus comprise a collection of display maps for ℂ [X_{1}, …, X_{n}].

Theorem 3.6 The indeterminate subobjects X_{i} of b_{i} are generic with respect to the maps in the image of Hom_{ℂ}( , b_{i}) under ℂ ^{ι} ℂ [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 ∈ ∅.

□

Definition 3.7 An object ⟨A, H⟩ is atomic if H is of the form tJ^{i} for a basis vector J^{i} (see 3.5), and some arrow A _{t} σ_{i}. That is to say, H is the formula X_{i}(t).

We will discuss the lifting of τ-structure from ℂ to ℂ [X_{1}, …, X_{n}] below. But first, there is a more elementary notion of canonical subobject worth identifying in ℂ [X_{1}, …, X_{n}].

Definition 3.8 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}.

3.1.1 Generic Predicate Diagrams

A certain family of formulas will play an important role here: the class of canonical or generic formula diagrams over a base category ℂ, that is to say, those built up from generic predicates. Spelling it out, we mean the formula diagrams over the signature (𝕂, D, B) where 𝕂 is ℂ [X_{1}, …, X_{n}], D is the image of the category ℂ in ℂ [X_{1}, …, X_{n}] and B is the sequence X_{1}, …, X_{n} of generic predicate tokens corresponding to some sort b⃗. We simplify notation for this class.

Definition 3.9 Let ℂ be a finite product category and b = b_{1}, …, b_{n} a sequence of sorts from ℂ. By the b-signature ℂ [X_{1}, …, X_{n}] or the b-signature ℂ we mean the signature (ℂ [X_{1}, …, X_{n}], ℂ , ⟨X_{1}, …, X_{n}⟩) of canonical formula diagrams, where each X_{i} is a generic predicate token of sort b_{i}. The class of canonical formula diagrams over the b-signature ℂ [X_{1}, …, X_{n}] is denoted F (ℂ [X_{1}, …, X_{n}]).

When b, the sequence of sorts of generic predicate tokens is clear from context its mention may be omitted.

Observe that every object ⟨A, S⟩ of ℂ [X_{1}, …, X_{n}] is the source of a canonical subobject of its “sort object” ⟨A,∅⟩. This allows us to define a natural strict indexed structure for ℂ [X_{1}, …, X_{n}] over ℂ, which we then lift to predicate diagrams.

3.2 Predicates via indexed categories

The dependency of predicates on sorts (and later in this paper on underlying programs or states) is nicely captured and generalized via indexed category structure. Indexed categories resolve logic and logic programing structure in a clean way into a (vertical) basic logical component (the structure in the fibers) and the (horizontal) predicate logic and substitution component, which, as we shall soon see, is a special case of state change in logic programming.

Indexed categories are a natural categorical formalization of the notion of families of sets indexed by another. Predicates of a given sort σ from a base category ℂ can be viewed as objects of a category over that sort, called the fiber over σ. Arrows between sorts (e.g. substitutions) give rise to induced (co-variant or contravariant) functors between the resulting fibers (such as pullbacks of predicates from one sort to another in the preceding section). Logic programming may be developed in the completely general setting of arbitrary indexed monoidal categories[2, 3]. We will not have need of this generality here, although it is briefly discussed and compared with our approach. It has been treated in [59, 12] for the special case of a base category of sorts. We will consider specific indexed categories over much more general base categories capturing operational and state information, which has not yet been considered in the literature.

We will show that our generic predicate construction is closely related to this general formulation, however, via the so-called Grothendieck construction.

[figure: ℂ; σ; f; P f; P σ; ρ; P ρ]

Definition 3.10 A strict indexed ℂ -category (or just a ℂ -category) is a functor

ℂ ^{P} ℂAT .

An indexed functor from one ℂ -category p to another q is just a natural transformation from p to q. The category P σ associated to the object σ of the base category ℂ is called the fiber at σ. To each arrow σ ^{f} ρ between objects in the base category, P associates a functor P f between the fibers.

Indexed categories may be covariant or contravariant. The figure illustrates a contravariant indexed category. Indexed functors may also change the base category, but we will not have need of this generality here.

If the word strict is dropped, the functoriality condition on p is relaxed: it need only be a pseudofunctor preserving identity and composition up to equivalence rather than on the nose. Pseudofunctoriality arises naturally in the absence of the kind of canonical structure imposed in our work, for example with arbitrary pullbacks.

We denote the action of q on objects σ by q(σ), and on arrows σ ^{t} ρ, by q_{t}.

Definition 3.11 Let ℂ be a category and b = b_{1}, …, b_{n} a sequence of objects of ℂ. Then

Πb : ℂ ℂ𝔸𝕋,

the indexed cartesian category of generic predicates with sort b, is defined as follows. Each fiber Πb(σ) has objects the members of

F inP ow(ℂ (σ, b_{1})) × ⋯ F inP ow(ℂ (σ, b_{n}))

where F inP ow denotes the finite power set, i.e. sequences S = S_{1}, …, S_{n} where each S_{i} is a finite set of arrows from σ to b_{i}, further endowed with the poset operation of pointwise containment: S ≤ T iff for all i S_{i} ⊆ T_{i}. To indicate the fiber in question, we will sometimes write objects as pairs ⟨σ, S⟩. The action of Πb on arrows is given by

Πb(σ ^{f} ρ) = f^{#} : Πb(ρ) Πb(σ)

Notice that the pullback operation referred to by f^{#} maps ⟨ρ, S⟩ ^{id_{ρ}} ⟨ρ,∅⟩ to ⟨σ, fS⟩ ^{id_{σ}} ⟨σ,∅⟩. Thus (fg)^{#} is precisely g^{#}f^{#} on the nose, so the indexed category is strict.

Finally, observe that each fiber Πb(σ) is closed under finite unions and intersections, hence Πb is finitely complete and co-complete as an indexed category, i.e. in particular, it is cartesian, which is all we will need to make use of in this section.

In the preceding section, we saw how how to define predicates which are generic, i.e. whose meaning is not yet constrained (and will subsequently be defined by a program). We now compare this category with a notion of generalized category of predicates introduced in a related (but somewhat different) form by Hermida [27] and Asperti-Corradini [12].

3.3 From Formula Diagrams to Generalized Formulas

Definition 3.12 A (generalized) category of predicates over a base category ℂ is any indexed category q over ℂ. An object in q(σ) is called a generalized predicate of sort σ. We say the category of predicates is [FP,cartesian] if each fiber is, respectively, a finite product or a cartesian category. Let b = b_{1}, …, b_{n} be a finite sequence of objects of ℂ. Then a q-signature of sort b is a sequence of objects d= d_{1}, …, d_{n} with d_{i} ∈ |q(b_{i})|. A signature-preserving morphism of predicate categories is just a natural transformation of indexed categories sending the sequence of distinguished objects in one signature to the other. We call an object of the form q_{t}(d), where d is a component of d in |q(b)| and t is an arrow in ℂ with target b, an atomic formula over the q-signature d. We will always assume here that our categories of predicates are at least FP indexed categories. This assumption may be replaced by a more general monoidal structure (cf. [12]).

The generic predicate category Πb comes with a canonical signature over b, namely the sequence of generic objects J^{1}, ⋯, J^{n} (where each J^{i} is the vector of definition 3.5 above) in Πb(b_{i}).

Lemma 3.13 Let ℂ be an FP category, q a cartesian category of predicates, b = b_{1}, …, b_{n} a finite sequence of objects of ℂ, and d = d_{1}, …, d_{n} a q-signature of sort b. Then there is a cartesian, signature-preserving morphism

Πb ^{φ} q

unique up to isomorphism.

Thus Πb is free in the category of cartesian predicate categories with signatures over b.

Proof. Define φ_{σ}(S) = lim{q_{t}(d_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n}. See comments in the proof of theorem 3.18 below. □

Finally, we observe that our original definition of the generic predicate category ℂ [X_{1}, …, X_{n}] can be recovered from the indexed formulation Πb just given via a well-known canonical operation: the so-called Grothendieck construction of a fibration from an indexed category, presented in e.g. [6], and sketched in the appendix.

Let G(ℂ , Πb) be the source of the Grothendieck fibration induced by the indexed category Πb, i.e. the category with

\underline{objects}: pairs ⟨σ, S⟩ with σ ∈ |ℂ | and S ∈ |Πb(σ)| and

\underline{arrows}: ⟨σ, S⟩ ^{⟨θ,f⟩} ⟨ρ, T ⟩ for each pair σ ^{θ} ρ in ℂ and S ^{f} Πb(θ)(T) an arrow in Πb(σ). Composition of arrows is given by:

⟨σ, S⟩ ^{⟨θ,f⟩} ⟨ρ, T ⟩ ∘ ⟨ρ, T ⟩ ^{⟨ψ,g⟩} ⟨μ, U⟩ = ⟨σ, S⟩ ^{⟨θψ,Πb(θ)(g)⟩} ⟨μ, U⟩

Since each Πb(σ) is a poset, and Πb(θ) is the pullback operation along θ, which is defined by left composition with θ, this reduces to the following definition.

⟨σ, S⟩ ^{⟨θ,≤⟩} ⟨ρ, T ⟩

is an arrow in t G(ℂ , Πb) whenever S ≤ θT.

This is precisely the category ℂ [X_{1}, …, X_{n}].

We now generalize the notion of formula diagrams, defined in subsection 2.1, along the same lines as definition 3.12. We will mainly be interested in the sequel in goals and programs built from formula diagrams, i.e. from the free instance of this definition, and will not make extensive use of this generality here. The interested reader can supply the appropriate notions of resolution and unification, or read about them in [2, 3].

Definition 3.14 Let ℂ be a finite-product category and b = b_{1}, …, b_{n} a finite sequence of objects of ℂ. A generalized first-order category of formulas (FOCF) 𝔽 over ℂ with signature d = d_{1}, …, d_{n} of sort b is a predicate category over ℂ with signature d = d_{1}, …, d_{n} of sort b (see def. 3.12) with the following additional structure:

1. Every fiber 𝔽(σ) has an object ⊤_{σ}.

2. there are ℂ -indexed covariant bi-functors

∨, ∧ : 𝔽 × 𝔽 𝔽

and a bi-functor

⇒: 𝔽 × 𝔽 𝔽

contravariant in its first coordinate and covariant in its second.

3. for every σ ^{f} ρ ∈ ℂ there are functors

∃_{f}, ∀_{f} : 𝔽(σ) 𝔽(ρ)

We have not imposed the requirement that an FOCF be a hyperdoctrine (that existential and universal quantification along f be left and right adjoints to 𝔽_{f} satisfying Beck and Frobenius conditions, see e.g. [65]) because we want categories of formulas to be a more primitive structural notion, and let the semantics do the extra work. The theory could be developed using both sytactic and semantic hyperdoctrines with more notation but essentially along the same lines. This approach to logic programming is taken up in [2, 3].

We observe that formula diagrams can be viewed as a discrete FOCF with 𝔽(σ) the set of formula diagrams of sort σ, 𝔽(σ ^{θ} ρ) the generalized pullback operation, and with ∨, ∧, ⇒, ∃_{f}, ∀_{f} the operations that form compound formula diagrams from their components.

Now we define a “canonical intersection” functor for the indexed category Πb:

Definition 3.15 Let ∩ : Πb × Πb Πb be defined by ⟨σ, S⟩ ∩_{σ} ⟨σ, T ⟩ = ⟨σ, S ∪ T ⟩. It is easy to see that that ∩ commutes with pullback, i.e. is a morphism of indexed categories.

The reader can check that indexed canonical intersections of canonical subobjects of the same sort yield representatives of the ordinary intersection on the subobject lattices. That is to say ⟨σ, S⟩ ∩_{σ} ⟨σ, T ⟩ is a representative of the subobject, in ℂ [X_{1}, …, X_{n}], of [⟨σ, S⟩] ∩ [⟨σ, T ⟩], where brackets denote the subobject equivalence class, and ∩ the intersection obtained by pulling back the following diagram.

⟨σ, S⟩  ⟨σ, T ⟩
[figure: id_{A}; id_{A}]
⟨σ,∅⟩

We now return to the fibration ℂ [X_{1}, …, X_{n}] and establish some key properties we will need when we study semantics.

τ-structure

We have defined a notion of canonical subobject for ℂ [X_{1}, …, X_{n}] that is independent of any τstructure on ℂ. It is natural to ask if, in the presence of such structure, ℂ [X_{1}, …, X_{n}] inherits it, and if it yields the same notion of canonical subobject and intersection. It does.

Theorem 3.16 ℂ [X_{1}, …, X_{n}] inherits τ-structure from ℂ via the forgetful functor U : ℂ [X_{1}, …, X_{n}] ℂ, adjoint to the full and faithful ι of theorem 3.3.

Proof. We may define τ_{ℂ[X_{1},...,X_{n}]} as the collection of all tables whose image under U is in τ_{ℂ}. It is straightforward to verify that this definition satisfies the axioms of a τ-category. □

Observe that the image under U of any canonical subobject ⟨σ, S⟩ ^{id_{A}} ⟨σ,∅⟩ is A =^{id} A, which is in τ_{ℂ} by axiom 2 of the definition 2.9 of τ-categories. Thus our canonical subobjects are τ-canonical, and our canonical intersections are τ-canonical pullbacks.

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 3.17 Every object ⟨σ, 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}) = ⟨σ, tJ^{i}⟩ = ⟨σ, ∅ ⋯ ∅ \underbrace{\{t\}}_{i} ∅ ⋯ ∅⟩.

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

Theorem 3.18 (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⃗(⟨σ, S⟩) = \underleftarrow{lim}\{F (t)^{#}(B_{i}) : t ∈ S_{i}, 1 ≤ i ≤ n\}. The universal

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

targeted 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 ⟨σ, S⟩ ^{θ} F ⟨σ′, S′⟩ which is the value of F (⟨σ, S⟩ ^{f} ⟨σ′, 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 3.19 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.

3.3.1 Unordered Goals

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

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

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

We will be considering a more general definition of goals in this paper, given by certain formula diagrams. But it is worth noting that an approximate notion is already present in the category ℂ [X_{1}, …, X_{n}] whose objects are effectively unordered goals. By the representation lemma, above, objects ⟨σ, S⟩ are intersections

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

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 3.18. Since the S_{i} are sets, they cannot capture order or repititions of atoms within goals. Thus, this category does not have enough structure to give an account of a deterministic proof theory, or of an operational semantics sensitive to e.g. goal order or selection rules (such as those studied by [36]), but enough to give a standard interpretation along the lines of the Kowalski-Van Emden T_{P} -semantics.

Definition 3.20 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 a functor extending the Yoneda embedding on ℂ, assigning to each X_{i} some canonical subobject B_{i} of ℂ ( , b_{i}) as in corollary 3.19. In other words, an interpretation is a functor

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

• agreeing with the Yoneda embedding on ℂ, and

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

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

We let Iℂ ; X⃗ denote the set of interpretations for a given sequence X⃗ = X_{1}, …, X_{n} of generic predicates. When ℂ or X⃗ are clear from context, we will drop the sub- and super-scripts.

Note that since interpretations always return canonical subobjects, pointwise set-theoretic containment makes the set of interpretations into a poset ⟨IX⃗, ⊑⟩. It is easily seen that for any two interpretations [[ ]] and [[ ]]′, we have [[ ]] ⊑ [[ ]]′ if and only if for each generic predicate [[X_{i}]] ⊆ [[X_{i}]]′

In a more general formulation of semantics based on theorem (3.18), with no stipulations about canonical structure, we would obtain such a poset by using the induced pointwise order on subobjects. The following lemma is immediate.

Lemma 3.21 The poset of interpretations Iℂ ; X⃗ is a complete lattice with (general) meet and join operations given pointwise, and top and bottom elements [[ ]]^{⊤} and [[ ]]^{⊥} given by

[[X_{i}]]^{⊤} = ℂ ( , b_{i}) =^{id} ℂ ( , b_{i})  (1)
[[X_{i}]]^{⊥} = 0 ¡ ℂ ( , b_{i})  (2)

It is straightforward to define (see [20]), given a Horn-clause program P built from generic predicates described above, a continuous operator on this lattice whose least-fixed point is a categorical analogue of the least Herbrand model for P. This is precisely what we will do with weak Hereditarily Harrop formulas below. We briefly sketch here the results for the Horn case from [20].

Definition 3.22 An interpretation [[ ]] is a model of a Horn clause 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 refer to the empty goal of sort σ by □_{σ}.

Lemma 3.23 (Soundness) Let [[ ]] be a model of program P. Suppose G_{1} and G_{2} are goals, of

sorts α_{1}, α_{2} respectively, and there is a resolution proof G_{1}⇝ ⋯^{θ,c} ⇝G_{2}, where α_{2} ^{θ} α_{1} is the computed answer substitution. 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. To motivate our definition, we briefly review the classical Kowalsi-van Emden semantics [38] of Horn Clause programs, also known as the bottom-up semantics. Associated with a conventional Horn-clause program P consisting of a finite set of first-order clause formulas of the form cl = T l ⇒ h(t), t a vector of terms, there is an operator T_{P} : ℘(B_{P}) ⟶ ℘(B_{P}) where B_{P} is the Herbrand Base, the set of all ground instantiations of predicates over the signature of P, and ℘( ) is the power-set operator. T_{P} is defined as follows:

T_{P} (X) = {Aθ : T l ⇒ A is a clause of P and T lθ ∈ X}.  (3)

It is easily shown that T_{P} is continuous on ⟨℘(B_{P}), ⊆⟩ (commutes with unions of chains) and that its least fixed point is the least term model M_{P} of P, in which a goal is true iff it is derivable in classical logic from P iff it is derivable in minimal intuitionistic logic from P iff it is derivable by SLD-resolution from P. By the Tarski-Knaster theorem this model is a union of a countable chain of finitary approximations M_{P}^{n} of the least term model, hence the term bottom-up semantics. Since the definition of the T_{P} operator resembles resolution in reverse it is easy to show that the least-fixed point of T_{P} (as a singleton model class) is complete with respect to resolution. The remarkable fact is that it is also sound and complete with respect to all of classical deduction, which gives a semantic proof of the fact that the restricted proof search of systems based on resolution (operational proofs in the Miller-Nadathur-Scedrov-Pfenning terminology [46]) does not omit any theorems for the restricted class of Horn Theories and existential goals.

This approach to completeness has had a remarkable success in logic programming: countless extensions of declarative programming to e.g. constraints [30], abstract interpretation [5, 11], Hereditarily Harrop programming [44], higher-order logic [17, 18] build on a similar completeness proof. We take this semantic definition as a foundation for a categorical treatment of uniform logic programming.

A slight change in the presentation of the Kowalski-van Emden semantics is more consistent with the spirit of categorical logic. If we define an interpretation [[ ]] as an operator on formulas (determined by its value on predicate symbols or atoms A) whose value is the set of true instances of its argument, then we may define an operator E_{P} similar to T_{P} above (3), as an operator on interpretations, thus:

E_{P} ( [[ ]])(A) = ⋃{θ : [[T lθ]] = ⊤}

where the union is taken over all clauses T l ⇒ B in the program whose heads B unify via mgu θ with atomic goal A, and where ⊤ denotes the set of all instances. As was shown for the Horn case in [20] this admits a simple generalization in categorical logic.

Program P is now assumed to be a set of Horn formula diagrams over ℂ [X_{1}, …, X_{n}].

Definition 3.24 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}]])  (4)

In [20] 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 3.25 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 [20]

Theorem 3.26 (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} ⇝□

4 Program Syntax

We now present the definitions of two first-order logic programming languages, Horn and Weak Hereditarily Harrop (WHH) formulas, in the context of formula diagrams over a category. We will restrict attention to generic categorical signatures ℂ [X], i.e. where ℂ is an arbitrary τ-category and X a finite set of τ-monics freely adjoined to ℂ. These definitions then give rise to two families of programming languages: Horn(ℂ) and WHH(ℂ), parametrized by the categorical signature.

We recall that uniform programming languages are given by the following data: a set of program formulas P and a set of goal formulas G recursively interdefined, as well as a notion of operational derivation ⊢_{o} of sequents P ⊢_{o} G where P is a finite subset of P and G ∈ G. The sets P and G for Horn(ℂ) and WHH(ℂ) are defined below. The proof theory will be discussed in section 4.3.

In each of the cases, formula will mean formula diagram over the categorical signature ℂ [X]. In particular atomic formulas will be of the form A = (u)^{#}(X_{i}) for some X_{i} ∈ X. ⊤_{α} will mean the identity α = α for any object α.

Definition 4.1

• Horn(ℂ) program formulae D and goal formulae G over a categorical signature are given by:

G ::= ⊤ | A | G ∧ G | G ∨ G
D ::= A | G ⇒ A | D ∧ D | ∀_{x:α}D

• WHH (ℂ) program formulae and goal formulae over a categorical signature are given by:

G ::= ⊤ | A | G ∧ G | G ∨ G | D ⇒ G | ∃_{x:α}D
D ::= A | G ⇒ A | D ∧ D | ∀_{x:α}D

Definition 4.2 A program P is a finite theory consisting of program formulae (necessarily of the same sort). A goal is a goal formula G.

4.1 Uniform Programming Categories

To continue the thread of generalized predicates introduced in subsection 3.3, we briefly present the natural indexed category generalization of the preceding definitions. Once again take a base category ℂ and define a WHH structure to be a triple of ℂ -indexed categories

Goal, Atom, Prog : ℂ ℂ𝔸𝕋

endowed with the following indexed category morphisms:

• ⇒: Goal × Atom Prog

• ∧ : Prog × Prog Prog

• ∧, ∨ : Goal × Goal Goal

• ⟶: Prog × Goal Goal satisfying

1. Atom ⊆ Goal

2. Atom ⊆ Prog Furthermore, for each σ ^{θ} ρ in ℂ, there are functors

1. ∃_{θ} : Goal(σ) Goal(ρ)

2. ∀_{θ} : Prog(σ) Prog(ρ)

Observe that we can easily define a WHH structure using the canonical formula diagrams F (ℂ [X_{1}, …, X_{n}], ℂ , ⟨X_{1}, …, X_{n}⟩), by taking the appropriate goal, atom and program formula diagrams over a given sort for the fibers, and taking the connectives ∨, ∧, ⇒ to be the free diagram constructors introduced in the first section, and, e.g. for σ ^{θ} ρ in ℂ, defining ∃_{θ} : Goal(σ) Goal(ρ) by the action

[figure: σ; P; ⇝; σ; P; θ, ∃; ρ]

4.2 Programs as Sets of Formal Sequents

In order to recapture the familiar notion of program as a set of clauses or formal sequents, with a head and tail, we carry out the translation described below. This translation process yields constituent clauses while cumulatively computing the sort extension that is taking place as quantifiers are removed. The effect of the translation is to replace outermost conjunctions with (finite) sets of formulae, and further translate the formulae by

• removing outer occurences of universal quantification, and

• replacing atoms A by the equivalent clause ⊤ ⇒ A, where ⊤ = ⊤_{σ} has the same sort as the

atom A. We obtain clausal formulae of the form

tl_{cl} ⇒ hd_{cl}(tm_{cl})

accompanied by a sort-extending substitution (i.e. a projection). Definition 4.3 We inductively define the translation κ by

• κ(φ, A) = {(φ, ⊤ ⇒ A)}, ⊤ of the same sort as A.

• κ(φ, G ⇒ A) = {(φ, G ⇒ A)}

• κ(φ, P_{1} ∧ P_{2}) = κ(φ, P_{1}) ∪ κ(φ, P_{2})

• κ(φ, ∀_{f:α→β}P) = κ(fφ, P).

It is sometimes convenient to extend κ to sets of program formulae via κ(φ, {P_{i} : i ∈ I}) = ⋃ κ(φ, P_{i}).

If P is a program, a clause, cl, of P is the second component of a member (φ, cl) ∈ κ(P). The pair (φ, cl) will be called an annotated clause. We will write κ(P) as abbreviated notation for κ(id, P).

Each clause yielded by this translation is of the form G ⇒ A, where A is an atomic formula diagram X_{i}(t) with X_{i} a predicate token and t an arrow in ℂ. Given a clause cl, we define the head of the clause, hd_{cl}, to be the token X_{i}, the tail of the clause, tl_{cl}, to be the goal formula G and the head term of the clause, tm_{cl}, to be the arrow t.

κ is a (non-sort-preserving) mapping from the set of program formulae to the power set of the class of all formula diagrams. It induces a partial order on programs (and hence on each sort-indexed fiber), namely by:

P ⊆ P′ iff κ(P) ⊆ κ(P′).

4.3 Resolution

Program computation is carried out via resolution reduction rules. These rules are given as transitions between state vectors: vectors of pairs ⟨P | A⟩ where P is a program, A a goal.

Definition 4.4 Let ℂ be a τ-category and σ an object in ℂ . A σ-state is a pair ⟨P | A⟩_{σ} where P is a program over ℂ of sort σ and A a goal diagram over the same category and sort. When clear from context, mention of the sort σ may be omitted.

A state vector is a finite sequence ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A_{i}⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ of Σ-vectors of the same sort and signature.

State vectors form a natural indexed monoidal category over ℂ. The program and formula of a state can be thought of as a combined diagram over a sort σ (which the reader can think of as labelled by the “connective” |). The projections occurring in the goal formula and program indicate which data (variables) are shared, and which are independent (see subsection 2.3.2). Similarly, state vectors are best thought of as diagrams over a common sort with & as a top-level label.

We define a one-step resolution as a labelled binary relation on state vectors (or, equivalently, a ternary relation on state-vectors×labels×state-vectors, where labels are one of A, ∨_{r}, ∨_{l}, ∧ or a substitution-clause pair). For the Horn case Corradini and Asperti have shown how propositional resolution with respect to an ambient program P can be formalized categorically via the free indexed monoidal category (whose objects are tensors of propositional atoms) induced by the clauses of P as arrows. Resolutions correspond to reversed arrows in this category. Predicate resolution (with unification) can then recovered via the Grothendieck construction applied to this indexed category. We do not study the generalization of this approach to Hereditarily Harrop programming here, as we will not need it for our main results. This approach is used for an axiomatic presentation of resolution in [2, 3].

For the rest of this section we will restrict our attention to quantification along projections, which corresponds, in categorical logic, to conventional quantification with respect to variables. The more general quantification yielded by categorical logic provides a new logic-based way of programming with certain constraints. We return to this point at the end of the section.

Resolution reduction rules:

backchain ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A_{i}⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{θπ,(G⇒A′_{i})}

⟨(π^{#}P_{1})θ | (π^{#}A_{1})θ⟩ & ⋯ & ⟨(π^{#}P_{i})θ | Gθ⟩ & ⋯ & ⟨(π^{#}P_{n})θ | (π^{#}A_{n})θ⟩

for atomic formula diagrams A_{i}, clause diagrams (G ⇒ A′_{i}) and substitution arrows θπ, where

• (π, G ⇒ A′_{i}) ∈ κ(P_{i})

• θ is a unifier of the (sort-extended) atomic goal diagram π^{#}A_{i} and the head A′_{i} of the selected clause.

This rule extends conventional backchaining to categorical logic. The only significant novelty is the lack of a canonical choice of unifiers (such as a most general unifier) in the absence of any constraints on the underlying category. All resulting states appear pulled back along π because the clause G ⇒ A′_{i} whose head is unified with the selected goal A_{i} may result from the peeling off of universal quantifiers in the original program, the effect of which has been to extend the sort of the whole state-vector.

augment ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A ⇒ B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{A}

⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} ∧ A | B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩

instance ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | ∃_{x:α}A_{i}⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{π}

⟨π^{#}P_{1} | π^{#}A_{1}⟩ & ⋯ & ⟨π^{#}P_{i} | A_{i}⟩ & ⋯ & ⟨π^{#}P_{n} | π^{#}A_{n}⟩

where π is the projection σ × α → σ.

This rule effectively replaces an existentially quantified variable in the selected goal by a free one which must now be instantiated by subsequent proof search, and which therefore behaves like a logic variable.

and ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A ∧ B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{∧}

⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A⟩ & ⟨P_{i} | B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩

or-right ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A ∨ B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{∨_{r}}

⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩

or-left ⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A ∨ B⟩ & ⋯ & ⟨P_{n} | A_{n}⟩ ⇝^{∨_{l}}

⟨P_{1} | A_{1}⟩ & ⋯ & ⟨P_{i} | A⟩ & ⋯ & ⟨P_{n} | A_{n}⟩

A null resolution vector is one of the form ⟨P_{1} | ⊤⟩ & ⋯ & ⟨P_{n} | ⊤⟩

Definition 4.5 Let P be a program diagram and G a goal diagram over a category ℂ, that is to say, a categorical signature (ℂ [X_{1}, …, X_{n}], ℂ , ⟨X_{1}, …, X_{n}⟩). Then an SLD derivation is a sequence of reductions starting with (singleton) state vector ⟨P | G⟩.

An operational (SLD) proof is a (finite) sequence of reductions ⟨P | G⟩⇝ ⋯ ⇝ NULL where NULL is a null resolution vector.

Definition 4.6 A computed answer substitution θ is the composition of all the substitutions occurring in the backchain and instance steps of an SLD-proof.

We are now in a position to define operational inference ⊢_{o} based on the notion of resolution. We must be careful, however, to distinguish between the universal role played by open formulas (formulas of non-terminator sort, corresponding to those containing free variables) in a sequent and the existential character they have (as formulas with logic variables) in a resolution sequence

⟨P | G⟩⇝^{θ}⇝ ⋯ ⇝NULL.

The intended meaning of such a derivation is that θ has successfully instantiated an existential query and that any variables remaining free after application of θ (i.e. if the source of θ is other than 1) are universal. Thus, for example, the existence of the derivation above should be equivalent to the assertion P θ ⊢_{o} Gθ.

We now make these observations precise in the following definition.

Definition 4.7 We will say that G is operationally derivable from P and write P ⊢_{o} G iff there is a program P̃ and a formula G̃ such that ⟨P̃ | G̃⟩⇝^{θ}⇝ ⋯ ⇝ NULL, with computed answer substitution θ, P = P̃θ and G = G̃θ.

In the next three lemmas we establish several important properties of ⊢_{o} including a characterization (in lemma 4.9) we will often use: P ⊢_{o} G iff ⟨P | G⟩⇝^{id}⇝ ⋯ ⇝ NULL.

Lemma 4.8 If ⟨P (t) | G(t)⟩⇝^{θ}⇝ ⋯ ⇝ NULL, then ⟨P | G⟩⇝^{(θt)}⇝ ⋯ ⇝ NULL.

Proof. See appendix. □

Lemma 4.9 P ⊢_{o} G iff there is an SLD-proof ⟨P | G⟩⇝^{id}⇝ ⋯ ⇝ NULL with computed answer substitution id.

Proof. See appendix. □

Lemma 4.10 If ⟨P | G⟩⇝^{(θt)}⇝ ⋯ ⇝ NULL, then ⟨P (t) | G(t)⟩⇝^{θ}⇝ ⋯ ⇝ NULL.

Proof. Suppose ⟨P | G⟩⇝^{(θt)}⇝ ⋯ ⇝ NULL. By lemma 4.9 then,

⟨P (θt) | G(θt)⟩⇝^{id}⇝ ⋯ ⇝NULL

which may be rewritten as

⟨(P (t))(θ) | (G(t))(θ)⟩⇝^{id}⇝ ⋯ ⇝NULL

But then, by lemma 4.8,

⟨P (t) | G(t)⟩⇝^{θ}⇝ ⋯ ⇝NULL
□

Remark 4.11 (Syntactic Pullback Property) The combination of Lemmas 4.8 and 4.10 then gives us that

⟨P (t) | G(t)⟩⇝^{θ}⇝ ⋯ ⇝NULL iff ⟨P | G⟩⇝^{(θt)}⇝ ⋯ ⇝NULL

Categorical Quantification In the definition of formula diagrams we have allowed the formation of quantification along arrows ∃_{f}G where G is a formula diagram of sort σ and σ ^{f} ρ is an arrow in ℂ. In conventional logic the meaning of an entailment

Γ(x) ⊢ ∃_{f}G

is that for every x there is a t of the appropriate sort such that

Γ(x) ⊢ G(t) ∧ f(t) = x.

Without introducing equality reasoning directly, we can formalize such a goal using the diagonal predicate Δ ^{δ} ρ × ρ which, e.g. in Set, represents the subset {(r, r) : r ∈ ρ}. The identity of f(t) and x is equivalent to the assertion that the pullback Δ′ along f(t) × id_{ρ} of Δ is an isomorphism. It is straightforward to produce a resolution rule for the goal ∃_{f}G in terms of such a predicate, but subsequent satisfaction of the predicate requires varying the definition of generic predicate to build in this constraint dynamically during execution. The relevant generic predicate definition is taken up in [42] and [37], and will not be further discussed here.

5 Operational Semantics

One of our key aims in proposing a categorical semantics is to give a sufficiently general treatment of the Kowalski-van Emden fixed point semantics of logic programming [38, 67], a remarkably robust approach that has been successfully applied to many variants and extensions of Prolog. Our semantics takes this idea as a cornerstone of a more general treatment of declarative programming. The model theory yielded by approach is also known as bottom-up semantics, since it assigns approximate meanings

[[A]]^{0} ⊆ [[A]]^{1} ⊆ ⋯

to goal predicates A in stages, starting with the empty interpretation. Because of the continuity of the operator used to build these approximations, the canonical least fixed point interpretation of each predicate is the union of these approximations.

The approximate models produced by the bottom-up semantics do not coincide with conventional topos (Kripke) models, and are best understood as model-fragments. In fact the approximate interpretation [[ ]]^{n} is a semantic abstraction of the notion of “derivability in n steps”. As a result, this semantics closely mirrors the resolution process and gives a nice characterization of SLD resolution in terms of inductive definablity of predicates in the semantics.

Since these models do not give rise, even in the colimit, to a bona fide topos model of full firstorder logic, they do not really capture the a priori notion of declarative truth that one associates with the text of a program. For this reason we need to distinguish between the bottom-up semantics, which we will henceforth call the operational interpretation, and conventional topos semantics, developed in section 6. In that section we will reconcile the conventional and operational interpretations, thus justifying the operational semantics in terms of the declarative meaning of the program.

5.1 The Operational Interpretation

In [46], Miller et al. proposed uniform proof systems, sequent systems in which connectives can be given a search-theoretic interpretation, as a fundamental defining characteristic of logic programming systems.

The semantic operator we introduce below captures this uniformity through the interpretation of several of the logical connectives via shifts over a category of states (in this case program-signature pairs). For example, [[A ⇒ B]]_{P} = [[B]]_{P ∧A} defines the meaning of A ⇒ B over P as the meaning of B over P ∧ A. In short, [[ ]] incorporates a search theoretic interpretation of connectives directly into the semantics.

Our operational interpretation extends the Yoneda embedding of the base syntactic category ℂ to an assignment of predicates in the Yoneda Topos to states (goal-program pairs of a given sort) in a way that preserves the ordering of states and which satisfies a number of additional properties.

Let S_{σ} be the set of states of sort σ over ℂ [X_{1}, …, X_{n}], that is to say the set of all triples (G, P, σ), where G is a goal formula diagram and P is a program in K, both of sort σ. Endow S_{σ} with poset structure as follows:

(G, P, σ) ⊆ (G, P′, σ) iff P ⊆ P′

where we recall the order on program formula diagrams is induced by the translation κ of definition 4.3.

Let A_{σ}, A, be the restriction of S_{σ} and S to atomic states (X_{i}(t), P, σ), where X_{i} is a generic subobject in X.

Let 𝕊 be the strict indexed category ℂ ⟶ ℂ𝔸𝕋 given by

• 𝕊(σ) = S_{σ}

• 𝕊(ρ ^{t} σ) = (t)^{#} : 𝕊(σ) ⟶ 𝕊(ρ)

and let 𝕄 be the strict indexed category (also over ℂ) given by

• 𝕄(σ) = Sub(Hom_{ℂ}( , σ))

• 𝕄(ρ ^{t} σ) = [Hom_{ℂ}( , t)]^{#} : Sub(Hom_{ℂ}( , σ)) ⟶ Sub(Hom_{ℂ}( , ρ))

where Sub(Hom_{ℂ}( , σ)) is the complete Heyting algebra of subobjects in Set^{(ℂ)^{o}} of the Yoneda image Hom_{ℂ}( , σ) of σ. Then an operational interpretation is a ℂ -indexed functor

[[ ]] : 𝕊 ⟶ 𝕄.

whose action on triples (U, P, σ) is denoted [[U ]]_{P,σ} (or just [[U ]]_{P} when the sort is clear from context) and satisfying:

1. triples (G, P, σ) ∈ S_{σ} are mapped to monics with target Hom_{ℂ}( , σ)

2. [[⊤]]_{P} is mapped to the identity arrow on Hom_{ℂ}( , σ).

3. [[A ∧ B]]_{P} = [[A]]_{P} ∩ [[B]]_{P}

4. [[A ∨ B]]_{P} = [[A]]_{P} ∪ [[B]]_{P} 5. [[A ⇒ B]]_{P} = [[B]]_{P ∧A}

6. [[∃_{f}A]]_{P} = Im_{[[f ]]} [[A]]_{P (f)}

where Im_{[[f ]]} is the image along f, also denoted ∃_{[[f ]]}.

Observe that, by naturality of [[ ]], for every ρ ^{t} σ in ℂ

[figure: 𝕊(σ); [[ ]]; 𝕄(σ); 𝕊(ρ); 𝕊(t); [[ ]]; 𝕄(ρ); 𝕄(t)]

in other words, [[U(t) ]]_{P (t)} = [Hom_{ℂ}( , t)]^{#} [[U ]]_{P}.

Letting 𝕍 be the indexed category of state vectors, [[ ]] lifts immediately to

[[ ]] : 𝕍 ⟶ 𝕄

via

[[V_{1}&V_{2} ]] = [[V_{1} ]] ∩ [[V_{2} ]]

We note that condition 4 above is what distinguishes operational interpretations from conventional Topos-theoretic (or Kripke) semantics, as it does not interpret implication in terms of a semantic implication operator, thus permitting a considerably simpler notion of model. It effectively carries over into the semantics the search-theoretic character of the implication connective. However, it is interesting to note that it can be built into the very definition of indexed category morphism simply by choosing a more robust base category for indexed structure in which programs play a similar role to sorts, as we show in the next subsection. In effect we show that such treatment of the connective is similar to the treatment of substitution itself as a change-of-fiber, that is to say, a semantically safe change of logical state.

5.2 Indexing over state information

Our choice of notation [[G]]_{P} for the action of [[ ]] on pairs (G, P) suggests indexing over programs (as well as over sorts). We now make this implicit indexed structure precise.

Let Prog_{0} : ℂ ℂ𝔸𝕋 be the indexed category given by:

• Prog_{0}(σ) = {P : P is a program of sort σ} with arrows generated by the identity arrows, and, for each pair of programs P, A, the right-adjoin arrows

P ^{α_{A}} P ∧ A,

and

• Prog_{0}(σ ^{θ} ρ) = Prog_{0}(ρ) ^{θ^{#}} Prog_{0}(σ)

Let GP be the category yielded by the Grothendieck construction G(ℂ , Prog_{0}), namely the category with objects pairs (P, σ) with P a program of sort σ and arrows

(P, σ) ^{(α_{A},θ)} (Q, ρ)

where σ ^{θ} ρ in ℂ and P ^{α_{A}} θ^{#}(Q), whenever θ^{#}(Q) = P ∧ A.

We now define categories of goals and models indexed over GP:

Gℓ, M : GP ⟶ ℂ𝔸𝕋

as follows:

• M(P, σ) = Sub(ℂ ( , σ))

• M[(Q, ρ) ^{(α_{A},θ)} (P, σ)] by pullback along θ

and

• Gℓ(P, σ) = {(G, P, σ) : G is a goal over σ}

• Gℓ(Q, ρ) ^{Gℓ(α_{A},θ)} Gℓ(P, σ) via (G, Q, ρ) ↦ (A ⇒ θ^{#}(G), P, σ), where A ⇒ θ^{#}(G) is an implicative formula diagram.

Then an operational interpretation may be defined as a GP-indexed functor

[[ ]] : Gℓ ⟶ M.

satisfying conditions 1,2,3,5 above, since condition 4 is now guaranteed by naturality of [[ ]] over the base category GP. If we fix the sort σ and vary programs, the commutativity of

[figure: Gℓ(P ∧ A, σ); [[ ]]; M(P ∧ A, σ); Gℓ(P, σ); Gℓ(α_{A}); [[ ]]; M(P, σ); M(α_{A})]

implies [[A ⇒ G]]_{P} = [[G]]_{P ∧A}.

By suitable choice of base category we have eliminated explicit enforcement of a search-theoretic semantic condition 4 corresponding to a uniform proof step. The only remaining conditions are preservation of connectives.

5.3 Soundness

There is a natural partial order on interpretations.

Definition 5.1 [[ ]] ⊆ [[ ]]′ iff for all goal formulae A and every P ∈ K of the same sort, [[A]]_{P} ⊆ [[A]]′_{P}.

It suffices to check the order on atoms.

Lemma 5.2 If [[X_{i}(t) ]]_{P} ⊆ [[X_{i}(t) ]]′_{P} for all atoms X_{i}(t) and all P ∈ K of the same sort, then [[ ]] ⊆ [[ ]]′

Proof. By a straightforward induction on the structure of goals. □

Definition 5.3 We shall say that an interpretation [[ ]] is a model of a program P of sort σ if for every program Q of the same sort which extends P and every clause (π, tl_{cl} ⇒ X_{i}(tm_{cl})) ∈ κ(Q), we have [[tl_{cl}]]_{Q(π)} ⊆ [[X_{i}(tm_{cl}) ]]_{Q(π)}, where we recall σ × α ^{π} σ is the projection from the sort of the clause to that of P.

Proposition 5.4 (Soundness) If [[ ]] is a model of a program P, then for any goal G and any program Q of the same sort which extends P, if Q ⊢_{o} G then [[G]]_{Q} is an isomorphism.

Proof. By induction on length of proof.

Let [[ ]] be a model of P, and let G be a goal and Q a program extending P, both of the same sort, such that Q ⊢_{o} G.

Consider the first resolution rule of the proof of Q ⊢_{o} G, which by lemma 4.9 may be assumed to have computed answer substitution the identity:

Backchain ⟨Q | G⟩ ⇝^{θ_{1}π,(tl_{cl}⇒G̃)} ⟨(π^{#}Q)θ_{1} | tl_{cl}θ_{1}⟩⇝ ⋯ ⇝^{φ} ⇝ NULL

By the induction hypothesis then, [[(tl_{cl}θ_{1})φ]]_{Q} is an isomorphism. But, [[(tl_{cl}θ_{1})φ]]_{Q} ⊆

[[(G̃θ_{1})φ]]_{Q} = [[((π^{#}G)θ_{1})φ]]_{Q} = [[G]]_{Q} which must then also be an isomorphism.

Conjunction ⟨Q | A ∧ B⟩ ⇝^{∧} ⟨Q | A⟩ & ⟨Q | B⟩ ⇝ ⋯ ⇝^{id}⇝ NULL.

By the induction hypothesis then we know that [[A]]_{Q} and [[B]]_{Q} are isomorphisms, as then is [[A ∧ B]]_{Q}.

Disjunction ⟨Q | A_{1} ∨ A_{2}⟩ ⇝^{∨} ⟨Q | A_{i}⟩ ⇝ ⋯ ⇝^{id}⇝ NULL.

By the induction hypothesis then we know that [[A_{i}]]_{Q} is an isomorphism, as then is [[A_{1} ∨ A_{2} ]]_{Q}.

Augment ⟨Q | A ⇒ B⟩ ⇝^{A} ⟨Q ∧ A | B⟩ ⇝ ⋯ ⇝^{id}⇝ NULL.

By the induction hypothesis then, we know that [[A ⇒ B]]_{Q} = [[B]]_{Q∧{A}} is an isomorphism.

Instance ⟨Q | ∃_{x:α}A⟩ ⇝^{π} ⟨(π^{#})Q | A⟩ ⇝ ⋯ ⇝^{⟨id,θ⟩}⇝ NULL. The form ⟨id, θ⟩ of the second computed substitution ψ is dictated by the fact that πψ must be id_{α}. By the induction hypothesis then, we know that [[(⟨id, θ⟩)^{#}A]]_{Q} is an isomorphism, i.e., [[⊤_{α}]] ⊆ ( [[⟨id, θ⟩]])^{#} [[A]]_{Qπ}. Now using the fact that image is left-adjoint to pullback, we have Im_{[[⟨id,θ⟩]]} [[⊤_{α}]] ⊆ [[A]]_{Qπ}. Taking the image along π of both sides, we have [[⊤_{α}]] ⊆ [[∃_{x:σ}A]]_{Q} as we wanted to show.

□

We now show that the pullback property of operational interpretations extends to nonatomic goals.

Lemma 5.5 (Pullback Lemma) Suppose P is a program and A is a goal. Then

[[A(t) ]]_{P (t)} = ( [[t]])^{#}( [[A]]_{P}).

Proof. We argue by induction on the structure of goal diagrams A. The atomic case follows from naturality of [[ ]]. The cases [[(A_{1} ∧ A_{2})(t) ]]_{P (t)} and [[(A_{1} ∨ A_{2})(t) ]]_{P (t)} follow from the fact that pullbacks (which also have left adjoints) commute with intersections and unions. [[(A_{1} ⇒ A_{2})(t) ]]_{P (t)} = [[A_{2}(t) ]]_{P (t)∧{A_{1}(t)}}, which is equal, by induction hypothesis, to ( [[t]])^{#}( [[A_{2} ]]_{P ∧A_{1}}) = ( [[t]])^{#}( [[A_{1} ⇒ A_{2} ]]_{P}).

For the existential case, observe that (t)^{#}(∃_{π}G), or, equivalently, (∃_{π}G)(t) is ∃_{π′}G(t × id).

[figure: β × σ; u^{#}P; β; g, ∃; α × σ; P; f, ∃; α; t; u]

So [[(t)^{#}(∃_{π}G) ]]_{P (t)} = [[∃_{π′}G(t × id) ]]_{P (t)}, which, by definition is Im_{[[π′]]} [[G(t × id) ]]_{P (π′t)} = Im_{[[π′]]} [[G(t × id) ]]_{P (t×idπ)}. By the induction hypothesis, this is Im_{[[π′]]}(( [[t × id]])^{#} [[G]]_{P (π)}). By the Beck-Frobenius condition in Set^{ℂ^{o}}, this is ( [[t]])^{#}(Im_{[[π]]} [[G]]_{P (π)}), which is precisely ( [[t]])^{#} [[∃_{π}G]]_{P}

□

5.4 The Semantic Operator E_{P}: the WHH case

We now give a categorical analogue of the set-theoretic T_{P} operator for WHH formula diagrams without reference to ground terms and which, depending on the category K of programs, leads to different generalizations of the Least Herbrand Universe over arbitrary τ-categories. Recall that we are using the notation Im_{f} for the left-adjoint of the pullback functor f^{#} : Sub(ρ) Sub(σ) along any arrow σ ^{f} ρ, called the image along f, and sometimes denoted ∃_{f} in the literature. The fact that it also has a right adjoint in any topos will be used later.

Definition 5.6 Let [[ ]] be an operational semantics, P a program in K, and X_{i}(t) an atomic goal, both of the same sort. We define

E(P, [[ ]], X_{i}, t) = ⋃_{θtm_{cl} = θπt_{(π,cl)∈κ(P),hd_{cl}=X_{i}}} Im_{[[θπ]]} [[θtl_{cl}]]_{P θπ}

If we restrict attention to closed programs (such as Horn clause programs), the values E(P, [[ ]], X_{i}, t) can be expressed in terms of pullbacks of E(P, [[ ]], X_{i}), given, in turn, by the considerably simpler expression (4) of definition 3.24 However, in the general Hereditarily Harrop case, the presence of free variables in programs requires a more delicate treatment, both in the semantics and the proof theory.

Lemma 5.7 If [[ ]] ⊆ [[ ]]′, then for any indeterminate monic X_{i}, arrow t targeted at the sort of X_{i}, and program P ∈ K of the same sort, E(P, [[ ]], X_{i}, t) ⊆ E(P, [[ ]]′, X_{i}, t)

Proof. By hypothesis we have that [[tl_{cl}]]_{P π} ⊆ [[tl_{cl}]]′_{P π} for each pair (π, cl) ∈ κ(P) such that hd_{cl} = X_{i}. Thus for any unifier θ of πt and tm_{cl}, we also have

Im_{[[θπ]]}( [[θ]])^{#}( [[tl_{cl}]]_{P π}) ⊆ Im_{[[θπ]]}( [[θ]])^{#}( [[tl_{cl}]]′_{P π})

But now the required containment follows directly from elementary properties of unions. □

Proposition 5.8 Let C_{1} ^{r} C_{2} and C_{0} ^{t} C_{2} be arrows in ℂ. If [[t]] factors through Im_{[[r]]}(F) for some subobject F of [[C_{2} ]], then t is an instance of r in ℂ 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{Im_{[[r]]}(F)}; Im_{[[r]]}(F); [[C_{2} ]]; [[t]]]
[figure: F; [[r]]]
[[C_{1} ]]

where eIm_{[[r]]}(F) is an epi-monic image factorization of F [[r]] and each [[C_{i}]] is a representable functor in Set^{ℂ^{o}}, and therefore projective. The projectivity of [[C_{0} ]] implies that the arrow u (which exists by the hypothesis that [[t]] factors through Im_{[[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. □

5.5 The Approximate Interpretations and their Properties

Definition 5.9 The sequence of operational interpretations [[ ]]^{0}, [[ ]]^{1}, …, [[ ]]^{n}, … is given by [[X_{i}(t) ]]_{P}^{0} = the unique map 0 → [[b]] and [[X_{i}(t) ]]_{P}^{n+1} = E(P, [[ ]]^{n}, X_{i}, t) for indeterminate monics X_{i}, where b = sort of X_{i}(t) and P.

Lemma 5.10 [[ ]]^{n} ⊆ [[ ]]^{n+1}.

Proof. It suffices to show that [[X_{i}(t) ]]_{P}^{n} ⊆ [[X_{i}(t) ]]_{P}^{n+1} for each atomic X_{i}(t) and program P which extends P_{o}. In other words, that [[X_{i}(t) ]]_{P}^{n} ⊆ E(P, [[ ]]^{n}, X_{i}, t). We proceed by induction on n. If n = 0, then [[X_{i}(t) ]]_{P}^{0} = the unique map 0 → [[b]]^{0}, where b = sort of X_{i}(t). But then by initiality of 0, there is a map 0 → [[X_{i}(t) ]]_{P}^{1} such that

0  \overline{}[[X_{i}(t) ]]_{P}^{1}
[figure]
b

Now suppose that [[X_{i}(t) ]]_{P}^{k} ⊆ [[X_{i}(t) ]]_{P}^{k+1}, and show that [[X_{i}(t) ]]_{P}^{k+1} ⊆ [[X_{i}(t) ]]_{P}^{k+2}. Since by hypothesis, [[X_{i}(t) ]]_{P}^{k} ⊆ [[X_{i}(t) ]]_{P}^{k+1}, we know by lemma 5.7 that [[X_{i}(t) ]]_{P}^{k+1} = E(P, [[ ]]^{k}, X_{i}, t) ⊆ E(P, [[ ]]^{k+1}, X_{i}, t) = [[X_{i}(t) ]]_{P}^{k+2}. □

We now establish some key properties of the interpretations [[ ]]^{n} and give a useful characterization of the fixed point operator E in terms of equalizers in the topos Set^{(ℂ)^{o}}.

Lemma 5.11 [[X_{i}(tv) ]]_{P (t)}^{n} is an isomorphism iff ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}) is an isomorphism.

Proof. See appendix. □

Corollary 5.12

( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}) = [[X_{i}(tv) ]]_{P (t)}^{n}

Proof. We show that [[X_{i}(tv) ]]_{P (t)}^{n}(α) = ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n})(α) for every object α in ℂ. Let γ be an arrow in ℂ whose source is α and whose target is the source of t.

γ ∈ ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n})(α) iff (γt) ∈ [[X_{i}(v) ]]_{P}^{n} (α)
iff ( [[γt]])^{#}( [[X_{i}(v) ]]_{P}^{n}) is an isomorphism
iff [[X_{i}(γtv) ]]_{P (γt)}^{n} = [[(X_{i}(tv))(γ) ]]_{(P (t))(γ)}^{n} is an isomorphism
iff ( [[γ]])^{#}( [[X_{i}(tv) ]]_{P (t)}^{n}) is an isomorphism
iff γ ∈ [[X_{i}(tv) ]]_{P (t)}^{n}(α)
□

The values of the semantic operator E(P, [[ ]], X_{i}, t) defined above were described in terms of substitutions from the base syntactic category ℂ. We must consider all unifying substitutions, since in arbitrary categorical signatures the existence of mgu’s is not guaranteed. But the Yoneda Topos Set^{(ℂ)^{o}} has equalizers, in terms of which we can give a characterization of the operator E.

Theorem 5.13

E(P, [[ ]], X_{i}, v) = ⋃_{(π, cl) ∈ κ(P_{i})_{hd_{cl}=X_{i}}}{Im_{[[π]]}Imeq( [[πv]], [[_{tm_{cl}}]])(eq( [[πv]], [[tm_{cl}]]))^{#} [[tl_{cl}]]_{P π}}

In the case where most general unifiers exist in ℂ, the equalizers in the formula above are representable.

Proof. See appendix. □

5.6 The Kowalski-van Emden model

We now define a canonical operational interpretation of a logic program, inspired by the Kowalski-van Emden construction [38, 67] of the least Herbrand model. In one form or another, this construction has provided complete operational semantics for a broad class of logic programming languages [29, 64, 48]. One of the aims of this paper is to show that, suitably reformulated as a topos interpretation, it gives a semantics for Weak Hereditarily Harrop programs in the full generality of categorical signatures, with respect to which resolution is complete. After defining the canonical interpretation, we establish some important properties of models and show the interpretation is initial with respect to all models of a program.

Definition 5.14 The Kowalski-van Emden model is defined by letting

[[X_{i}(t) ]]_{P}^{∗} = \underrightarrow{lim}\{ [[X_{i}(t) ]]_{P}^{n} \}

where \underrightarrow{lim}\{ [[X_{i}(t) ]]_{P}^{n} \} is the filtered colimit in Set^{(ℂ)^{o}} of the following diagram of inclusions

[figure: [[X_{i}(t) ]]_{P}^{0}; [[X_{i}(t) ]]_{P}^{1}; ⋯; [[X_{i}(t) ]]_{P}^{k}; ⋯]

Lemma 5.15 [[A]]_{P}^{∗} = \underrightarrow{lim}\{ [[A]]_{P}^{n} \} for all formulae A and programs P ∈ K of the same sort.

Proof. Follows by a straightforward induction on formulae. □

Definition 5.16 An operational interpretation [[ ]] is said to be a pre-fixed point of E at program P if for every atomic goal X_{i}(u) of the same sort as P, and for every program Q of the same sort as P extending P

E(Q, [[ ]], X_{i}, u) ⊆ [[X_{i}(u) ]]_{Q}

and a fixed point of E at P if the containment can be replaced by equality.

Lemma 5.17 If [[ ]] is a fixed point of E at P it is a model of P. If it is a model of P it is a pre-fixed point of E at P.

Proof. Suppose [[ ]] is a fixed point of E at program P of sort σ. Let Q extend P and suppose B ⇒ X_{i}(u) is a clause of Q of sort σ × α (necessarily extending the sort of Q since it has had any possible quantification removed). Then

[[X_{i}(u) ]]_{Q(π)} = ⋃_{(π′, cl) ∈ κ(Q(π))_{hd_{cl}=X_{i}}}{Im_{[[θπ′ ]]}( [[θ]])^{#} [[tl_{cl}]]_{Q(π′π)}}.

Consider the expression in the right hand union corresponding to the clause B(π×id) ⇒ X_{i}((π×id)u) of Q(π) with θ chosen to be the unifier σ × α ^{id_{σ}×δ} σ × α × α where α ^{δ} α × α is the diagonal map, as shown in the following diagram

B(π × id) ⇒ X_{i}((π × id)u)  B ⇒ X_{i}(u)

[figure: σ × α; θ; σ × α × α; π × id; σ × α]

[figure: σ × α; π′, ∀; π; σ; π, ∀]

This expression is

Im_{[[θπ′]]}( [[θ]])^{#} [[B(π × id_{α}) ]]_{Q(π′π)}

which is equal to

( [[θ]])^{#} [[B(π × id_{α}) ]]_{Q((π×id_{α})π)}

since θ(π × id_{α}) = id_{α×σ} = θπ′. This yields, using the pullback property,

( [[θ(π × id_{α}) ]])^{#} [[B]]_{Q(π)}

which is equal to [[B]]_{Q(π)}. This shows [[B]]_{Q(π)} ⊆ [[X_{i}(u) ]]_{Q(π)}. Thus, [[ ]] is a model of P. For the second claim, suppose [[ ]] is a model of P. Then

E(Q, [[ ]], X_{i}, t) = ⋃_{(π, cl) ∈ κ(Q)_{hd_{cl}=X_{i}}} Im_{[[θπ]]}( [[θ]])^{#} [[tl_{cl}]]_{Q(π)}

⊆ ⋃_{(π, cl) ∈ κ(Q)_{hd_{cl}=X_{i}}} Im_{[[θπ]]}( [[θ]])^{#} [[X_{i}(tm_{cl}) ]]_{Q(π)}

where the θ range over all unifiers of X_{i}(πt) and X_{i}(tm_{cl}) of clauses in Q for which hd_{cl} = X_{i}. But then

( [[θ]])^{#} [[X_{i}(tm_{cl}) ]]_{Q(π)} = [[X_{i}(θtm_{cl}) ]]_{Q(θπ)}
= [[X_{i}(θπt) ]]_{Q(θπ)}
= ( [[θπ]])^{#} [[X_{i}(t) ]]_{Q}

So every expression in the definition of E(Q, [[ ]], X_{i}, t) is of the form

Im_{[[θπ]]}( [[θπ]])^{#} [[X_{i}(t) ]]_{Q}

which, since Im_{f}(f)^{#}(A) ⊆ A for any f and subobject A, is always a subobject of [[X_{i}(t) ]]_{Q}. Thus

E(Q, [[ ]], X_{i}, t) ⊆ [[X_{i}(t) ]]_{Q}

as we wanted to show. □

Lemma 5.18 The interpretation [[ ]]^{∗} is a model of P.

Proof. We show that, in fact, E is continuous, that is to say, E preserves colimits of subobject chains:

[[X_{i}(t) ]]_{Q}^{∗} = ⋃_{{(π, cl) ∈ κ(Q) \atop hd_{cl}=X_{i}}}\{Im_{[[π]]}Imeq( [[_{tm_{cl}}]], [[πt]])(eq( [[tm_{cl}]], [[πt]]))^{#}( [[tl_{cl}]]_{Qπ}^{∗})\}

for each atomic formula X_{i}(t) and each program Q of the same sort extending P. This shows that [[ ]]^{∗} is a fixed point of E at P and hence a model of P.

We will let eq_{cl} stand for eq( [[tm_{cl}]], [[πt]]).

First we will show that

[[X_{i}(t) ]]_{Q}^{∗} ⊆ ⋃_{{(π, cl) ∈ κ(Q) \atop hd_{cl}=X_{i}}}\{Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{∗})\}

It suffices then to show that

[[X_{i}(t) ]]_{Q}^{n} ⊆ ⋃_{{(π, cl) ∈ κ(Q) \atop hd_{cl}=X_{i}}}\{Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{∗})\}

By lemma 5.15, [[tl_{cl}]]_{Qπ}^{n−1} ⊆ [[tl_{cl}]]_{Qπ}^{∗} and hence

Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{n−1}) ⊆ Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{∗})

Thus,

[[X_{i}(t) ]]_{Q}^{n} = ⋃_{{(π, cl) ∈ κ(Q) \atop hd_{cl}=X_{i}}}\{Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{n−1})\}

⊆ ⋃_{{(π, cl) ∈ κ(Q) \atop hd_{cl}=X_{i}}}\{Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{∗})\}

Now, for the other direction, it suffices to show that for each pair (π, cl) in κ(Q) such that hd_{cl} = X_{i},

Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#}( [[tl_{cl}]]_{Qπ}^{∗}) ⊆ [[X_{i}(t) ]]_{Q}^{∗}

We know by the definition of [[X_{i}(t) ]]_{Q}^{k+1} that Im_{[[π]]}Im_{eq_{cl}}(eq_{cl})^{#} [[tl_{cl}]]_{Qπ}^{k} ⊆ [[X_{i}(t) ]]_{Q}^{k+1}. So we know that for each k

Im_{eq_{cl}} [[tl_{cl}]]_{Q(π)}^{k} ⊆ (eq_{cl})^{#}( [[π]])^{#} [[X_{i}(t) ]]_{Q}^{k+1}
⊆ (eq_{cl})^{#}( [[π]])^{#} [[X_{i}(t) ]]_{Q}^{∗}

And so, since by lemma 5.15 we know that [[tl_{cl}]]_{Qπ}^{∗} = \underrightarrow{lim}\{ [[tl_{cl}]]_{Qπ}^{k}\}, we may conclude that

(eq_{cl})^{#} [[tl_{cl}]]_{Qπ}^{∗} = (eq_{cl})^{#}\underrightarrow{lim}\{ [[tl_{cl}]]_{Qπ}^{k}\}
= \underrightarrow{lim}\{(eq_{cl})^{#} [[tl_{cl}]]_{Qπ}^{k}\}
⊆ (eq_{cl})^{#}( [[π]])^{#} [[X_{i}(t) ]]_{Q}^{∗}

From which the result follows by elementary properties of adjunctions and unions.

□

Lemma 5.19 The interpretation [[ ]]^{∗} is an initial model of P.

Proof. We must show that for any model [[ ]]′ of P, [[ ]]^{∗} ⊆ [[ ]]′. In particular, it suffices to show by lemma 5.2 that for all atomic formula diagrams X_{i}(t) and programs Q extending P, [[X_{i}(t) ]]_{Q}^{∗} ⊆ [[X_{i}(t) ]]′_{Q}.

We first show by induction on k that for all such X_{i}(t) and Q both of sort σ, and for all k, [[X_{i}(t) ]]_{Q}^{k} ⊆ [[X_{i}(t) ]]′_{Q}. Since [[X_{i}(t) ]]_{Q}^{0} = the unique map 0 → [[σ]], it is clear that [[X_{i}(t) ]]_{Q}^{0} ⊆ [[X_{i}(t) ]]′_{Q}. Now suppose that [[X_{i}(t) ]]_{Q}^{k} ⊆ [[X_{i}(t) ]]′_{Q} for all X_{i}(t) and Q. By Lemma 5.7 and the fact (lemma 5.17) that any model of P is a pre-fixed point of E at P,

[[X_{i}(t) ]]_{Q}^{k+1} = E(Q, [[ ]]^{k}, X_{i}, t) ⊆ E(Q, [[ ]]′, X_{i}, t) ⊆ [[X_{i}(t) ]]′_{Q}

It now follows by the definition of [[ ]]^{∗} that [[X_{i}(t) ]]_{Q}^{∗} = \underrightarrow{lim}\{ [[X_{i}(t) ]]_{Q}^{n}\} ⊆ [[X_{i}(t) ]]′_{Q}. □

5.7 Completeness

We now establish completeness of our operational interpretation by showing that every goal true in the Kowalski-van Emden model of a program is derivable from the program by resolution. We first show that goals valid in the interpretation are valid in some finite approximation using elementary properties of the Yoneda embedding. We also show that in the atomic case such goals are admitted, i.e. are an instance of the head of some clause of the program. Finally we show that goals valid in some finite approximation are derivable by constructing a resolution proof, the first step of which is follows from admittance.

Lemma 5.20 Let G be a goal formula and P ∈ K a program, both of sort σ. If [[G]]_{P}^{∗} is an isomorphism, then for some n, [[G]]_{P}^{n} is an isomorphism.

Proof. We proceed by induction on formulae.

G atomic Suppose [[G]]_{P}^{∗} = [[X_{i}(t) ]]_{P}^{∗} is an isomorphism. Then the identity on [[σ]] factors through \underrightarrow{lim}\{ [[X_{i}(t) ]]_{P}^{n} \}. By coprimeness of [[σ]] it factors through some [[X_{i}(t) ]]_{P}^{n}, which is therefore an isomorphism.

IH Now suppose that the result holds for every program P and all simpler formulae.

G = A_{1}∧ A_{2} Suppose [[A_{1} ∧ A_{2} ]]_{P}^{∗} = [[A_{1} ]]_{P}^{∗} ∩ [[A_{2} ]]_{P}^{∗} is an isomorphism. Then both [[A_{1} ]]_{P}^{∗} and [[A_{2} ]]_{P}^{∗} are isomorphisms. By the induction hypothesis, there exist some n and m such that [[A_{1} ]]_{P}^{n} and [[A_{2} ]]_{P}^{m} are isomorphisms. But then by lemma 5.10, [[A_{1} ∧ A_{2} ]]_{P}^{max(n,m)} is an isomorphism.

G = A_{1}∨ A_{2} Suppose [[A_{1} ∨ A_{2} ]]_{P}^{∗} = [[A_{1} ]]_{P}^{∗} ∪ [[A_{2} ]]_{P}^{∗} is an isomorphism. Then again by coprimeness of representables in the Yoneda embedding, either [[A_{1} ]]_{P}^{∗} or [[A_{2} ]]_{P}^{∗} is an isomorphism. But the induction hypothesis then, there exist some n such that either [[A_{1} ]]_{P}^{n} or [[A_{2} ]]_{P}^{n} is an isomorphism. In either case [[A_{1} ∨ A_{2} ]]_{P}^{n} is an isomorphism.

G = C ⇒ D Suppose [[C ⇒ D]]_{P}^{∗} = [[D]]_{P ∪{C}}^{∗} is an isomorphism. Then by the induction hypothesis, there is an n such that [[D]]_{P ∪{C}}^{n} = [[C ⇒ D]]_{P}^{n} is an isomorphism.

G = ∃_{x:α}A Suppose that [[∃_{x:α}A]]_{P}^{∗} = Im_{[[π]]} [[A]]_{P (π)} is an isomorphism.

In particular, there is an isomorphism Hom(σ, α) ^{f} [[∃_{x:α}A]]_{P}^{∗} inverse to [[∃_{x:α}A]]_{P}^{∗} ⊆ Hom(σ, α). Observe that there is an epimorphism [[A]]_{P}^{∗} ^{e} [[∃_{x:α}A]]_{P}^{∗} (there is an epi from any subobject m to its image under Hom( , σ × α) ^{[[π]]} Hom(σ, α), which is precisely the first map of the epi-mono factorization of m [[π]]). Now we proceed by an argument almost identical to that of proposition (5.8). The source of f is representable, hence projective, so it lifts to an arrow Hom(σ, α) ^{f′} [[A]]_{P}^{∗}. But the composition f [[A]]_{P}^{∗} Hom( , σ × α) is an arrow between representables. By Yoneda it is the image of a substitution σ ^{θ} σ × α. By construction it is left inverse to [[π]], i.e. θ = ⟨id, t⟩ for some σ ^{t} α. Thus [[⟨id, t⟩]] factors through [[A]]_{P}^{∗}, so [[A(⟨id, t⟩) ]]_{P}^{∗} is an isomorphism.

By induction hypothesis, there is an n such that [[A(⟨id, t⟩) ]]_{P}^{n} is an isomorphism, i.e. [[⊤_{σ}]]^{n} ⊆ ( [[⟨id, t⟩]])^{#} [[A]]_{P}^{n}. By the argument at the end of the last case of the proof of soundness (lemma 5.4) [[⊤_{σ}]]^{n} ⊆ [[∃_{x:α}A]]_{P}^{n} so [[∃_{x:α}A]]_{P}^{n} is an isomorphism, as we wanted to show.

□

Definition 5.21 A clause of a program of the form tl_{cl} ⇒ X_{k}(u) is said to admit a formula X_{j}(t) if j = k and t is an instance of u.

Lemma 5.22 If an atomic formula A = X_{j}(t) is valid in all models of the program P, (i.e. is interpreted as an isomorphism) then some clause of P admits it.

Proof. Consider the model [[ ]]′ given by

[[X_{i}(t) ]]′_{Q} = ⋃_{(π, cl) ∈ κ(Q)_{hd_{cl}=X_{i}}}{Im_{[[π]]}Imeq( [[πt]], [[_{tm_{cl}}]])(eq( [[πt]], [[tm_{cl}]]))^{#}(id_{[[σ×α]]})}

for any program Q extending P, and where by convention, if X_{i} ≠ hd_{cl} for any cl ∈ κ(Q) then [[X_{i}(t) ]]′_{Q} (the empty union) shall be the unique arrow 0 → [[σ]] for σ = sort of X_{i}(t).

First we show that [[ ]]′ is a model of P. We must show that for any clause cl = (tl_{cl} ⇒ X_{i}(v)) of sort σ × β in any extension Q of P, [[tl_{cl}]]′_{Q(π)} ⊆ [[X_{i}(v) ]]′_{Q(π)}, where π is the projection σ × β σ.

Thus consider any clause (π : σ × β → σ, tl_{cl} ⇒ X_{i}(v)) ∈ κ(Q), for any extension Q of P of sort σ. To elucidate the following argument, some discussion of sorts will be useful.

Observe that if Q is a program extending P of sort σ, and B ⇒ X_{i}(u) a (possibly different) clause of Q of sort, say, σ × α, then the corresponding clause in a sort-adjusted program Q(π) is B(π × id) ⇒ X_{i}((π × id)u), as the following diagram illustrates:

B(π × id) ⇒ X_{i}((π × id)u)  B ⇒ X_{i}(u)

[figure: σ × β × α; π × id; σ × α]

[figure: σ × β; π′, ∀; π; σ; π′′, ∀]

Now we observe that by the definition above, for the particular clause under consideration,

[[X_{i}(v) ]]′_{Q(π)} = ⋃_{(π′, cl) ∈ κ(Q(π))_{hd_{cl}=X_{i}}}{Im_{[[π′ ]]}Imeq( [[π_{′}v]], [[(π × id)u]])(eq( [[π′v]], [[(π × id)u]]))^{#}(id_{[[σ×β×α]]})}

But one of the expressions in this union is the one corresponding to the clause cl = (tl_{cl} ⇒ X_{i}(v)) itself:

Im_{[[π′]]}Imeq( [[π_{′}v]], [[π_{′}v]])(eq( [[π′v]], [[π′v]]))^{#}(id_{[[σ×β×β]]})

which is just id_{[[σ×β]]}, implying [[X_{i}(v) ]]′_{Q(π)} is an iso. Hence, trivially, [[tl_{cl}]]′_{Q(π)} ⊆ [[X_{i}(v) ]]′_{Q(π)}. And thus [[ ]]′ is a model of P.

Now suppose X_{i}(t) is any goal valid in all models of P, so in particular in [[ ]]′. Then [[X_{i}(t) ]]′_{P} is an isomorphism. By coprimeness of representables, one of the expressions in the union defining this monic is also an iso. Let us suppose it is

Im_{[[π′′]]}Imeq( [[u]], [[π_{′′}t]])(eq( [[u]], [[π′′t]]))^{#}(id_{[[σ×α]]})

corresponding to some clause B ⇒ X_{i}(u). Since id_{[[σ]]} factors through this expression, by proposition 5.8 there is an arrow φ such that id_{[[σ]]} = φeq( [[u]], [[π′′t]]) [[π′′]]. But then

[[t]] = φeq( [[u]], [[π′′t]]) [[π′′]] [[t]]
= φeq( [[u]], [[π′′t]]) [[u]]

But φeq( [[u]], [[π′′t]]) has representable source and target and so, by fullness of the Yoneda embedding, is of the form [[θ]] for some θ in ℂ. By faithfulness of the Yoneda embedding t = θu which establishes that t is an instance of u. □

Lemma 5.23 Let G be any goal formula and P ∈ K a program, both of the same sort σ. If [[G]]_{P}^{k} is an isomorphism, then P ⊢_{o} G.

Proof. We proceed by induction on the structure of G and on k.

G atomic If k = 0, G must be the identity goal formula ⊤_{σ}, since [[X_{i}(t) ]]_{P}^{0} = 0 → [[σ]] cannot be an isomorphism. But the state ⟨P | ⊤_{σ}⟩ is already an SLD deduction of G from P.

Now suppose the result holds for all k < n, and all programs P ∈ K .

Suppose G = X_{i}(t) for some predicate token X_{i} and term t. Then

[[X_{i}(t) ]]_{P}^{n} = ⋃_{θtm_{cl} = θπt_{(π,cl)∈κ(P),hd_{cl}=X_{i}}}{Im_{[[π]]}Im_{[[θ]]} [[tl_{cl}θ]]_{P θπ}^{n−1}}

which is nonempty since by lemma 5.22 some clause of P admits X_{i}(t). Thus by hypothesis, the union on the right hand side is an iso. By coprimeness of representables in the Yoneda embedding one of the members Im_{[[π]]}Im_{[[θ]]} [[tl_{cl}θ]]_{P θπ}^{n−1} of the union is an iso, corresponding to some clause cl ∈ κ(P) such that hd_{cl} = X_{i} and θtm_{cl} = θπt.

By proposition 5.8 there is an arrow φ such that id_{σ} = φθπ and [[φ]] factors through [[tl_{cl}θ]]_{P θπ}^{n−1}. Letting γ = φθ we have that [[tl_{cl}γ]]_{P γπ}^{n−1} is an iso, with γtm_{cl} = γπt. By the induction hypothesis, there is a reduction sequence

⟨P γπ | tl_{cl}γ⟩⇝ ⋯ ⇝^{id}⇝NULL.

But then

⟨P | X_{i}(t)⟩ ⇝^{γπ,(tl_{cl}⇒X_{i}(tm_{cl}))} ⟨P γπ | tl_{cl}γ⟩⇝ ⋯ ⇝^{id}⇝NULL

is an SLD proof with computed answer substitution the identity, and so and P ⊢_{o} X_{i}(t).

G = A_{1}∧ A_{2} Then [[A_{1} ∧ A_{2} ]]_{P}^{n} = [[A_{1} ]]_{P}^{n} ∩ [[A_{2} ]]_{P}^{n} is an isomorphism iff both [[A_{1} ]]_{P}^{n} and [[A_{2} ]]_{P}^{n} are isomorphisms. But then by the induction hypothesis, P ⊢_{o} A_{1} and P ⊢_{o} A_{2}. Thus there are resolution sequences

⟨P | A_{1}⟩⇝ ⋯ ⇝^{id}⇝NULL

and

⟨P | A_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

which may be combined to give

⟨P | A_{1} ∧ A_{2}⟩⇝⟨P | A_{1}⟩&⟨P | A_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

Hence P ⊢_{o} A_{1} ∧ A_{2}.

G = A_{1}∨ A_{2} Then [[A_{1} ∨ A_{2} ]]_{P}^{n} = [[A_{1} ]]_{P}^{n} ∪ [[A_{2} ]]_{P}^{n} is an isomorphism iff either [[A_{1} ]]_{P}^{n} or [[A_{2} ]]_{P}^{n} are isomorphisms. But then by the induction hypothesis, either P ⊢_{o} A_{1} or P ⊢_{o} A_{2}. Thus there is a resolution sequence

⟨P | A_{i}⟩⇝ ⋯ ⇝^{id}⇝NULL

from which we have

⟨P | A_{1} ∨ A_{2}⟩⇝⟨P | A_{i}⟩⇝ ⋯ ⇝^{id}⇝NULL

And hence P ⊢_{o} A_{1} ∨ A_{2}.

G = C ⇒ D Then [[C ⇒ D]]_{P}^{n} = [[D]]_{P ∪{C}}^{n} is an isomorphism. But then by the induction hypothesis, P ∪ {C} ⊢_{o} D. Thus there is a resolution sequence

⟨P ∪ {C} | D⟩⇝ ⋯ ⇝^{id}⇝NULL

from which we have

⟨P | C ⇒ D⟩⇝⟨P ∪ {C} | D⟩⇝ ⋯ ⇝^{id}⇝NULL

And hence P ⊢_{o} C ⇒ D.

G = ∃_{x:α}A Suppose that [[∃_{x:α}A]]_{P}^{n} = Im_{[[π]]} [[A]]_{P (π)}^{n} is entire, i.e. equal to ℂ ( , σ). Then Im_{[[π]]} [[A]]_{P (π)}^{n}(σ) = ℂ (σ, σ), so id_{σ} ∈ (Im_{[[π]]} [[A]]_{P (π)}^{n})(σ) = Im_{[[π]]}^{set}( [[A]]_{P (π)}^{n}(σ)). Thus there is an arrow t in ℂ (σ, α) with ⟨t, id_{α}⟩ ∈ [[A]]_{P (π)}^{n}(σ). It follows easily that ( [[⟨t, id_{α}⟩]])^{#} [[A]]_{P (π)}^{n}, or, equivalently (lemma 5.5) [[A(⟨t, id_{α}⟩) ]]_{P}^{n} is an isomorphism. By the induction hypothesis, there is a resolution proof

⟨P | A(⟨t, id_{α}⟩)⟩⇝ ⋯ ⇝^{id}⇝NULL

which means, using lemma 4.10, that the following is also a resolution proof

⟨P | ∃_{x:α}A⟩ ⇝^{π} ⟨P π | A⟩⇝ ⋯ ⇝^{⟨t,id_{α}⟩}⇝NULL.

Thus we have P ⊢_{o} ∃_{x:α}A.

□

Theorem 5.24 (Operational Completeness) Let G be a goal formula and P a program over the signature ℂ[X], both of sort σ. Then, for any object ρ in ℂ

ρ ^{t} σ ∈ [[G]]_{P}^{∗} (ρ)  iff  P (t) ⊢_{o} G(t).

Proof. An immediate consequence of the Yoneda lemma ([33, 23]) is the equivalence of the following two conditions: for G a formula diagram of sort σ and ρ ^{t} σ in ℂ,

1. t ∈ [[G]]_{P}^{∗} (ρ).

2. Hom_{ℂ}( , ρ) ^{[[t]]} Hom_{ℂ}( , σ) factors through [[G]]_{P}^{∗},

where, we recall, [[t]] is the natural transformation Hom_{ℂ}( , t) whose action

[[t]](μ) : Hom_{ℂ}(μ, ρ) Hom_{ℂ}(μ, σ)

at each object μ of ℂ is given by [[t]](μ)(θ) = θt.

Hence t ∈ [[G]]_{P}^{∗} (ρ) iff [[t]] factors through [[G]]_{P}^{∗} iff [[G(t) ]]_{P (t)}^{∗} is an isomorphism. By lemmas 5.20,5.23 and soundness (lemmas 5.4,5.18) this holds iff P (t) ⊢_{o} G(t). □

6 Topos Semantics

Declarative programming is so called because the text of a program has an independent mathematical meaning which coincides, in a suitably defined way, with its operational meaning. The programming languages introduced in this paper consist of formula diagrams over a finite product category. Their operational meaning and resolution proof theory has been the subject of the preceding sections. We now define an analogue of the (first-order, intuitionistic) sequent calculus for such formula diagrams, and prove it sound and complete for conventional topos semantics. We then show that in the case of Weak Hereditarily Harrop programs and goals the notions of operational entailment and topos entailment coincide.

Topoi are categorical generalizations of the category of sets with internal operations that interpret logical connectives in a manner that generalizes their meaning in set-theoretic models. We begin by recalling the definitions of logical connectives in a topos. We then consider a restricted class of topos-theoretic models that generalizes the notion of Herbrand models, or term models, to models over a category, so as to give a Henkin-style proof of completeness. For more background on Topos theory and its logic the reader should consult e.g. [23, 34, 33].

Given some syntactic class of formulas F and a topos 𝔼, an 𝔼 -interpretation {[ ]} : F ⟶ 𝔼 maps sorts in F to objects and atomic formulas in F to subobjects (monics) of the appropriate object in 𝔼.

Definition 6.1 Let 𝔸 be a finite product category, 𝔸 [X] a categorical signature and let 𝔼 be a topos. A topos interpretation of 𝔸 -formulas (an 𝔸 -interpretation) into 𝔼 is a cartesian (pullback and terminator preserving) functor

{[ ]} : 𝔸 [X] ⟶ 𝔼

whose value {[X_{i}]} on monics X_{i} ∈ X of sort σ is a monic whose target is {[σ]}.

A topos interpretation extends to formula diagrams over the signature 𝔸 [X] via the conventional topos-theoretic logical operators {∩, ∪, ⊃} on the subobject Heyting Algebra as follows:

• {[A(t) ]} = ( {[t]})^{#}( {[A]})

• {[A_{1} ∧ A_{2} ]} = {[A_{1} ]} ∩ {[A_{2} ]}

• {[A_{1} ∨ A_{2} ]} = {[A_{1} ]} ∪ {[A_{2} ]}

• {[A_{1} ⇒ A_{2} ]} = {[A_{1} ]} ⊃ {[A_{2} ]}

• {[∀_{x:α}A]} = ∀_{π}( {[A]})

• {[∃_{x:α}A]} = ∃_{π}( {[A]})

where ∀_{π}, ∃_{π} are the right and left adjoints of the pullback functor (π)^{#} : Sub( {[σ]}) ⟶ Sub( {[σ]} × {[α]}) induced by the projection σ × α ^{π} σ in 𝔸, and σ is the sort of the formulas ∀_{x:α}A and ∃_{x:α}A.

Definition 6.2 A formula diagram A is true in the interpretation if the subobject {[A]} is an isomorphism.

We will now introduce a logic for 𝔸 -interpretations, that is to say a sequent calculus for first-order minimal intuitionistic logic for formula diagrams over a finite-product category.

6.1 First-order Logic over a Finite Product Category

In this section we define a categorical logic over extensions of a finite product τ-category ℂ. By an indeterminate, or a generic constant of sort σ over ℂ we mean a new arrow 1 σ.

We say that a categorical signature 𝔻 extends ℂ if it is a category ℂ (Y) obtained by freely adjoining a possibly infinite set Y of indeterminates to ℂ. This well-known construction is covered in e.g. [33].

6.1.1 Expanding the signature

Given a finite product category ℂ, we consider a category of polynomial categories, or Henkin extensions of ℂ, created by adding fresh constants drawn from a set W_{ℂ} of witnesses (countably many of each sort) to ℂ. The collection of Henkin extensions ℂ (Y) by a finite set Y ⊂ W_{ℂ}, together with the faithful, finite-product preserving functors ι_{1,2} : ℂ (Y_{1}) ⟶ ℂ (Y_{2}) obtained from the universal mapping property for polynomial categories, has as a colimit the category ℂ^{∗} = ℂ (W_{ℂ}) which is the full Henkin extension. An alternative treatment to Henkin completeness using slice categories to add generic arrows and using capitalization is given in [23].

Definition 6.3 Let ℂ be a small finite product category, Y a set disjoint from the collection of arrows in ℂ, each member of which is associated with an object of ℂ, (which we will call its sort). Then the category ℂ (Y) is obtained by freely adjoining generic constants Y to ℂ.

One can easily show that ℂ (Y) has a terminator, finite products, and a τ-structure. The definitions and arguments are similar to those given in e.g. [33], where the following is also shown.

Lemma 6.4 Let ℂ and Y be as in the preceding definition. Then there is a faithful finite product functor ι_{Y} : ℂ ℂ (Y). Let ℂ ^{F} 𝔹 be a finite-product functor and B = {1 ^{b_{y}} A_{y} : y ∈ Y } a set of arrows in ℂ in one to one correspondence with Y. Then there is a unique finite-product functor Ψ_{B} : ℂ (Y) 𝔹 with Ψ_{B}([y]) = b_{y} and ιΨ_{B} = F.

Corollary 6.5 If Y_{1} ⊂ Y_{2} ⊂ Y there is a unique faithful finite product functor ℂ (Y_{1}) ^{ι_{1,2}} ℂ (Y_{2}).

Proof. We let ℂ ^{F} 𝔹 be ℂ ^{ι_{Y_{2}}} ℂ (Y_{2}) in the preceding lemma. □

Definition 6.6 Let ℂ be a small finite product category. The Henkin set W_{ℂ} for ℂ is the set {(σ, i) : σ ∈ |ℂ | and i ∈ ℕ}. The category of finite generic extensions [ℂ] has, for

\underline{objects}: the categories \{ℂ (Y) : Y a finite subset of W_{ℂ}\}, together with the “point at infinity” ℂ (W_{ℂ}) and

\underline{arrows}: the collection \{ℂ (Y_{1}) ^{ι_{Y_{1},Y_{2}}} ℂ (Y_{2}) : ∅ ⊆ Y_{1} ⊆ Y_{2} ⊂ W_{ℂ}\} and the arrows to the point at infinity {ℂ (Y) ^{ι_{Y}^{∗}} : Y ⊆ W_{ℂ}}

Let X_{1}, …, X_{n} be a sequence of generic predicate tokens of sorts b = b_{1}, …, b_{n} from ℂ. Recall that the canonical, or generic formula diagrams F (ℂ [X_{1}, …, X_{n}]) of b-signature ℂ (definition 3.9) are the formula diagrams built up using generic predicate tokens of sorts b. We can now define generic formula diagrams for the same generic predicate tokens over each category in [ℂ], since the maps ι between objects ℂ_{1} and ℂ_{2} in [ℂ]induce maps ι̂ between the sets of formula diagrams over these objects. To see this one first shows that ι induces a faithful FP functor from ℂ_{1}[X_{1}, …, X_{n}] to ℂ_{2}[X_{1}, …, X_{n}] which sends objects (σ, S) to (σ, ιS) and arrows between objects (which live in ℂ) to themselves. This functor lifts naturally to a map between the classes of formula diagrams built over each.

We adopt the following coercion conventions for speaking about such formula diagrams. If A ∈ F (ℂ (Y_{1})) and Y_{1} ⊂ Y_{2} then we may denote by the same symbol A the formula diagram ι̂_{1,2}(A) in F (ℂ (Y_{2})) when the context makes clear that we are over the category ℂ (Y_{2}). Similarly we will speak of arrows t in ℂ (Y_{1}) as arrows of ℂ (Y_{2}).

Definition 6.7 (The language of a formula) Suppose A is a formula diagram over ℂ^{∗}. Then there is a unique minimal Y ⊆ W_{ℂ} with some A′ ∈ ℂ (Y) and A = ι_{Y}^{∗} (A′).We refer to ℂ (Y) as the signature or language of A.

Let the map χ : F (ℂ (W_{ℂ})[X]) × |ℂ | ℂ^{∗} be defined by letting χ(A, σ) be the least (σ, i) in ℂ^{∗} not in the language of A.

The map χ will be used to provide fresh generic constants for universally quantified formulas.

6.1.2 A Sequent Calculus

We now introduce our sequent calculus for reasoning with formula diagrams over the categories in [ℂ].

Definition 6.8 Let ℂ be a finite product τ-category and X a set of predicate letters with sorts in ℂ. A (categorical) 𝔻 -sequent is an ordered triple (𝔻 , Γ, A), where 𝔻 is a language extending ℂ, A is a formula diagram over 𝔻, and Γ is a 𝔻 -theory: a set of formula diagrams of the same sort over 𝔻. Sequents are written 𝔻 , Γ ≫ A.

Definition 6.9 A sequent 𝔻 , Γ ≫ A is said to be initial if A ∈ Γ and A is an atom. A 𝔻 -proof is either a 𝔻 -initial sequent or a tree with 𝔻 -initial sequents at its leaves, built from smaller proofs by the use of the rules of inference in the following table.

\frac{𝔻 , B, C, Γ ≫ A}{𝔻 , B ∧ C, Γ ≫ A}∧-L  \frac{𝔻 , Γ ≫ B  𝔻 , Γ ≫ C}{𝔻 , Γ ≫ B ∧ C} ∧-R
\frac{𝔻 , Γ, B ≫ A  𝔻 , Γ, C ≫ A}{𝔻 , Γ, B ∨ C ≫ A}∨-L  \frac{𝔻 , Γ ≫ B}{𝔻 , Γ ≫ B ∨ C} ∨-R \frac{𝔻 , Γ ≫ C}{𝔻 , Γ ≫ B ∨ C} ∨-R
\frac{𝔻 , Γ ≫ B  𝔻 , Γ, C ≫ A}{𝔻 , Γ, B ⇒ C ≫ A}⇒-L  \frac{𝔻 , Γ, B ≫ C}{𝔻 , Γ ≫ B ⇒ C} ⇒-R
\frac{𝔻 , Γ, P (⟨id_{σ}, t⟩) ≫ A}{𝔻 , Γ, ∀_{x:α}P ≫ A}∀-L  \frac{𝔻 (a), Γ ≫ P (⟨id_{σ},!_{σ}a⟩)}{𝔻 , Γ ≫ ∀_{x:α}P}∀-R∗
\frac{𝔻 (a), Γ, P (⟨id,!_{σ}a⟩) ≫ A}{𝔻 , Γ, ∃_{x:α}P ≫ A}∃-L∗  \frac{𝔻 , Γ ≫ P (⟨id_{σ}, t⟩)}{𝔻 , Γ ≫ ∃_{x:α}P}∃-R

where (σ ^{t} α) ∈ 𝔻 in ∀-L and ∃-R, and !_{σ}a means the composition

σ ^{!_{σ}} 1 ^{a} σ.

Rules marked with a ∗ have the side condition that ‘a’ is a Henkin constant which must not be in the language (e.g. χ(D, σ), see definition 6.7) of any formula diagrams in the conclusion of the rule. The starred rules yield quantified formulas from premisses involving generic constants. The predicates are instantiated at ⟨id_{σ},!_{σ}a⟩ because the sorts of the unquantified predicates are product sorts.

We write 𝔻 , Γ ⊢_{c} B to mean there is a 𝔻 -proof whose final sequent is 𝔻 , Γ ≫ B.

A closed formula diagram means a diagram of sort 1. A closed theory means a set of closed formula diagrams. If Γ is closed, then, in a τ-category⟨id,!_{σ}a⟩ = a.

The following facts, which are easily checked, will prove useful:

Lemma 6.10 If the language of the theory Γ and the formula diagram A is 𝔻, and 𝔻′ extends 𝔻 in [ℂ], and

𝔻′, Γ ⊢_{c} A

then

𝔻 , Γ ⊢_{c} A

Lemma 6.11 Sequents are preserved under pullback: if 𝔻 , Γ ⊢_{c} A then 𝔻 , Γ(t) ⊢_{c} A(t) for t of the appropriate sort in 𝔻, where Γ(t) means the set {γ(t) : γ ∈ Γ}

The proof is an easy induction.

Lemma 6.12 (Cut Elimination) The cut rule is admissible in the 𝔻 -sequent calculus defined above: if a sequent is derivable using the rule

\frac{𝔻 , Γ ≫ B  𝔻 , Γ′, B ≫ A}{𝔻 , Γ, Γ′ ≫ A}CUT

it has a cut-free proof.

The proof is identical to that for cut elimination in the standard sequent calculus, see e.g. [25].

Theorem 6.13 (Soundness) If 𝔻 , Γ ⊢_{c} A then A is true in every 𝔻 -interpretation of Γ (i.e. in which every formula diagram in Γ is true).

The proof is identical to the standard proof of soundness of topos semantics for first-order logic. We will now show these rules are complete for 𝔸 -interpretations. We will use a canonical inter-

pretation, a topos-theoretic analogue of the Henkin model familiar from logic. To do so, we make use of the following notions and facts from conventional logic which extend easily to categorical logic.

Definition 6.14 A set Γ of formula diagrams over 𝔻 [X] is said to be a prime theory over 𝔻 (or 𝔻 -saturated theory) if it has the disjunction and existence properties:

𝔻 , Γ ⊢_{c} A ∨ B ⇒ 𝔻 , Γ ⊢_{c} A or 𝔻 , Γ ⊢_{c} B
𝔻 , Γ ⊢_{c} ∃_{x:α}A ⇒ 𝔻 , Γ ⊢_{c} A(⟨id_{σ}, u⟩)  for some σ ^{u} α in 𝔻 .

Lemma 6.15 (Lindenbaum) If 𝔻 , Γ ⊬_{c} A then, for any 𝔻′ extending 𝔻, there is a prime theory Δ over 𝔻′ such that Δ ⊇ Γ and

𝔻′, Δ ⊬_{c} A

i.e. every consistent theory has a consistent prime extension.

The proof is the same as the standard one for logic: the prime extension is constructed in stages. See e.g. [66].

6.2 Henkin Interpretations

Let {V_{i} : i ∈ ℕ} be a countable collection of disjoint sets of witnesses (see e.g. section 6.1.1) containing countably many new constants of each sort in ℂ. Let W_{o} = ϕ, and for n ≥ 1, let W_{n} = V_{1} ∪ ⋯ ∪ V_{n} and W = ⋃ W_{n}. Assume that for each sort σ, the (countable) set W_{σ} of constants in W of sort σ is well-ordered, so that for any proper subset Y of W_{σ} we can speak of the least member of W_{σ} not in Y. Let B be the collection of polynomial categories ℂ (W_{n}) or ℂ (W) extending ℂ by freely adjoining the constants in W_{n} or W, as in section 6.1.1. To simplify notation, we will use the symbols 𝔹_{o}, 𝔹 , 𝔹′, 𝔹′′, … to range over the collection of categories in B. Note that all members of B have the same collection of objects and there are canonical faithful finite product preserving functors ι_{𝔹} : 𝔹 → 𝔹′ whenever 𝔹′ is an extension of 𝔹 .

Definition 6.16 If Γ is a theory (a set of formula diagrams), we say Γ′ extends Γ if Γ ⊆ Γ′.

Let 𝔹 be a category in B, and Γ a closed prime theory over 𝔹. J (𝔹 , Γ) is the poset of signaturetheory pairs (𝔹′, Γ′) extending (𝔹 , Γ).

Definition 6.17 Let 𝔹 be a category in B, and Γ a closed prime theory over 𝔹. Then 𝕁 (𝔹 , Γ) is the following category:

• \underline{objects:} triples (ρ, 𝔹′, Γ′) with ρ an object in ℂ, and (𝔹′, Γ′) in J (𝔹 , Γ).

• \underline{arrows:} (ρ, 𝔹′, Γ′) ^{t} (ρ′, 𝔹′′, Γ′′) where (𝔹′, Γ′) ≥ (𝔹′′, Γ′′) and ρ ^{t} ρ′ is in 𝔹′(ρ, ρ′).

Definition 6.18 Let 𝔹_{o} be a category in B and Γ_{o} a prime theory over 𝔹_{o}. A Henkin 𝔹_{o}- interpretation of Γ_{o} is a topos interpretation into the Yoneda presheaf topos for 𝕁 (𝔹_{o}, Γ_{o}) given by a functor

{[ ]}_{𝔹_{o}} : 𝔹_{o}[X] ⟶ Set^{𝕁(𝔹_{o},Γ_{o})^{o}}

mapping monics X_{i}(t) to monics, and satisfying:

{[σ]}_{𝔹_{o}}(ρ, 𝔹 , Γ) = Hom_{𝔹}(ρ, σ)
{[σ]}_{𝔹_{o}}((ρ, 𝔹 , Γ) ^{t} (ρ′, 𝔹′, Γ′))(θ) = t(ι_{𝔹′}θ)

and which, on arrows σ ^{u} σ′ in 𝔹_{o}, {[u]}_{𝔹_{o}} : {[σ]}_{𝔹_{o}} ⟶ {[σ′]}_{𝔹_{o}} is given by

{[u]}_{𝔹_{o}}(ρ, 𝔹 , Γ)(θ) = θ(ι_{𝔹_{o}}u).

In other words {[ ]}_{𝔹_{o}} behaves similarly to a “varying Yoneda embedding” indexed over B. We will not take the trouble to formalize the obvious indexed category structure here.

When the ambient signature of 𝔹_{o} is clear from context we will also omit reference to it, and write {[B]} instead of {[B]}_{𝔹_{o}}. Note also that a Henkin interpretation is completely determined by an assignment of monics in Set^{𝕁(𝔹_{o},Γ_{o})^{o}} with appropriate targets, to the monics X_{i} in X.

Remark 6.19 We have defined a family of Henkin interpretations, one for each signature-theory pair (𝔹_{o}, Γ_{o}). The reader can check that if (𝔹′, Γ′) extends (𝔹 , Γ) then J (𝔹′, Γ′) ⊂ J (𝔹 , Γ) and there is an inclusion functor 𝕁 (𝔹′, Γ′) ⊂ 𝕁 (𝔹 , Γ) and an induced functor

Set^{𝕁 (𝔹 ,Γ)^{o}} Set^{𝕁 (𝔹′,Γ′)^{o}}.

Hence, whenever both sides are defined, (i.e. A is a formula diagram over a signature extended by 𝔹′and 𝔹′′, and 𝔹′′′extends both of these signatures, and Γ′′′ extends the base theory)

{[A]}_{𝔹′}^{∗}(ρ, 𝔹′′′, Γ′′′) = {[A]}_{𝔹′′}^{∗}(ρ, 𝔹′′′, Γ′′′).

6.3 The Canonical Henkin Interpretation

We now give a a completeness theorem for the generalized categorical logic (section 6.1) in the spirit of Aczel’s completeness theorem for intuitionistic logic [66]. We define canonical Henkin interpretations {[ ]}^{∗}, by letting monic assignments be dictated by the proof theory.

Definition 6.20 Let ℂ [X]be a categorical signature, 𝔹_{o} a Henkin extension in B, and Γ_{o} a closed prime theory over 𝔹_{o}. The canonical interpretation {[ ]}_{𝔹_{o}}^{∗} for Γ_{o} is the Henkin interpretation induced by the following assignment of monics X_{i} ∈ X of sort σ in the topos Set^{𝕁(𝔹_{o},Γ_{o})^{o}}

{[X_{i}]}_{𝔹_{o}}^{∗}(ρ, 𝔹 , Γ) := {t : ρ ^{t} σ ∈ 𝔹 and 𝔹 ,!_{ρ}Γ ⊢ X_{i}(t)}

Proposition 6.21 (Completeness of ℂ -logic) Suppose A is a formula diagram of sort σ over 𝔹_{o}[X], and {[ ]}_{𝔹_{o}}^{∗} the canonical Henkin interpretation of the closed prime theory Γ_{o} over 𝔹_{o}[X]. Then, for any object (ρ, 𝔹 , Γ) in 𝕁 (𝔹_{o}, Γ_{o}),

{[A]}_{𝔹_{o}}^{∗}(ρ, 𝔹 , Γ) = {t : ρ ^{t} σ ∈ 𝔹 and 𝔹 ,!_{ρ}Γ ⊢_{c} A(t)}

Proof. We establish this equation by induction on the structure of the formula diagram A. The atomic case is true by hypothesis.

\underline{A ≡ A_{1} ∧ A_{2}}: \{[A_{1} ∧ A_{2} ]\}^{∗}(ρ, 𝔹 , Γ) = \{[A_{1} ]\}^{∗}(ρ, 𝔹 , Γ)∩ \{[A_{2} ]\}^{∗}(ρ, 𝔹 , Γ) which, by inductive hypoth-

esis and the ∧-R and ∧-L rules, is {t : ρ ^{t} σ ∈ 𝔹 and 𝔹 ,!_{ρ}Γ ⊢_{c} (A_{1} ∧ A_{2})(t)}.

\underline{A ≡ A_{1} ∨ A_{2}}: \{[A_{1} ∨ A_{2} ]\}^{∗}(ρ, 𝔹 , Γ) = \{[A_{1} ]\}^{∗}(ρ, 𝔹 , Γ) ∪ \{[A_{2} ]\}^{∗}(ρ, 𝔹 , Γ) =

{ρ ^{t} σ : 𝔹 ,!_{ρ}Γ ⊢_{c} A_{1}(t) or 𝔹 ,!_{ρ}Γ ⊢_{c} A_{2}(t)}. Since Γ satisfies the disjunction property, the latter set is equal to {ρ ^{t} σ : 𝔹 ,!_{ρ}Γ ⊢_{c} A(t)}.

\underline{A ≡ ∃_{x:α}B}: We begin showing that an easy consequence of the proof rules is the following derived rule of inference:

\frac{𝔹 ,!_{ρ}Γ ≫ B(⟨t, w⟩)}{𝔹 ,!_{ρ}Γ ≫ (∃_{x:α}B)(t)}

where the quantification in the conclusion is along the projection ρ × α ^{π′} ρ.

B(t × id_{α})  B

[figure: ρ; ⟨id_{ρ}, w⟩; ρ × α; t × id_{α}; σ × α]

[figure: ρ; π′, ∃; t; σ; π, ∃]

By definition (2.2) (∃_{x:α}B)(t) = ∃_{x:α}(B(t × id_{α})) and ⟨id_{ρ}, w⟩(t × id_{α}) = ⟨t, w⟩. Thus, 𝔹 ,!_{ρ}Γ ≫ B(⟨t, w⟩) iff 𝔹 ,!_{ρ}Γ ≫ B(t × id_{α})(⟨id_{ρ}, w⟩) from which, by ∃-R, we infer 𝔹 ,!_{ρ}Γ ≫ ∃_{x:α}(B(t × id_{α})), which is precisely 𝔹 ,!_{ρ}Γ ≫ (∃_{x:α}B)(t).

Now suppose ρ ^{u_{o}} σ is an arrow in 𝔹 and

u_{o} ∈ {[∃_{x:α}B]}^{∗}(ρ, 𝔹 , Γ).

Images are evaluated pointwise, so this yields u_{o} ∈ ∃_{π}( {[B]}^{∗})(ρ, 𝔹 , Γ). Hence, for some ρ ^{u_{1}} α we have ⟨u_{o}, u_{1}⟩ ∈ {[B]}^{∗}(ρ, 𝔹 , Γ). By induction hypothesis 𝔹 ,!_{ρ}Γ ⊢_{c} B(⟨u_{o}, u_{1}⟩), hence we may infer 𝔹 ,!_{ρ}Γ ⊢_{c} (∃_{x:α}B)(u_{o}). We have shown

{[∃_{x:α}B]}^{∗}(ρ, 𝔹 , Γ) ⊆ {ρ ^{t} σ : 𝔹 ,!_{ρ}Γ ⊢_{c} (∃_{x:α}B)(t)}.

For the other direction, suppose 𝔹 ,!_{ρ}Γ ⊢_{c} (∃_{x:α}B)(t), that is to say,

𝔹 ,!_{ρ}Γ ⊢_{c} ∃_{x:α}(B(t × id_{α})).

Since Γ is a prime theory, there is a ρ ^{v} α such that

𝔹 ,!_{ρ}Γ ⊢_{c} (B(t × id_{α}))(⟨id_{ρ}, v⟩).

But (B(t × id_{α}))(⟨id_{ρ}, v⟩) = B(⟨id_{ρ}, v⟩(t × id_{α})) = B(⟨t, v⟩). So, by induction hypothesis we have ⟨t, v⟩ ∈ {[B]}^{∗}(ρ, 𝔹 , Γ) whence t ∈ ∃_{π}( {[B]}^{∗})(ρ, 𝔹 , Γ), which establishes the other containment.

\underline{A ≡ A_{1} ⇒ A_{2}}: Implication of predicates in a topos is not evaluated pointwise. \{[A_{1} ⇒ A_{2} ]\}^{∗}(ρ, 𝔹 , Γ) = [ {[A_{1} ]}^{∗} ⊃ {[A_{2} ]}^{∗}](ρ, 𝔹 , Γ), which equals

{t : for every (ν, 𝔹′, Γ′) ^{u} (ρ, 𝔹 , Γ) if u(ι_{𝔹}t) ∈ {[A_{1} ]}^{∗}(ν, 𝔹′, Γ′) then u(ι_{𝔹}t) ∈ {[A_{2} ]}^{∗}(ν, 𝔹′, Γ′)}

By the induction hypothesis, this is equal to

{t : ∀u, if 𝔹′,!Γ′ ⊢_{c} A_{1}(ut)then 𝔹′,!Γ′ ⊢_{c} A_{2}(ut)}  (5)

We now claim this is, in fact, the set

{t : 𝔹 ,!Γ ⊢_{c} (A_{1} ⇒ A_{2})(t)}  (6)

That (6)⊆(5) follows immediately from the cut rule.

So, it suffices to show that (5)⊆(6). If not, for some t in (5), 𝔹 ,!Γ ⊬_{c} (A_{1} ⇒ A_{2})(t). Then, using cut, the ∀ − R rule and lemma 6.11, we have that 𝔹 (a), Γ ⊬_{c} (A_{1} ⇒ A_{2})(at) and so 𝔹 (a), Γ, A_{1}(at) ⊬_{c} A_{2}(at). By Lindenbaum’s lemma 6.15, some prime extension 𝔹′, Γ′ of the premise 𝔹 (a), Γ, A_{1}(at) exists for which 𝔹′, Γ′ ⊬_{c} A_{2}(at) despite the fact that 𝔹′, Γ′ ⊢_{c} A_{1}(at) contradicting the definition of t.

\underline{A ≡ ∀_{x:α}B}: \{[∀_{x:α}B]\}^{∗} = ∀_{π} \{[B]\}^{∗}. ∀_{π}, the right adjoint of pullback along σ × α ^{π} σ, is not evaluated pointwise:

∀_{π} {[B]}^{∗}(ρ, 𝔹 , Γ) =

{t : for every(ν, 𝔹′, Γ′) ^{u} (ρ, 𝔹 , Γ), {⟨ut, v⟩ : v ∈ Hom_{𝔹′}(ν, α)} ⊆ {[B]}^{∗}(ν, 𝔹′, Γ′)}

Suppose 𝔹 ,!_{ρ}Γ ⊢_{c} ∀_{x:α}(B(t × id_{α})). Then, using cut and lemma 6.11, we have, for every (ν, 𝔹′, Γ′) ^{u} (ρ, 𝔹 , Γ) that 𝔹′,!_{ν}Γ′ ⊢_{c} (B(ut × id_{α}))⟨id, v⟩ for all v ∈ Hom_{𝔹′}(ν, α). Hence, by the induction hypothesis, ⟨ut, v⟩ ∈ {[B]}^{∗}(ν, 𝔹′, Γ′), and so by definition, t ∈ ∀_{π} {[B]}^{∗}(ρ, 𝔹 , Γ).

Conversely, suppose t ∈ ∀_{π} {[B]}^{∗}(ρ, 𝔹 , Γ), but 𝔹 , Γ ⊬_{c} (∀_{x:α}B)(t). Then for any 𝔹′ extending 𝔹, and any generic constant c of sort α in 𝔹′but not in 𝔹, we have 𝔹′, Γ ⊬_{c} B(⟨t,!c⟩)

By Lindenbaum’s lemma, for some 𝔹′-prime theory Γ′ extending Γ we have 𝔹′, Γ′ ⊬_{c} B(⟨t,!c⟩). Hence, by the induction hypothesis, (⟨t,!c⟩) ∉ {[B]}^{∗}(ρ, 𝔹′, Γ′) so t ∉ ∀_{π} {[B]}^{∗}(ρ, 𝔹 , Γ). □

Corollary 6.22 Suppose A is a formula diagram of sort σ over 𝔹_{o}[X]. Then {[A]}^{∗} is an isomorphism (as a subobject of {[σ]}_{𝔹_{o}}^{∗}) if and only if 𝔹_{o}, Γ ⊢_{c} A.

The corollary follows from the fact that 𝔹_{o}, Γ ⊢_{c} A if and only if the identity morphism is in {[A]}^{∗}(σ, 𝔹_{o}, Γ) if and only if {[A]}^{∗} is an isomorphism.

To show the equivalence of operational and declarative semantics when applied to programs and goals, we use the equivalence of the associated logics of SLD-proofs and ℂ -proofs. The proof of their equivalence is identical to that given in [46] (theorems 4 and the proof of 6), since the relevant properties, permutability of the left ∧, ∀, ⇒ rules with the right ∧, ∨ ⇒ ∀, ∃ rules are easily seen to hold in ℂ -logic as well. A direct semantic proof of the equivalence of operational and Kripke semantics is given in [17].

Theorem 6.23 Let P_{o} be a closed program over ℂ, G a goal of sort σ over ℂ. For each arrow ρ ^{t} σ in ℂ

t ∈ {[G]}^{∗}(ρ, ℂ , P_{o}) ⟺ t ∈ [[G]]_{!_{σ}P_{o}}^{∗}(ρ).

Proof. We make use of the respective completeness theorems (5.24,6.21) to reduce the claim to the just cited equivalence of resolution ⊢_{o} and provability in the ℂ-sequent calculus. Suppose t ∈ {[G]}^{∗}(ρ, ℂ , P_{o}). Then ℂ ,!_{ρ}P_{o} ⊢_{c} G(t), whence !_{ρ}P_{o} ⊢_{o} G(t), and thus ι_{∗}t ∈ [[G]]_{!_{σ}P_{o}}^{∗}(ρ).

To prove the converse, suppose t ∈ [[G]]_{!_{σ}P_{o}}^{∗}(ρ). Then !_{ρ}P_{o} ⊢_{o} G(t), so ℂ ,!_{ρ}P_{o} ⊢_{c} G(t). By lemma 6.10, this implies ℂ ,!_{ρ}P_{o} ⊢_{c} G(t), whence t ∈ {[G]}^{∗}(ρ, ℂ , P_{o}). □

7 Examples and Conclusion

In this paper we have given a categorical treatment of the resolution calculus for Horn and firstorder Weak Hereditarily Harrop (WHH) formulas with categorically defined constraints, sound and complete with respect to operational and declarative semantics. Our notion of categorical signature formalizes the structure of many constraint systems. For example, let L be a first-order language, E an equational theory over L. We define two finite-product categories: ℍ the empty Lawvere algebraic theory for L, and ℍ/E the algebraic theory associated with E, to capture pure logic programming over the Herbrand Universe in the former case, and logic programming over the equational constraints in E in the latter. We give a brief description here. The reader should consult e.g. [58] for a fuller treatment of algebraic theories.

Define ℍ, 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, 2, …, and arrows the closure under composition of the following:

• For each nonzero pair of objects m, n with m ≤ n all the projection maps

π_{m}^{n}(i_{1}, …, i_{m}) : n → m,

where i_{1}, …, i_{m} is a sequence of m elements from {1, …, n}, and all the diagonal arrows δ : m → n. These arrows define precisely the opposite category of the full subcategory of Set consisting of the Von-Neumann finite ordinals

{} ⊂ {0} ⊂ {0, 1} ⊂ ⋯

• In addition, the signature contributes, 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 all usual identities for projections and diagonal maps.

This category has products (n×m = nm) and τ-structure, as the reader can check. Furthermore there is a one-to-one correspondence between arrows from 0 to 1 in ℍ and terms in the Herbrand universe over L. The arrows from 0 to m correspond to m-tuples of terms. If we now give ℍ 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, with X_{i} of sort n if the corresponding predicate letter has arity n, then H[X_{1}, …, X_{n}] captures logic programming in the sense made precise in the theorem below.

Theorem 7.1 Let P be a Horn (resp. Weak Hereditarily Harrop) program, G a goal in the corresponding language. Let X be a set of generic monics of appropriate sort, corresponding to each of the predicate letters in P and G. Then there is a Horn-SLD (resp. Weak Hereditarily Harrop) proof P ⊢_{o}G over ℍ if and only if for every topos 𝔼 and every ℍ-interpretation {[ ]} : ℍ [X] ⟶ 𝔼 in which P is true we have that {[G]} is an isomorphism.

SLD proofs over ℍ are resolution proofs in our sense. All computed answer substitutions can be taken to be compositions of equalizers (mgu’s). Categorical Horn clause programming over ℍ is essentially the case studied in [4].

Even in the case of Horn clause programs over the Herbrand universe, our operational interpretation gives non-ground bottom-up semantics, which is more general than the usual T_{P} -operator.

A straightforward adaptation of the preceding construction gives the corresponding free category ℍ_{L} for many-sorted logic, by taking sorts as objects, with the obvious projections and diagonals. We can further modify the construction to capture equational constraints. Let L be a language, possibly many-sorted, and E an equational theory over L. By taking a quotient ℍ_{L}/E of the Herbrand category we obtain the algebraic theory associated with E, containing the same objects as ℍ_{L} and congruence classes of arrows induced by E as morphisms.

SLD-resolution over this category corresponds to finding a computed answer with equational constraints from E. Similarly, the following theorem is an immediate consequence of the results in this paper.

Theorem 7.2 Let P be a Horn (resp. WHH) program, G a goal, both over the language L. Let X be a set of generic monics of appropriate sort, corresponding to each of the predicate letters in P and G. Then there is a Horn-SLD (resp. WHH) proof P ⊢_{o}G over ℍ_{L}/E if and only if for every topos 𝔼 and every ℍ_{L}/E-interpretation {[ ]} : ℍ_{L}/E[X] ⟶ 𝔼 in which P is true we have that {[G]} is an isomorphism.

The notion of constraint captured in this paper is considerably more general than these examples: not all cartesian categories are algebraic theories. A precise syntactic characterization of such constraints requires a study of Cartesian Logic [22], which is the subject of a forthcoming paper.

Beyond Generic Predicates The reader may ask how results in this paper are affected by the restriction of categorical signatures to those of the form (ℂ [X], X) induced by generic predicates. McGrail [42] has shown how to modify the notion of generic predicate to build in functional constraint and monad structure, which is also outlined in [37]. It would be interesting to see how these results could be extended to incorporate higher-order constraint information and e.g. objects and inheritance into logic programming.

7.1 Perspectives on Uniform proofs

In our operational semantics, we characterize the predicates defined by a logic program via a fixpoint construction using a continuous operator E which induces a map from interpretations to interpretations, incrementally defining the meaning of goal formulae. An essential component of the behavior of the interpretations so defined is that they give a search theoretic interpretation of certain critical connectives. For example, the meaning of A ⇒ B is given by [[A ⇒ B]]_{P} = [[B]]_{P,A}, that is to say, by tearing apart formulae and interpreting them in a shifted semantics, which are only required to give meaning to basic (in our case atomic, conjunctive and disjunctive) formulas. Thus a semantic shift or change of state appears to be an essential feature of the uniform or search-theoretic interpretations of connectives. What guarantees correctness with respect to a “standard” interpretation is the agreement of the limiting operational bracket with conventional interpretation {[ ]} in a standard model (in our case, a topos). This suggests a quite general blueprint for analyzing abstract connectives, or even defining them semantically. One seeks identities of the form

[[A ∗ B]]_{𝔹,P} = [[F (A, B, P, 𝔹) ]]_{G(A,B,P,𝔹)},

where the operator G defines the interpretation shift and F yields a formula that is –in some sense– more basic than A ∗ B. It would be interesting to study which operations of this kind (over more general semantic categories) corresponding to other logics (e.g. Girard’s LU[24], linear logic programming languages [28, 45, 9]), and which give rise to useful operations that still agree with some notion of conventional semantics in the limiting case.

7.2 Directions for future work

This foundation opens the way to a categorical approach to modeling other extensions of logic programming [28, 51, 50, 55, 49], and connecting well-known techniques for modeling functional evaluation, non-local control, side effects (e.g. monads, see [62, 42, 47, 68, 69]), to the declarative and operational semantics of logic programs.

Our operational semantics ignores control issues (such as the selection rule) since it is defined in terms of the declarative text of the program. It would be straightforward to modify the operator E to take such control into account, giving rise to different, more computationally oriented semantics. Also, it would be interesting to capture in a categorical context the structure of other semantics (compositional, open program, unfolding, etc.), studied by Levi et. al. [8, 40, 1, 43].

In addition, an interesting follow-up to the work presented here would be a categorical analysis of the Jaffar-Lassez criteria [29] for constraint domains and of the Lassez-MacAloon [35] constraint calculi. Our categorical study should also be extended to the case of higher-order logic, L-λ, and dependent type theory. It would seem that a categorical formulation of abstract interpretation [5, 14] would yield some interesting insights as well.

Appendix

A Proofs of Theorems

Lemma A.1 (Lemma 4.8) If ⟨P (t) | G(t)⟩⇝^{θ}⇝ ⋯ ⇝ NULL, then ⟨P | G⟩⇝^{(θt)}⇝ ⋯ ⇝ NULL.

Proof. We proceed by induction on the length of the SLD-proof. Consider the first resolution rule.

backchain Suppose

⟨P (t) | G(t)⟩ ⇝^{φπ,(tl_{cl}⇒G′)} ⟨P (t)(φπ) | tl_{cl}φ⟩⇝ ⋯ ⇝^{ψ}⇝NULL

where ψφπ = θ and (π, tl_{cl} ⇒ G′) ∈ κ(P (t)). Consider the diagram

π_{ρ}^{#}(P (t))  P (t)  P

[figure: ρ × σ; π_{ρ}; ρ; t; α]
[figure: t × id_{σ}; π_{α}]
α × σ

By the inductive definition of the pullback P (t), any (tl_{cl} ⇒ G′) ∈ κ(P (t)) must be of the form H(t × id_{σ}) ⇒ B′(t × id_{σ}) where (H ⇒ B′) ∈ κ(P). So the resolution sequence above is equivalent to

⟨P (t) | G(t)⟩ ⇝^{φπ_{ρ},(H(t×id_{σ})⇒B′(t×id_{σ}))} ⟨(π_{α}^{#}P)(t × id_{σ})φ | H(t × id_{σ})φ⟩⇝ ⋯ ⇝^{ψ}⇝NULL

But then

⟨P | G⟩ ⇝^{φ(t×id_{σ})π_{α},(H(t×id_{σ})⇒B′(t×id_{σ}))} ⟨(π_{α}^{#}P)(t × id_{σ})φ | H(t × id_{σ})φ⟩⇝ ⋯ ⇝^{ψ}⇝NULL

with computed answer substitution ψφ(t × id_{σ})π_{α} = ψφπ_{ρ}t = θt. augment Suppose ⟨P (t) | (A_{1} ⇒ A_{2})(t)⟩⇝ ⋯ ⇝^{θ}⇝NULL. By the inductive definition of pullback

then, this is

⟨P (t) | A_{1}(t) ⇒ A_{2}(t)⟩⇝⟨P (t) ∪ A_{1}(t) | A_{2}(t)⟩⇝ ⋯ ⇝^{θ}⇝NULL

By the induction hypothesis, ⟨P ∪ A_{1} | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL, so

⟨P | A_{1} ⇒ A_{2}⟩⇝⟨P ∪ A_{1} | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL

instance Suppose ⟨P (t) | (∃_{x:σ}A)(t)⟩⇝ ⋯ ⇝^{θ}⇝NULL. Then since

∃_{x:σ}(A(t × id_{σ})) = (∃_{x:σ}A)(t)  A
[figure: ρ × σ; t × id_{σ}; α × σ]
[figure: ρ; π_{α}, ∃; t; α; π_{α}, ∃]

and

π_{ρ}^{#}(P (t))  P (t)  P
[figure: ρ × σ; π_{ρ}; ρ; t; α]
[figure: t × id_{σ}; π_{α}]
α × σ

the resolution above must be of the form

⟨P (t) | (∃_{x:σ}A)(t)⟩ ⇝^{π_{ρ}} ⟨π_{ρ}^{#}(P (t)) = (π_{α}^{#}P)(t × id_{σ}) | A(t × id_{σ})⟩⇝ ⋯ ⇝^{⟨θ,β⟩}⇝NULL

for some β. By the induction hypothesis then since ⟨π_{ρ}^{#}(P (t)) = (π_{α}^{#}P)(t × id_{σ}) | A(t × id_{σ})⟩⇝ ⋯ ⇝^{⟨θ,β⟩}⇝NULL we have

⟨π_{α}^{#}P | A⟩⇝ ⋯ ⇝^{⟨θ,β⟩(t×id_{σ})}⇝NULL

and so

⟨P | ∃_{x:σ}A⟩ ⇝^{π_{α}} ⟨π_{α}^{#}P | A⟩⇝ ⋯ ⇝^{⟨θ,β⟩(t×id_{σ})}⇝NULL

with computed answer substitution ⟨θ, β⟩(t × id_{σ})(π_{α}) = θt.

and Suppose

⟨P (t) | (A_{1}(t) ∧ A_{2}(t))⟩⇝⟨P (t) | A_{1}(t)⟩ & ⟨P (t) | A_{2}(t)⟩⇝ ⋯ ⇝^{θ}⇝NULL

Then by the induction hypothesis,

⟨P | A_{1}⟩⇝ ⋯ ⇝^{θt}⇝NULL

and

⟨P | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL

Thus,

⟨P | (A_{1} ∧ A_{2})⟩⇝⟨P | A_{1}⟩ & ⟨P | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL

or-right Suppose

⟨P (t) | (A_{1}(t) ∨ A_{2}(t))⟩⇝⟨P (t) | A_{2}(t)⟩⇝ ⋯ ⇝^{θ}⇝NULL

Then by the induction hypothesis,

⟨P | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL

Thus

⟨P | (A_{1} ∨ A_{2})⟩⇝⟨P | A_{2}⟩⇝ ⋯ ⇝^{θt}⇝NULL

or-left Similarly.

□

Lemma A.2 (Lemma 4.9) P ⊢_{o} G iff there is an SLD-proof ⟨P | G⟩⇝^{id}⇝ ⋯ ⇝ NULL with computed answer substitution id.

Proof. That an SLD-proof of the form ⟨P | G⟩⇝^{id}⇝ ⋯ ⇝ NULL implies that P ⊢_{o} G is immediate by definition.

Suppose P ⊢_{o} G. Then there is a program Q and a formula H such that ⟨Q | H⟩⇝^{θ}⇝ ⋯ ⇝ NULL, P = Qθ and G = Hθ. We proceed by induction on the length of this SLD-proof. Consider the first resolution rule.

backchain Suppose

⟨Q | H⟩ ⇝^{φπ,(tl_{cl}⇒H′)} ⟨Q(φπ) | tl_{cl}φ⟩⇝ ⋯ ⇝^{ψ}⇝NULL

where

ρ
[figure: θ]
β^{ψ}  α
[figure: π_{α}]
α × σ^{φ}

which implies in particular that ψφ = ⟨θ, f⟩ for some f : ρ → σ, and where (tl_{cl} ⇒ H′) ∈ κ(Q). By the induction hypothesis, we have that

⟨(Q(φπ))ψ | (tl_{cl}φ)ψ⟩⇝ ⋯ ⇝^{id}⇝NULL

And by considering the following diagram

ρ
[figure: id; π_{ρ}; θ]
ρ \overline{\begin{matrix}⟨id, f⟩ \\  \end{matrix}}ρ × σ  α
[figure: ⟨θ, f⟩; θ × id; π_{α}]
α × σ

we have also that (Q(φπ_{α}))ψ = Q(ψφπ_{α}) = Qθ = P = P (⟨id, f⟩π_{ρ}) = (π_{ρ}^{#}P)⟨id, f⟩, as well as (tl_{cl}φ)ψ = tl_{cl}(ψφ) = tl_{cl}⟨θ, f⟩ = (tl_{cl}(θ × id))⟨id, f⟩. So

⟨(π_{ρ}^{#}P)⟨id, f⟩ | (tl_{cl}(θ × id))⟨id, f⟩⟩⇝ ⋯ ⇝^{id}⇝NULL

and since (tl_{cl} ⇒ H′) ∈ κ(Q) also implies by the inductive definition of pullback that (tl_{cl}(θ × id) ⇒ H′(θ × id)) ∈ κ(Qθ = P) we have

⟨P | G⟩ ⇝^{⟨id,f⟩π_{ρ}=id,tl_{cl}(θ×id)⇒H′(θ×id)} ⟨(π_{ρ}^{#}P)⟨id, f⟩ | (tl_{cl}(θ × id))⟨id, f⟩⟩⇝ ⋯ ⇝^{id}⇝NULL

with computed answer substitution id.

augment Suppose

⟨Q | H_{1} ⇒ H_{2}⟩⇝⟨Q ∪ H_{1} | H_{2}⟩⇝ ⋯ ⇝^{θ}⇝NULL

Then by the induction hypothesis,

⟨P ∪ G_{1} | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

and so

⟨P | G_{1} ⇒ G_{2}⟩⇝⟨P ∪ G_{1} | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

instance Suppose

⟨Q | ∃_{x:σ}H⟩ ⇝^{π_{α}} ⟨(π^{#}Q) | H⟩⇝ ⋯ ⇝^{ψ}⇝NULL

where the computed answer substitution is ψπ_{α} = θ (and so ψ = ⟨θ, δ⟩ for some arrow δ : ρ → σ) and

G  H

[figure: ρ × σ; θ × id_{σ}; α × σ]

[figure: ρ; π_{ρ}, ∃; θ; α; π_{α}, ∃]

By the induction hypothesis,

⟨P | Hψ⟩⇝ ⋯ ⇝^{id}⇝NULL

But since P = (π^{#}P)⟨id_{ρ}, δ⟩ and Hψ = H⟨θ, δ⟩ = (H(θ × id_{σ}))(⟨id_{ρ}, δ⟩) = G⟨id_{ρ}, δ⟩ this is equivalent to

⟨(π^{#}P)⟨id_{ρ}, δ⟩ | G⟨id_{ρ}, δ⟩⟩⇝ ⋯ ⇝^{id}⇝NULL

Then, by lemma 4.8 we have

⟨P | ∃_{x:σ}G⟩ ⇝^{π_{ρ}} ⟨π_{ρ}^{#}P | G⟩⇝ ⋯ ⇝^{⟨id_{ρ},δ⟩}⇝NULL

with computed answer substitution id.

and Suppose

⟨Q | H_{1} ∧ H_{2}⟩⇝⟨Q | H_{1}⟩ & ⟨Q | H_{2}⟩⇝ ⋯ ⇝^{θ}⇝NULL

Then by the induction hypothesis,

⟨P | G_{1}⟩⇝ ⋯ ⇝^{id}⇝NULL

and

⟨P | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

Thus

⟨P | G_{1} ∧ G_{2}⟩⇝⟨P | G_{1}⟩ & ⟨P | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

or-right Suppose

⟨Q | H_{1} ∨ H_{2}⟩⇝⟨Q | H_{2}⟩⇝ ⋯ ⇝^{θ}⇝NULL

Then by the induction hypothesis,

⟨P | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

and so

⟨P | G_{1} ∨ G_{2}⟩⇝⟨P | G_{2}⟩⇝ ⋯ ⇝^{id}⇝NULL

or-left Similarly.

□

Lemma A.3 (Lemma 5.11) [[X_{i}(tv) ]]_{P (t)}^{n} is an isomorphism iff ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}) is an isomorphism.

Proof. We proceed by induction on n. The case n=0 is trivial.

First, suppose ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}) is an isomorphism, where P is of sort ρ, X_{i} of sort σ, v is an arrow from ρ to σ and t is necessarily an arrow whose target is ρ and whose source is, say, η (see diagram below).

This means that for some pair (π_{1}, B ⇒ X_{i}(u)) ∈ κ(P) and some substitution θ such that θπ_{1}v = θu, ( [[t]])^{#}(Im_{[[θ]]π_{1}}( [[θ]])^{#} [[B]]_{P π_{1}}^{n−1}) is an iso. By proposition 5.8 there is a substitution φ such that t = φθπ_{1} and such that [[φ]] factors through ( [[θ]])^{#} [[B]]_{P π_{1}}^{n−1}. Thus ( [[φθ]])^{#} [[B]]_{P π_{1}}^{n−1} is an iso, and by the induction hypothesis, so is [[B(φθ) ]]_{P φθπ_{1}}^{n−1}.

The reader should note that if P is of sort ρ and the clause B ⇒ X_{i}(u) of sort ρ × μ is in κ(P) then

• P (t) is of sort η.

• The corresponding clause in κ(P (t)) is (ℓ, B(⟨ℓt, r⟩) ⇒ X_{i}(⟨ℓt, r⟩u)) of sort η × μ, as it is the result of stripping quantifiers off of some formula diagram in P (t) along a projection ℓ.

• A unifier γ of the head of this clause and the appropriately extended goal formula X_{i}(ℓtv) of sort η × μ must be targeted at η × μ and satisfy γ⟨ℓt, r⟩u = γ⟨ℓt, r⟩π_{1}v

as shown in the diagram below (where two triangles fail to commute: ⟨ℓt, r⟩ ≠ ℓφθ and u ≠ π_{1}v)

X_{i}(⟨ℓt, r⟩u)  X_{i}(u)  B
[figure: ⇐]
[figure]
⟨P | X_{i}(v)⟩

[figure: γ; η × μ; ⟨ℓt, r⟩; ρ × μ; u; σ] [figure: ψ; θ; v]

.

[figure: φ] [figure: η; ℓ; t; ρ; π_{1}]

Now we consider [[X_{i}(tv) ]]_{P (t)}^{n} which, by definition, is

⋃_{{(ℓ, B(⟨ℓt, r⟩) ⇒ X_{i}(⟨ℓt, r⟩u)) ∈ κ(P (t)) \atop γ⟨ℓt,r⟩u=γ⟨ℓt,r⟩π_{1}v}} \{Im_{[[ℓ]]}Im_{[[γ]]}( [[γ]])^{#}( [[B(⟨ℓt, r⟩) ]]_{P (ℓt)}^{n−1})\}  (7)

One of the members of this union is that for which γ is the arrow η ^{⟨id_{η},φθπ_{0}⟩} η × μ where η ^{φθ} ρ × μ ^{π_{0}} μ since

γ⟨ℓt, r⟩ = ⟨t, φθπ_{0}⟩
= ⟨φθπ_{1}, φθπ_{0}⟩
= φθ

and we have shown that θπ_{1}v = θu. Also observe that γℓ is the identity id_{η}.

Now recall that we had concluded above (from consideration of the fact that ( [[t]])^{#}( [[X(v) ]]_{P}^{n}) is an isomorphism) that [[B(φθ) ]]_{P (φθπ_{1})}^{n−1} is an iso. Since γ⟨ℓt, r⟩ = φθ, we have that [[Bγ⟨ℓt, r⟩]]_{P (γ⟨ℓt,r⟩π_{1})}^{n−1} is an iso. Using the induction hypothesis again, we may conclude that ( [[γ]])^{#} [[B⟨ℓt, r⟩]]_{P (ℓt)}^{n−1} is an iso.

But then, since γℓ is the identity id_{η}, we have that

Im_{[[γℓ]]}( [[γ]])^{#}( [[B⟨ℓt, r⟩]]_{P (ℓt)}^{n−1})

is also an iso. This is a member of the union in (7), so the union is an isomorphism, and thus so is [[X(tv) ]]_{P (t)}^{n}.

For the other direction, we refer to the same diagram above. Suppose [[X(tv) ]]_{P (t)}^{n} is an isomorphism. This means id_{[[η]]} factors through it, and so through

Im_{[[γℓ]]}( [[γ]])^{#}( [[B⟨ℓt, r⟩]]_{P (ℓt)}^{n−1})

for some substitution-clause pair (ℓ, B(⟨ℓt, r⟩) ⇒ X_{i}(⟨ℓt, r⟩u)) in κ(P (t)) where γ⟨ℓt, r⟩u = γ⟨ℓt, r⟩π_{1}v. Thus by proposition 5.8, there is a substitution ψ from η to the source of γ such that

• id_{η} = ψγℓ, and

• ( [[ψγ]])^{#}( [[B⟨ℓt, r⟩]]_{P (ℓt)}^{n−1}) is an iso.

Using the induction hypothesis this yields

[[Bψγ⟨ℓt, r⟩]]_{P (ψγℓt)}^{n−1}  is an iso .  (8)

Now we wish to show that

( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}) = ⋃_{{θπ_{1}v = θu \atop (π_{1},B⇒X_{i}(u))∈κ(P)}} \{( [[t]])^{#}(Im_{[[π_{1} ]]}Im_{[[θ]]}( [[θ]])^{#}( [[B]]_{P π_{1}}^{n−1}))\}  (9)

is an isomorphism. Consider the member of the union corresponding to the clause B ⇒ X_{i}(u) and with the substitution θ chosen to be ψγ⟨ℓt, r⟩ (taking φ to be the identity on η in the diagram). We have θπ_{1} = ψγℓt, so from (8) we infer that [[Bθ]]_{P θπ_{1}}^{n−1} is an iso. By the induction hypothesis again we have ( [[θ]])^{#}( [[B]]_{P π_{1}}^{n−1}) is an iso. Furthermore, since id_{η} = ψγℓ, we have

Im_{[[π_{1} ]]}Im_{[[θ]]} = Im_{[[θπ_{1} ]]}
= Im_{[[ψγℓt]]}
= Im_{[[t]]}

Thus the member of the union in (9) corresponding to this clause and substitution, ie:

( [[t]])^{#}Im_{[[π_{1} ]]}Im_{[[θ]]}( [[θ]])^{#}( [[B]]_{P π_{1}}^{n−1})

reduces to ( [[t]])^{#}Im_{[[t]]}( [[θ]])^{#}( [[B]]_{P π_{1}}^{n−1}). Now, since for any subobject F and (suitably targeted) arrow f, F ⊂ (f)^{#}Im_{f}(F), this member of the union is an isomorphism, and thus so is ( [[t]])^{#}( [[X_{i}(v) ]]_{P}^{n}). □

Theorem A.4 (Theorem 5.13)

E(P, [[ ]], X_{i}, v) = ⋃_{(π, cl) ∈ κ(P)_{hd_{cl}=X_{i}}}{Im_{[[π]]}Imeq( [[πv]], [[_{tm_{cl}}]])(eq( [[πv]], [[tm_{cl}]]))^{#} [[tl_{cl}]]_{P π}^{n−1}}

Proof. We establish that for any arrows u, t with same source (say σ) and target, and any subobject F of [[σ]]

Imeq( [[u]], [[t]])(eq( [[u]], [[t]]))^{#}(F) = ⋃_{θu=θt} Im_{[[θ]]}( [[θ]])^{#}(F).  (10)

from which the theorem follows easily.

We will need to be careful with notation here: we let \overline{eq( [[u]], [[t]])} denote the equalizer object, and e the monic eq( [[u]], [[t]]) from the equalizer to the source σ of the equalized arrows.

We begin by observing that, as with any object in Set^{ℂ^{o}}, \overline{eq( [[u]], [[t]])} is the colimit of a family of representable objects [[ε_{α}]], each equipped with a map f_{α} into \overline{eq( [[u]], [[t]])}.

[figure: [[ε_{α}]]; f_{α}; \overline{eq( [[u]], [[t]])}; e; σ; [[u]]; [[t]]]

For each α, the composition f_{α}e has representable source and target. Since the Yoneda embedding is full, each one is the image [[θ]] of some arrow θ in ℂ which must be a unifier of u and t as the reader can check. We now omit all reference to the objects [[ε_{α}]] and use the label ι_{θ} for the arrows f_{α} from the source of each [[θ]] into \overline{eq( [[u]], [[t]])}. This information is displayed in the diagram below, together with the epi-mono image factorization of [[θ]]

[figure: \overline{eq( [[u]], [[t]])}; e; σ; [[u]]; [[t]]]
[figure: ι_{θ}; .; [[θ]]]
[figure: .; u_{θ}; Im_{[[θ]]}(id); j_{θ}]

It is straightforward to show, using the universal properties of equalizers, colimits and unions, that e, whose source is by hypothesis the colimit of the objects that are the sources of the [[θ]], is equal, as a subobject of σ, to the union ⋃ j_{θ}.

Making use of this fact we have, for any subobject F of σ,

Im_{e}(e)^{#}(F) = Im_{⋃ j_{θ}}(⋃ j_{θ})^{#}(F)

Note that if a and b are any subobjects of an object σ

a ∩ b = Im_{a}(a)^{#}(b)  (11)

so Im_{⋃ j_{θ}}(⋃ j_{θ})^{#}(F) is precisely the intersection

(⋃ j_{θ}) ∩ F

which distributes in the co-complete topos Set^{ℂ^{o}} to yield

⋃(j_{θ} ∩ F).

Using fact (11) again, we obtain

⋃ Im_{j_{θ}}(j_{θ})^{#}(F)

It follows that

Im_{e}(e)^{#}(F) = ⋃ Im_{j_{θ}}(j_{θ})^{#}(F).

Observe, however, that

Im_{[[θ]]}( [[θ]])^{#}(F)
= Im_{u_{θ}j_{θ}}(u_{θ}j_{θ})^{#}(F)
= Im_{j_{θ}}Im_{u_{θ}}(u_{θ})^{#}(j_{θ})^{#}(F)
= Im_{j_{θ}}(j_{θ})^{#}(F)

the last equation following from the fact that the composition Im_{u_{θ}}(u_{θ})^{#} yields identity since u_{θ} is epic. This estabishes the identity (10) above.

Now letting F be [[tl_{cl}]]_{P π} and taking the arrow t to be πv we conclude that

Imeq( [[πv]], [[u]])(eq( [[πv]], [[u]]))^{#}( [[tl_{cl}]]_{P π}) = ⋃_{θu=θπv}{Im_{[[θ]]}( [[θ]])^{#}( [[tl_{cl}]]_{P})}.

Applying the image functor Im_{[[π]]} to both sides (and observing that it commutes with unions), the theorem follows readily. □

B A Sketch of the Grothendieck Construction

An indexed category I over a base category ℂ is a ℂ -indexed family of categories (the fibers), together with a functor If between fibers Iσ and Iρ associated with every arrow σ ^{f} ρ in the base category. By such a device we resolve logic and logic programing structure into a (vertical) propositional logical component (the structure in the fibers) and the (horizontal) predicate logic and substitution component, which, as it turns out, is a special case of state change in logic programming. We have seen that the base category may also capture change of ambient program in the Weak Hereditarily Harrop case.

But logic program resolutions act on state-goal pairs, or vectors of such. So actual resolution steps do not correspond to any arrows in the indexed category framework: they are paths consisting of arrows in the fibers followed by shifts along reindexing functors. This problem can be remedied by a simple, elegant construction due to Grothendieck that builds a single category out of an indexed category, indeed, a category together with a functor into the base category, called a fibration (or op-fibration if the indexed category is covariant). This construction allows us to visualize quite intricate logic programming resolutions in conventional or extended logic programming as automatically generated by a simple core of data: program clauses in the fibers and state change definitions in the base of an indexed category.

In this paper we have also shown how a category ℂ [X] of freely generated (generic) predicates over a base category arises as a result of the Grothendieck construction over basic (propositional) data presented in an indexed category Πb.

Definition B.1 Given an indexed category I : ℂ ℂ𝔸𝕋, the category G(ℂ , I) is defined as follows

objects: pairs (σ, G) where σ ∈ |ℂ | and G ∈ |Iσ|.

arrows: pairs (θ, u) : (σ, G) (ρ, K) where σ ^{θ} ρ is an arrow in the base category ℂ and Iθ(K) ^{u} G an arrow in the fiber I(σ).

Composition

(σ, G) ^{(θ,u)} (ρ, K ^{(φ,v)} )(α, V)

is given by the pair (θφ, Iθ(v)u), the second component of which is the composition

Iθ(Iφ(V)) ^{Iθ(v)} Iθ(U) ^{u} G.

We refer the reader to the exposition in [6] for a proof of the fact that G(ℂ , I) is category which, together with projection functor G(ℂ , I) ⟶ ℂ yields a split fibration, and that this correspondence induces an equivalence of the categories of indexed categories and split fibrations.

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] Gianluca Amato. Sequent Calculus and Indexed Categories as Foundations for Logic Programming. PhD thesis, University of Pisa, 2000.

[3] Gianluca Amato and James Lipton. Indexed categories and bottom-up semantics of logic programing. In Proceedings of LPAR ’01, volume 2250 of Lecture Notes in Artificial Intelligence, 2002.

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

[5] R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics based, bottom-up abstract interpretation of logic programs. ACM Transactions on Programming Languages and Systems, 15(1):133–181, 1993.

[6] Michael Barr and Charles Wells. Category Theory for Computing Science. Prentice Hall, 1995.

[7] N. Benton, G. Bierman, V. de Paiva, and J.M.E. Hyland. Term assignment for intuitionistic linear logic. In Proc. CSL ’92, 1993.

[8] A. Bossi, M. Gabrielli, G. Levi, and M. C. Meo. A compositional semantics for logic programs. Theoretical Computer Science, 122(1-2):3–47, 1994.

[9] Jawahar Chirimar. Proof Theoretic Approach to Specification Languages. PhD thesis, University of Pennsylvania, 1995.

[10] Jacques Cohen. Constraint logic programming languages. Communications of the ACM, 33(7):52–68, July 1990.

[11] M. Comini, C. Meo, and G. Levi. A theory of observables in logic programming. Information and Computation, 169(1):23–80, 2000.

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

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

[14] Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming, 13(2-3):103–179, July 1992.

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

[16] Oege de Moor. Categories, Relations, and Dynamic Programming. PhD thesis, St. John’s College, Oxford, 1991.

[17] M. DeMarco. Higher Order Logic Programming in the Theory of Types. PhD thesis, Wesleyan University, 1999.

[18] M. DeMarco and J. Lipton. The semantics of higher order hereditary harrop logic programming. To appear.

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

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

[21] P. Freyd, P. Mulry, G. Rosolini, and D. Scott. Extensional PERs. Information and Computation, 98(2)::211–227, 1992.

[22] Peter Freyd. The logic of cartesian categries. To appear.

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

[24] J.Y. Girard. On the unity of logic. Annals of Pure and Applied Logic, 59:201–217, 1993.

[25] J.Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1998.

[26] J. Harland and D. Pym. A uniform proof-theoretic investigation of linear logic programming. Journal of Logic and Computation, 4(2), 1994.

[27] Claudio Hermida. Fibrations,logical predicates and indeterminates. PhD thesis, University of Edinburgh, 1993.

[28] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327–365, May 1994.

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

[30] Joxan Jaffar and Michael Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503–581, 1994.

[31] Neil D. Jones. Abstract interpretation and partial evaluation in functional and logic programming. In Maurice Bruynooghe, editor, Logic Programming. Proceedings of the 1994 International Symposium, pages 17–22. The MIT Press, 1994.

[32] T. K. Lakshman and Uday S. Reddy. Typed Prolog: A semantic reconstruction of the Mycroft-O’Keefe type system. In Proceedings of the 1991 IEEE Symposium on Logic Programming, pages 202–220, 1991.

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

[34] Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic. Springer-Verlag, 1992.

[35] J. L. Lassez and K. MacAloon. A constraint sequent calculus. In Proceedings of tthe 5th Symp. on LICS, 1990.

[36] G. Levi. Models, unfolding rules, and fixpoint semantics. In R.A. Kowalski and K. A. Bowen, editors, Proc. Fifth International Symposium of Logic Programming. The MIT Press, 1988.

[37] J. Lipton and R. McGrail. Encapsulating data in logic programming via categorical constraints. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming, volume 1490 of LNCS. Springer Verlag, 1998.

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

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

[40] M. Martelli M. Falaschi, G. Levi and C. Palamidessi. A model-theoretic reconstruction of the operational semantics of logic programs. Information and Computation, 102(1):86–113, 1993.

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

[42] R. McGrail. Monads and Control in Logic Programming. PhD thesis, Wesleyan University, 1997.

[43] Maria Chiara Meo. A Framework for Reasoning about the Semantics of Logic Programs. PhD thesis, University of Pisa, 1996.

[44] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, pages 79–108, 1989.

[45] Dale Miller. A multiple-conclusion meta-logic. In Proceedings of the 1994 Symposium on Logics in Computer Science, pages 272–281, 1994.

[46] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51(1-2):125–157, 1991.

[47] E. Moggi. Notions of computation and monads. Information and Computation, 93, 1991.

[48] J. J. Moreno-Navarro and M. Rodríguez Artalejo. Logic programming with functiona and predicates: The language babel. The Journal of Logic Programming, 12(3/4):191–223, 1992.

[49] A. Mycroft and R. A. O’Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence, 23(3):295–307, 1984.

[50] Gopalan Nadathur and Dale Miller. Higher-order horn clauses. Journal of the ACM, 37(4):777–814, 1990.

[51] Gopalan Nadathur and Dale Miller. Higher-order logic programming. In Handbook of Logics for Artificial Intelligence and Logic Programming, volume 5. Oxford University Press, 1996.

[52] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. Technical report, Syracuse University, 1993.

[53] L. Ong. Non-determinism in functional programming. In Proceedings of the 8th IEEE Symposium on Logic and Computer Science, 1993.

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

[55] Frank Pfenning. Types in Logic Programming, chapter Dependent Types in Logic Programming. MIT, 1992.

[56] David Pitt, Samson Abramsky, Axel Poigne, and David Rydeheard, editors. Category Theory and Computer Programming. Springer-Verlag, New York, 1985. Lecture Notes in Computer Science 240.

[57] G. Plotkin and J. Reynolds. Logical Foundations of Functional Programming, chapter On functors expressible in the polymorphic lambda calculus. Addison-Wesley, 1990.

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

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

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

[61] D.E. Rydeheard and R.M. Burstall. A categorical unification algorithm. In Category Theory and Computer Programming, volume 240 of LNCS, pages 493–505, 1985.

[62] M. Spivey. A functional theory of exceptions. Science of Computer Programming, 14(1):25–42, 1990.

[63] T. Streicher. Semantics of Type Theory. Birkhäuser, 1992.

[64] P. J. Stuckey. Negation and constraint logic programming. Information and Computation, 118, 1995.

[65] Paul Taylor. Practical Foundations of Mathematics. Cambridge University Press, 1999.

[66] A. S. Troelstra and D. van Dalen. Constructivism in Mathematics: An Introduction, volume 2. Elsevier Science Publishers, 1988.

[67] M. H. van Emden and R. A. Kowalski. The semantics of predicate logic as a programming language. Journal of the ACM, 23, 1976.

[68] P. Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2, 1992.

[69] P. Wadler. How to declare an imperative. In Proc.International Logic Programming Symposium. MIT Press, 1995.