Some Notes on Logic Programming with a Relational Machine

Extended Abstract

James Lipton Dept. of Mathematics Wesleyan University

Emily Chapman Dept. of Mathematics Wesleyan University

Abstract We study the use of relation calculi for compilation and execution of Horn Clause programs with

an extended notion of input and output. We consider various other extensions to the Prolog core.

0 Introduction

Logic programming is programming with predicates in a certain fragment of logic. More broadly speaking, it is programming with executable specifications: code that has independent mathematical meaning consistent with its input-output behavior. Specifications are often formalized as relations. In this paper we explore how Logic Programming itself may be profitably understood, extended and compiled in terms of an underlying equational relational calculus, in which relation variables play a fundamental role, similar in some regards to the role of function variables in the lambda-calculus. The variables in the resulting terms correspond to predicate (second order) variables in the original program, whereas all first order variables are eliminated. Subsequent abstraction provides closed form solutions to all the program predicates.

In this study we use the relation algebra formalism as an executable algebra of logic programs, somewhat in the Backus tradition[Backus]. Our approach here, as in [BroLip, Colp] is to translate logic programs into combinatory relation expressions, which are then executed via rewriting and output-formatting algorithms. It will be useful to illustrate our intentions here with an example.

Consider the following Horn Clause program defining the transitive closure of a graph

             conn(X,X).
             conn(X,Y):-edge(X,Z),conn(Z,Y).

                                                          edge(a,b). edge(b,c). edge(a,l). edge(l,c).

and the queries

      | ?- conn(a,c).
      | ?- conn(X,c).

This rather carefully chosen example can be easily reformulated in first-order-variable-free relational terms as follows. We introduce the binary relation variables conn and edge and translate the program into a pair of relation equations. Composition of relations is denoted by “ ; ”.

edge = {(a, b), (b, c), (a, l), (l, c)}
conn = id ∪ (edge; conn)

where id denotes the identity relation. The queries are then represented by the relation expressions:

{(a, c)} ∩ conn and (1; {(c, c)}) ∩ conn

where 1 is the universal relation H × H and H is the set of closed terms in the program signature (hence (1; {(c, c)}) represents the set of all pairs whose second component is c).

Some questions that arise naturally at this point are: can such a translation be defined for an arbitrary Horn Clause program, or even for extensions of conventional programs, what kind of relation calculus is suitable for it, and can the resulting relational expressions be easily executed, controlled and optimised?

The aim of these notes is to sketch out in some detail a relation calculus, a translation, a semantics and a rewriting system that give evidence for an affirmative answer to these questions. The relational abstract machine sketched here is described in detail in [Chap, Ruhlen]^{1}.

A translation that will work for all Horn Clause programs (with equality) is necessarily a bit more involved than the one just shown. The one presented here draws on foundational ideas of Tarski, Givant, Freyd, Maddux, and Broome that have appeared at different times in the relational and allegory-theoretic literature although it is different from all of them in that is it aimed at producing executable intermediate relational code. Our work thus builds computation into the relational formalism, and shows how the relation calculus offers a new vehicle for proof search and automated deduction as well.

In the earlier paper [BroLip] cited, the authors showed how the existence of a logically correct executable translation of Horn clause programs follows from results of Tarski and others, and explored other “pure” relational programming formalisms. Here that work is considerably refined, and a simple rewriting system explicitly written out and shown correct.

Combinatory approaches to logic programming have appeared elsewhere in the literature: Bellia and Occhiuto develop an algebra of programs that captures unification, rewriting and narrowing in [BelOcc]. Our contribution is to define a more expressive algebra of logic programs, which admits first-order queries, extensions to equational logic, negation and higher order logic, as well as to show that such an algebra can be found within the relation calculus, a well-understood mathematical formalism which easily incorporates other programming paradigms.

A great deal of work has been done in specification refinement using relational specifications based on Hoare’s work [Algebra, Naumann, Backh], as well as on relational approaches to hardware design [BroHut, JonShe, BroJon]. In light of this work, the relational translation described here may provide a new formal link between logic programming, hardware specification, and program synthesis.

The work presented here also owes a substantial debt to the logic program transformation ideas of Clark [Lloyd] and Warren [WAM].

1 A Relation Calculus for Horn Clause Programming

In the following sections we formalize a relational theory and a class of relational structures suitable as a target compilation language for logic programs. The relational theory is close in spirit to the positive fragment of the untyped μ-relation calculus MU introduced by deRoever (see e.g. [deRoe, BakRoe, FriasMad]) with additional equations that capture unification requirements over the Herbrand Universe.

1.1 A Language and meta-language for Horn-clause programming

We begin by fixing a first-order signature for a Horn Clause program

Σ = C_{Σ} ∪ F_{Σ},

where C_{Σ} is the set of constant symbols of Σ and F_{Σ} the set of function symbols. We let α(f) denote the arity of the function symbol f. Let T_{Σ} be the set of closed terms over Σ. We fix a countable set of variables X (not to be confused with relation variables introduced in a later section) and let T_{Σ}(X) be the set of open terms over X.

Pairing

We will need to formalize an object-level pairing function, in order to account for the coding of vectors of terms in our relational language, that is to say, explicit vectors of terms manipulated by the compiler.

1The machine has been implemented in SWI-Prolog. Check http://www.cs.wesleyan.edu/~lipton for details.

This is done by adding a second, top-level tier to our concept of term and signature.

Many efficiencies in the translation of n-ary predicates to binary relations are achieved by working with relations that stand for pairs of vectors of length at least n, rather than those of length exactly n, since this permits dynamic expansion of arities on demand. By this device we are able to compile programs independently of queries, which may introduce an unpredictable number of new variables. This dictates certain choices of notation and conventions, such as associating pairs to the right (like simple type expressions).

We define the set of [Σ-closed] extended terms over Σ by letting Σ^{+} be the signature with constants given by all [closed] terms over Σ together with the binary function symbol

[ , ].

A Σ-open or Σ-closed extended term is a closed term over this meta-signature, built up from Σ-terms that are open or closed. In other words, we abuse language, and let closed or open refer to the bottom-tier terms that occur in our pairs. We will never need top-tier variables. Spelling it out via an inductive definition:

Definition 1.1 Let Σ be a signature and T_{Σ} the set of terms over Σ. Then the set T_{Σ}^{+}of extended terms is defined as follows:

1. If u is a [closed] term over Σ it is a [Σ-closed] extended term.

2. If u_{1}, u_{2} are [Σ-closed] extended terms then so is [u_{1}, u_{2}].

Henceforth open or closed extended term will mean Σ-open or Σ-closed.

Formal vectors and concatenation.

The presence of a formal pairing operator [ , ] in T_{Σ}^{+} allows us to define an internal product of terms within the collection of extended terms. This pairing operator associates to the right, so that we will write, for example

[t1, t2, t3, t4] for [t_{1}, [t_{2}, [t_{3}, t_{4}]]]

which we can think of as a formal vector of terms. If u is the extended term [u_{1}, u_{2}, …, u_{n}], and x is an extended term, we write ux to denote the extended term

[u_{1}, u_{2}, …, u_{n}, x].

Thus every extended term u can be assigned a length n and components u_{1}, …, u_{n} as follows:

Definition 1.2 An extended term t has length 1 if it is a Σ-term, and length n+1 if it is of the form ux, where x is not extended, and u is [u_{1}, u_{2}, …, u_{n}]. We write ∥ u ∥ for the length of u and call [u_{1}, u_{2}, …, u_{n}] the formal vector representation of u and u_{i} the ith component of u.

Note that, in general, if u is an extended term of the form [u_{1}, u_{2}, …, u_{n}], it is a formal vector of length at least n (since u_{n} may be an extended term). If x is a Σ-term and u, v and extended terms ∥ x ∥= 1 and ∥ uv ∥=∥ u ∥ + ∥ v ∥.

We now associate to each signature Σ a relation calculus RelΣ into which we will carry out a translation of both language and metalanguage. Among the atomic relation expressions in the calculus will be the n relation symbols f_{i}^{n} (1 ≤ i ≤ n) for each function symbol of arity n in Σ, formalizing the relation of projection of each term of the form f(u_{1}, …, u_{n}) onto its i-th subterm, and the relation symbol (a, a) for each constant a of Σ.

The relation expression (a, a) is a formal counterpart to the singleton relation {(a, a)}. The hd and tl relation expressions are formal projections corresponding to the pairing operator in the meta-signature Σ^{+}.

1.2 Relational Syntax

Definition 1.3 Let R_{var} be a countable set of relation variables. The relation calculus RelΣ has the following syntax. The atomic relation expressions are defined by

⟨R_{atom}⟩ ::= ⟨R_{var}⟩ | id | di | 1 | 0 | hd | tl | ⟨R_{Σ}⟩

where R_{Σ} is the set of relation constants consisting of all expressions {f_{i}^{n} : f ∈ F_{Σ}, α(f) = n, 1 ≤ i ≤ n} and {(a, a) : a ∈ C_{Σ}}. Compound expressions are given by the following BNF grammar:

R ::= ⟨R_{atom}⟩ | R^{o} | R ∪ R | R ∩ R | RR | fp⟨R_{var}⟩.(R)

Juxtaposition RR means composition, which we will sometimes write R; R using the infix operator “;” to enhance legibility. Powers R^{(n)} denote iterations of composition. We denote by ℜ_{Σ} the open terms (relation expressions) over the variables R_{var}. When the underlying signature is clear from context we will write ℜ for this set of terms. We will say a term is recursion-free if it contains no occurrences of fp.

Certain compound relation expressions will play an especially important role in the calculus, so we introduce them here.

Definition 1.4 Define the countable sequence {P_{i} : 1 ≤ i} of projection relations as follows:

P_{1} = hd  P_{2} = tl; hd  ⋯  P_{n} = (tl)^{(n−1)}; hd  ⋯  (1)

In the standard semantics to be discussed below, P_{i} is a relation between a formal vector with at least i + 1 components and its i-th component. That is to say, P_{i}’s set-theoretic interpretation consists of pairs of formal vectors (u, u_{i}).

Definition 1.5 The relation of partial identity up to the first n components on vectors of length at least n + 1 is defined as follows:

I_{n} := ⋂_{1≤i≤n} P_{i}(P_{i})^{o}  (2)

We also define the relation of true identity on such vectors by

id_{n} := ( ⋂_{1≤i≤n} P_{i}(P_{i})^{o}) ∩ tl^{n}(tl^{n})^{o}.  (3)

id_{n} is a subrelation of the identity relation id as a consequence of the equational theory we will define below and, of course, also in the standard semantics.

Definition 1.6 We also define the relation of identity on f-terms for f a function symbol of arity n in the signature Σ by

id_{f} := ⋂_{1≤i≤n} f_{i}^{n}(f_{i}^{n})^{o}

In the standard interpretation, id_{f} will denote the set of identical pairs of terms beginning with the function symbol f.

Finally, for each pair of ground terms t_{1}, t_{2} over Σ, define the formal relation expression (t_{1}, t_{2}), (whose semantics will be the singleton {(t_{1}, t_{2})}), as follows:

(a, a) := already defined  (4)
(f(u_{1}, …, u_{n}), f(u_{1}, …, u_{n})) := ⋂_{1≤i≤n} f_{i}^{n}(u_{i}, u_{i})(f_{i}^{n})^{o}  (5)
(t_{1}, t_{2}) := (t_{1}, t_{1})1(t_{2}, t_{2})  (6)

It is often convenient to work in a derived relational structure where the formal relations (t_{1}, t_{2}) are new primitives, satisfying the preceding equations. We will not make use of this variant here.

The reader should also note that unlike id_{n}, I_{n} is not a subrelation of the identity relation. In the standard set-theoretic interpretation to be defined below, it will denote all pairs of vectors (ux, uy), with u of length n.

1.3 The Equational Theory RelΣ

We will be using an equational theory which captures the general properties of relations we need as well as the behavior of the encoding of the structure of a Σ-term algebra. We therefore break it down into two components, one we will call DRA, the theory of distributive relation algebras, and the other RΣ. The latter theory is quite domain specific. It is the part we would expect to change to capture constraint logic programming over other domains, although this matter will not be taken up here.

Note that the containment A ⊆ B abbreviates the equation A ∩ B = B.

DRA ; \begin{matrix}R ∩ R = R  R ∩ S = S ∩ R  R ∩ (S ∩ T) = (R ∩ S) ∩ T \\ R id = R  R0 = 0  0 ⊆ R ⊆ 1 \\ R ∪ R = R  R ∪ S = S ∪ R  R ∪ (S ∪ T) = (R ∪ S) ∪ T \\ R ∪ (S ∩ R) = R = (R ∪ S) ∩ R \\ R(S ∪ T) = RS ∪ RT  (S ∪ T)R = SR ∪ T R \\ R ∩ (S ∪ T) = (R ∩ S) ∪ (R ∩ T) \\ (R ∪ S)^{o} = R^{o} ∪ S^{o}  (R ∩ S)^{o} = S^{o} ∩ R^{o} \\ R^{∘∘} = R  (RS)^{o} = S^{o}R^{o} \\ R(S ∩ T) ⊆ RS ∩ RT  RS ∩ T ⊆ (R ∩ T S^{o})S \\ id ∪ di = 1  id ∩ di = 0 \end{matrix} ; RΣ ; \begin{matrix}1(a, a)1 = 1  (a, a)R(a, a) = (a, a) ∩ R  (a, a) ⊆ id \\ hd(hd)^{o} ∩ tl(tl)^{o} ⊆ id  (hd)^{o}hd = (tl)^{o}tl = id  (hd)^{o}tl = 1 \\ id_{f} ≡ ⋂_{1≤i≤n} f_{i}^{n}(f_{i}^{n})^{o} ⊆ id  (f_{j}^{n})^{o}f_{i}^{n} = 1 (i ≠ j) \\ (f_{i}^{n})^{o}f_{i}^{n} = id  (f_{i}^{n})^{o}g_{j}^{m} = 0 \\ (f_{1})_{i_{1}}^{n_{1}}(f_{2})_{i_{2}}^{n_{2}} ⋯ (f_{k})_{i_{k}}^{n_{k}} ∩ id = 0 \\ hd^{o}f_{i}^{n} = 0 = tl^{o}f_{i}^{n}  f_{i}^{n}hd = 0 = f_{i}^{n}tl  hd ∩ id = 0 = tl ∩ id \\ id = ⋃\{(a, a) : a ∈ C_{Σ}\} ∪ ⋃\{id_{f} : f ∈ F_{Σ}\} \end{matrix}

We will also make occasional use of a fixpoint-operator, which will be used in relational structures satisfying axiom fp

fpx.E(x) = E(fpx.E(x)).  (7)

The so-called modular law included in DRA

RS ∩ T ⊆ (R ∩ T S^{o})S

plays an important role in the work discussed here. In the presence of the other DRA axioms it is equivalent to its left-modular formulation

T ∩ RS ⊆ R(R^{o}T ∩ S)

and the equational formulation

T ∩ RS = R(R^{o}T ∩ S) ∩ T.

The reader should consult [BroLip] for an example of how the modular law is used to improve termination behavior of certain relational rewrite systems, in particular in the computation of transitive closure.

We will have need for the following simplification of the modular law in special contexts.

Lemma 1.7 In the equational theory DRA, from SS^{o} ⊂ id we can infer A ∩ SR = S(S^{o}A ∩ R). From S^{o}S ⊂ id we can infer A ∩ RS = (AS^{o} ∩ R)S.

Proof: By the modular law we have, in the first case, A ∩ SR = S(S^{o}A ∩ R) ∩ A. But S(S^{o}A ∩ R) ⊆ SS^{o}A ∩ SR ⊆ idA ∩ SR = A ∩ SR. Thus S(S^{o}A ∩ R) ∩ A reduces to S(S^{o}A ∩ R). The argument for the second claim is symmetric.

In the standard interpretation defined below, the axioms

f_{i}^{n}hd = 0 = f_{i}^{n}tl

rule out the occurrence of extended terms as arguments to function symbols from Σ.

Some of the axioms of RΣ are a relational translation of the first-order theory CET: Clark’s equality theory [Lloyd]. The last axiom is a relational counterpart to the so-called domain closure axiom DC_{Σ}, satisfied in the Herbrand Universe over a finite signature, stating that every individual is a constant or a term beginning with one of the function symbols in the signature. The axiom scheme

(f_{1})_{i_{1}}^{n_{1}}(f_{2})_{i_{2}}^{n_{2}} ⋯ (f_{k})_{i_{k}}^{n_{k}} ∩ id = 0

for f_{1}, …, f_{k} function symbols of Σ of arities n_{1}, …, n_{k} respectively, enforces OC, the occurs-check axiom scheme ¬(x = t[x]) for every term t not identical to x in which x explicitly occurs.

In [Maher], building on earlier results of Mal’cev, Maher shows that CET + OC + DC_{Σ} is complete, decidable, and admits a partial elimination of quantifiers. This can be exploited to give a compact representation of the set-theoretic content of relations over this equational theory. See [BroLip] for details.

A number of useful identities follow from the equations above, and the definitions (6), (4) and (5).

1^{o} = 1  0^{o} = 0  11 = 1  id^{o} = id  idR = R
A ∩ B = B ⇒ A ∪ B = A A ⊆ B ⇒ A^{o} ⊆ B^{o}
f_{i}^{n} ∩ g_{j}^{m} = 0 f_{i}^{n} ⊆ di
(u, v) ∩ R = (u, u)R(v, v) A ∩ RS ⊆ R(R^{o}A ∩ R)
A ∩ RS = R(R^{o}A ∩ S) ∩ A = (AS^{o} ∩ R)S ∩ A
id_{n} ⊆ id

as well as the facts that ∩ and ∪ are the lattice-theoretic infimum and supremum with respect to containment.

1.4 Semantics

1.4.1 Two-tiered structures

Our semantics must interpret formal vectors of terms. It is convenient to do this via a two-tiered notion of model, the lower tier of which is a conventional Σ-algebra, and the upper tier of which interprets the product structure.

Definition 1.8 A Σ^{+}-algebra U is a pair of structures (U_{0}, U_{1}) with the carrier of the first contained in the second (U_{0} ⊆ U_{1}), such that U_{0} is a Σ-algebra and U_{1} is a set equipped with a binary injective function ⟨ , ⟩_{U} : U_{1} × U_{1} → U_{1}. We will refer to the set U_{1} as the carrier of the Σ^{+}-algebra U, and denote it by U, and the function ⟨ , ⟩_{U} as the pairing function supplied by U.

A Σ^{+}-morphism ψ : (U_{0}, U_{1}) (V_{0}, V_{1}) is a function from U_{1} to V_{1} whose restriction to U_{0} is a Σ-algebra homomorphism from U_{0} to V_{0} and which satisfies ψ(⟨x, y⟩_{U}) = ⟨ψx, ψy⟩_{V}.

The reader can easily check that (T_{Σ}, T_{Σ}^{+}) is an initial Σ^{+}-algebra, with pairing function ⟨s, t⟩ = [s, t].

1.4.2 Relational structures

We will use the expression Rel(U) to denote the full relation algebra P(U × U).

We will call a structure 𝔄 = ⟨A, 0^{𝔄}, 1^{𝔄}, id^{𝔄}, di^{𝔄}, ∩^{𝔄}, ∪^{𝔄}, ( )^{o,𝔄}, ∘^{𝔄}⟩ interpreting the relational syntax of the the theory DRA a distributive relation algebra or DRA if it satisfies the axioms DRA. It is called a settheoretic or standard DRA if, in addition, A is a subset of the set of binary relations Rel(U) = P(U × U) on some domain U, with 0^{𝔄}, 1^{𝔄} the empty and maximal set, and with union, intersection, converse and composition standardly interpreted.

A structure 𝔄 = ⟨A, 0^{𝔄}, 1^{𝔄}, id^{𝔄}, di^{𝔄}, (a, a)^{𝔄}hd^{𝔄}, tl^{𝔄}, (f_{i}^{n})^{𝔄}, ∩^{𝔄}, ∪^{𝔄}, ( )^{o,𝔄}, ∘^{𝔄}⟩_{f∈F_{Σ};a∈C_{Σ}} is called a RelΣalgebra if it interprets relational syntax in the obvious way, and satisfies the equational theory RelΣ. It is set-theoretic or standard if in addition A is a subset of Rel(U) for some Σ^{+}-algebra U, and in addition to the conditions satisfied by standard DRA’s, it interprets RΣ’s relational constant symbols (a, a) and f_{i}^{n} in a standard way:

\begin{matrix}(a, a)^{𝔄} = \{(a^{U}, a^{U})\} \\ (f_{i}^{n})^{𝔄} = \{(x, y) : (∃v_{1} ⋯ v_{n−1})(x = f^{U}(v_{1}, …, v_{i−1}, y, v_{i+1}, …, v_{n−1}))\}. \end{matrix}

Definition 1.9 Given a Σ^{+}-algebra U, a U-interpretation is a mapping

[[ ]]_{U} : ℜ → Rel(U)

satisfying

[[(a, a) ]]_{U} = {(a^{U}, a^{U})}  [[tl]]_{U}  = {(⟨t_{1}, t_{2}⟩, t_{1}) : t_{1}, t_{2} ∈ U}
[[id]]_{U}  = {(u, u) : u ∈ U}  [[di]]_{U}  = {(u, v) : u ≠ v ∈ U}
[[hd]]_{U}  = {(⟨t_{1}, t_{2}⟩, t_{1}) : t_{1}, t_{2} ∈ U}  [[R ∪ S]]_{U} = [[R]]_{U} ∪ [[S]]_{U}
[[1 ]]_{U}  = U × U  [[R ∩ S]]_{U} = [[R]]_{U} ∩ [[S]]_{U}
[[0 ]]_{U}  = ∅  [[RS]]_{U}  = {(x, y) : ∃v((x, v) ∈ [[R]]_{U} ∧ (v, y) ∈ [[S]]_{U})}
[[f_{i}^{n}]]_{U} = {(x, y) : (∃v_{1} ⋯ v_{n−1})(x = f^{U}(v_{1}, …, v_{i−1}, y, v_{i+1}, …, v_{n−1}))}
[[fpx.E(x) ]]_{U} = ⋃_{n≥0} E^{(n)}

where E^{(0)} = ∅ and E^{(n+1)} = [[E(x) ]]_{U} [x ← E^{(n)}].

The notation [[ ]]_{U} [x ← R] means the function that returns the same value as [[ ]]_{U} on all inputs save x, for which the output is R.

It is easy to show that any environment (function η from relation variables to sets in Rel(U)) extends uniquely to a U-interpretation. We also note that any interpretation is sound for the axioms DRA. We are interested in interpretations which also satisfy the axioms RΣ. We call these RelΣ-interpretations.

In addition to the semantics just given, natural categorical models exist: tabular distributive allegories [FreySce] provide a semantics for a considerably more general notion of logic program, over a finite product category [FFL, NFDP, PowKin, CorMont]. We will not have need of this generality to describe relational complilation of conventional Horn Clause programs, although, in the presence of types and other programming features, there are interesting applications of such structures to logic programming, abstract interpretation and compilation.

Lemma 1.10 If Σ is a signature with at least one function symbol and one constant symbol, and if U is the free Σ^{+}-algebra (consisting of all closed extended terms over Σ), then Rel(U) is a set-theoretic RelΣ-algebra in which axiom fp holds. Thus, the theory RelΣ + fp is sound in any U-interpretation.

The proof is straightforward: every full power set is a complete (Boolean) relation algebra. The axioms RΣ, as mentioned above, translate into the first-order statement of CET +OC+ DC_{Σ}, which holds in the free extended term algebra T_{Σ}^{+}.

Definition 1.11 Let I_{U} be the set of interpretations into Rel(U).

We denote by ⊑, ⊓, ⊔ the pointwise order and operations on I_{U} induced by the corresponding set-theoretic operations on Rel(U). [[ ]]_{U}^{⊥} and [[ ]]_{U}^{⊤} denote the maximal and minimal interpretations obtained by setting all relational variables equal to the interpretations of 0 and 1 respectively.

We now state some useful properties of interpretations, which follow from well known facts about lattices.

Theorem 1.12 The structure ⟨I_{U}, ⊑, ⊓, ⊔, [[ ]]_{U}^{⊥}, [[ ]]_{U}^{⊤}⟩ is a complete lattice, with supremum and infimum defined pointwise. Furthermore, each [[ ]]_{U} is completely determined by its values on relation variables. If [[ ]]_{U}^{1} and [[ ]]_{U}^{2} are two interpretations with [[X]]_{U}^{1} ⊆ [[X]]_{U}^{2} for each relation variable X then [[ ]]_{U}^{1} ⊑ [[ ]]_{U}^{2}.

Theorem 1.13 Let X_{1}, …, X_{n} be relation variables, and let F be a corresponding set

{F_{i}(X_{1}, …, X_{n}) : 1 ≤ i ≤ n}

of relation expressions with at most the X_{i} free. Define Φ_{F} : I_{U} → I_{U} by

Φ_{F}( [[ ]]_{U})(X_{i}) = [[F_{i}(X_{1}, …, X_{n}) ]]_{U} .

Then

1. Φ_{F} is continuous (hence monotone).

2. Φ_{F} has a least fixed point, [[ ]]_{U}^{∗}, which is the least interpretation in I_{U} satisfying the equations

X_{i} = F_{i}(X_{1}, …, X_{n}).

[[ ]]_{U}^{∗} is equal to the supremum of a countable chain ⨆ [[ ]]_{U}^{n} of interpretations, where [[ ]]_{U}^{o} = [[ ]]_{U}^{⊥} and [[ ]]_{U}^{n+1} = Φ_{F}( [[ ]]_{U}^{n}).

Proof: Straightforward. Proofs of most of these facts occur in one form or another in the literature. The last assertion is the well-known Tarski-Knaster theorem.

For the rest of this paper we fix a finite signature Σ (assumed to have at least one function symbol and one constant), and take the universe U above to be the set of extended ground terms T_{Σ}^{+}, with pairing function given by

⟨ ⟩(u, v) = [u, v].

When U is so chosen we call the resulting semantics a standard interpretation of ℜ into Rel(T_{Σ}^{+}), and denote it by the unadorned bracket [[ ]]. Since interpretations into the same range can only differ on relation variables and open relation expressions, we sometimes refer to [[R]], for closed R, as “the” standard interpretation of R.

We close the section by recalling a few elementary definitions from the theory of relations.

Definition 1.14 A binary relation R is reflexive if id ⊆ R, coreflexive if R ⊆ id, functional if R^{o}R is coreflexive, and injective if RR^{o} is coreflexive.

When stating that a certain relation expression is, e.g. injective or coreflexive, we mean that it is so when interpreted in the standard semantics. When we mean that it can be proved so in one of the equational theories defined in this paper, we will so indicate.

Coreflexive relations play a critical role here, since logic programs are translated into such relations, (although some components of logic programs are built up from more general relations). Coreflexive relations are often a good way to code data in the calculus of binary relations, that is to say, by embedding sets S into the calculus of relations as S^{c} = {(x, x) : x ∈ S}. Diverse approaches to the formalization of data types in the relation calculus has been studied extensively by the Eindhoven group [Backh] and by Bird and de Moor [Algebra].

Three particularly important coreflexive relations associated with any binary relation R are its formal diagonal, domain and range.

Δ(R) = R ∩ id
Dom(R) = R1 ∩ id = RR^{o} ∩ id
Ran(R) = R^{o}1 ∩ id = R^{o}R ∩ id

2 Logic without variables

One of the main results in [TarGiv] due to Tarski, Maddux and Givant (the so-called equipollence theorem), is that every first-order sentence in a theory φ over a theory with a pairing operator has a semantically equivalent equational counterpart X_{φ} = 1 in the theory QRA of relation algebras with quasi-projections. Tarski and Givant also prove a stronger proof-theoretic version of this result, and exhibit a bijective recursive transformation of sentences φ to their associated relation expressions X_{φ} and of first-order proofs of the former to equational derivations of the latter. We will not make direct use of the results or proofs here, but the work undertaken in this paper was inspired by it. The main contribution of the paper is to apply this transformation to compilation and evaluation of logic programming by extending it to map proof search in a fragment of first-order logic into rewriting in the appropriate relational theory.

We now sketch a simple proof of a semantic form of the equipollence theorem, for the special case of algebras of relations definable on a term algebra by first-order formulas over a given signature. Let Σ be a finite language. The atomic statements of T_{Σ} are of the form

t_{1} = t_{2}

which can be rewritten (after introducing a new variable x) as a conjunction of two basic equations x = t_{1} x = t_{2}. If we continue introducing variables, we can write this as a conjunction of elementary or flat equations of the form x = a or x = f(y_{1}, …, y_{n}) where a is a constant in Σ and the x, y_{i} are variables. We assume all atomic formulas are of this form.

Now we define a translation ( )^{r} from formulas θ in the language of T_{Σ} to relation expressions as follows. Recall that ℜ_{Σ}always contains the reserved projection operations hd and tl^{2} Let n be a natural number greater than the largest number of variables occurring in any sentence to be considered below.

Now define, for (0 ≤ i ≤ n)

S_{1} = P_{1}  S_{2} = P_{2}  …  S_{n−1} = P_{n−1}  S_{n} = tl^{n}.

where the P_{i} are given in (1) Observe that, in the standard interpretation for 1 ≤ i ≤ n, we have (u, v) ∈ [[S_{k}]] iff v is the k^{th} component of u. Now define

Q_{i}^{n} = ⋂_{j≠i≤n} S_{j}(S_{j})^{o} id_{n} = ⋂_{j≤n} S_{j}(S_{j})^{o}

Observe that (u, v) ∈ [[id_{n}]] means u and v are vectors of length n and have the same components (u)_{i} for (1 ≤ i ≤ n), and that u [[Q_{i}]]v means all but the i-th component of u and v agree. Let x_{1}, ⋯, x_{s} be all the variables, free or bound, that may occur in θ. Recall all atomic formulas θ may be taken elementary: either x_{i} = a, x_{i} = x_{j} or x_{i_{0}} = f(x_{i_{1}}, …, x_{i_{n}}).

\begin{aligned}(x_{i} = a)^{r} & = & S_{i}(a, a)S_{i}^{o} ∩ id_{n} & (φ ∧ θ)^{r} & = & (φ)^{r} ∩ (θ)^{r} ∩ id_{n} \\ (x_{i} = x_{j})^{r} & = & S_{i}S_{j}^{o} ∩ id_{n} & (¬φ)^{r} & = & id_{n} − (φ)^{r} \\ (x_{i_{0}} = f(x_{i_{1}}, …, x_{i_{n}}))^{r} & = & ⋂_{j}S_{i_{0}}; f_{j}^{n}; S_{i_{j}}^{o} ∩ id_{n} & (∃x_{i}φ)^{r} & = & Q_{i}(φ)^{r}Q_{i} ∩ id_{n} \end{aligned}

Then we have the following result, where H_{Σ} denotes the free Σ-algebra, with carrier the set of closed Σ-terms.

Theorem 2.1 (Freyd, Maddux, Tarski) Let θ be a sentence over the language of T_{Σ} , and let x_{1}, ⋯, x_{n} contain all the variables, free or bound, that may occur in θ. Then H_{Σ} ⊧ θ ⟺ [[(θ)^{r}]] = [[id_{n}]]. For open formulas φ with free variables among x_{1}, …, x_{n}

{(a_{1}, …, a_{n}) : ([a_{1}, …, a_{n}], [a_{1}, …, a_{n}]) ∈ [[(φ)^{r} ]]} = {(a_{1}, …, a_{n}) : H_{Σ} ⊧ φ[a_{1}/x_{1}, …, a_{n}/x_{s}]}

The proof is a straightforward induction on the structure of formulas^{3}.

Proof:

2called quasiprojections by Tarski and, in an essentially equivalent form, tabulations of the maximal relation on the product by Freyd[FreySce].

3The authors are indebted to Peter Freyd [Freyd92] for (a variant of) this formulation and proof of the variable elimination result.

\underline{θ ≡ (x_{i} = a)}: Let u⃗ be an n-tuple of terms in H_{Σ} , and suppose (u⃗, u⃗) ∈ [[(x_{i} = a)^{r}]] = [[S_{i}(a, a)S_{i}^{o} ∩ id_{n}]]. This implies that u_{i} = a, hence H_{Σ} ⊧ (x_{i} = a)[u_{1}/x_{1}, …, u_{n}/x_{n}]. Conversely u_{i} = a forces (u⃗, u⃗) ∈ [[(x_{i} = a)^{r}]].

\underline{θ ≡ (x_{i} = x_{j})}: Suppose (u⃗, u⃗) ∈ [[(x_{i} = x_{j})^{r}]] = [[S_{i}S_{j}^{o} ∩ id_{n}]]. Then u_{i} = u_{j} and H_{Σ} ⊧ (x_{i} = x_{j})[u⃗/x⃗]. The converse is also immediate.

\underline{θ ≡ x_{i_{0}} = f(x_{i_{1}}, …, x_{i_{n}})}: Suppose (u⃗, u⃗) ∈ [[(f(x_{i_{1}}, …, x_{i_{n}}))^{r}]], that is to say, in

⋂_{j} [[S_{i_{0}}; f_{j}^{n}; S_{i_{j}}^{o} ]] ∩ [[id_{n}]].

Then u_{i_{0}} = f(u_{i_{1}}, …, u_{i_{n}}) and H_{Σ} ⊧ θ[u⃗/x⃗]. The converse is immediate.

\underline{θ ≡ φ ∧ θ}: Suppose (u⃗, u⃗) ∈ [[(φ ∧ θ)^{r}]]. Then (u⃗, u⃗) ∈ [[(φ)^{r}]] and (u⃗, u⃗) ∈ [[(θ)^{r}]]. By the induction hypothesis, H_{Σ} ⊧ φ[u⃗/x⃗] and H_{Σ} ⊧ θ[u⃗/x⃗] and hence H_{Σ} ⊧ (φ ∧ θ)[u⃗/x⃗]

\underline{θ ≡ ¬φ}: Suppose (u⃗, u⃗) ∈ [[(¬φ)^{r}]]. Then (u⃗, u⃗) ∈ id_{n} − [[(φ)^{r}]] which is equivalent to saying that (u⃗, u⃗) ∈ [[(φ)^{r}]] is not the case. Using the induction hypothesis, this is equivalent to H_{Σ} |̸= φ[u⃗/x⃗], and hence to H_{Σ} ⊧ ¬φ[u⃗/x⃗].

\underline{θ ≡ ∃x_{i}φ}: If (u⃗, u⃗) ∈ [[(∃x_{i}φ)^{r}]] we must have (u⃗, u⃗) ∈ [[Q(φ)^{r}Q]]. This means there is an n-tuple of terms v⃗ with v_{j} = u_{j} for every j between 1 and n except i, and (v⃗, v⃗) ∈ [[(φ)^{r}]]. By the induction hypothesis, this means H_{Σ} ⊧ φ[v⃗/x⃗]. But this is equivalent to H_{Σ} ⊧ ∃x_{i}φ[u⃗/x⃗]. The converse is left to the reader.

We now turn our attention to the translation of Horn Clause programs. We will want to carry this out in a way that not only preserves meaning, as in the preceding translation, but in a way that is faithful to the operational semantics of the program. We will thus make different, more economical choices, and carry out the translation into RelΣ, defined above, a relational calculus without negation, and with extra constants for capturing the structure of terms in a way that such variable dependent phenomena as unification are easily converted to a variable-free combinatory reduction.

It should be noted that the absence of negation in RelΣis no handicap, vis-a-vis first-order formulas with negation over the Herbrand Universe, because of the well-known results of Mal’cev [Mal’cev, Maher] that any such formula is equivalent to a two-quantifier formula in which negation occurs only immediately preceding equations between terms, which can be modelled in RelΣ using di for disequality.

3 Embedded Prolog

3.1 Capturing Horn Clause Reasoning over Term Models

We introduce a family of relational terms that will prove useful in translating logic programs over the Herbrand Universe into relational equations. One component of this translation involves a sequence of intermediate transformations of the constituent predicates p(t_{1}, …, t_{n}) of the program into relation expressions. We first introduce new variables x⃗ = x_{1}, …, x_{n} and rewrite p(t_{1}, …, t_{n}) as

p(x_{1}, …, x_{n}) ∧ x_{1} = t_{1} ∧ … ∧ x_{n} = t_{n}.

Conjunctions will be replaced by commas below.

In the relational translation of programs, conjunctions of equations of the form x_{i} = t_{i} are translated to relation expressions K̇(t_{1}, …, t_{n}) defined by induction on the structure of the terms t_{i}, as discussed below. We show that the relevant relational translations preserve unification identities derived from Clark’s equality theory. This will require a number of ancillary lemmas and definitions, to which the rest of the section is devoted.

Recall that a relation A is simple or functional if A^{o}A ⊂ id and injective if AA^{o} ⊂ id, i.e. if A^{o} is functional. Injectivity and functionality are preserved under composition and intersection. Thus, in particular, P_{j} is functional (and hence (P_{j})^{o} injective) for every j, since it is built up from hd and tl by composition.

Definition 3.1 Let D be the disjoint union of the set open terms over Σ and the set of sequences ⟨t_{1}, ⋯, t_{n}⟩ of open terms (m ≥ 1). Define

K : D → Rel(U)

as follows. Let m, n, r be natural numbers greater than 0, and u be a term, or a sequence of n terms over some set x_{1}, ⋯, x_{m} of variables. K_{m}(u) is defined by induction on the structure of u.

K(a) = (a, a)1
K(x_{i}) = (P_{i})^{o}
K(f(u_{1}, …, u_{r})) = ⋂_{i≤r} f_{i}^{r}K(u_{i})
K(⟨t_{1}, ⋯, t_{n}⟩) = ⋂_{i≤n} P_{i}K(t_{i})

We also define, for u in D

K̇(u) = id ∩ K(u)1  and  Δ(K)(u) = id ∩ K(u)

Terms t and sequences ⟨t⟩ of terms of length 1 are treated differently by K in the preceding definition. Note that the sequences ⟨t_{1}, …, t_{n}⟩ in D are true members of the cartesian product of copies of the set of terms, and not the formal vectors [t_{1}, …, t_{n}] in T_{Σ}^{+}. Observe also that K(u) is always injective, and that for any substitution θ (whose range is among the set of terms over the variables x_{1}, ⋯, x_{m} in the universe of discourse), since

θf(u_{1}, …, u_{n}) = f(θu_{1}, …, θu_{n}),

we have K(θf(u_{1}, …, u_{n})) = ⋂_{i} f_{i}K(θu_{i})

In the standard set-theoretic interpretation, the K terms capture the structure of term equations in the following sense.

Lemma 3.2 Suppose ⟨t_{1}, ⋯, t_{n}⟩ is a sequence of terms with free variables among x_{1}, ⋯, x_{m}

Let u and y be formal vectors of ground terms of lengths n and m respectively, and u′, y′ arbitrary extended terms. Let u⃗ be the sequence ⟨u_{1}, …, u_{n}⟩. Then

(uu′, yy′) ∈ [[K(⟨t_{1}, ⋯, t_{n}⟩) ]] ⟺ H_{Σ} ⊧ u⃗ = [t_{1}, …, t_{n}][y_{1}/x_{1}, ⋯, y_{m}/x_{m}],

where H_{Σ} is the Herbrand Universe over Σ.

If we think of an m-tuple y of terms as denoting a substitution Θ_{y} for the variables x_{1}, ⋯, x_{m}, then [[K(⟨t_{1}, ⋯, t_{n}⟩) ]] is the set of instance-substitution pairs

{(Θ_{y}[t_{1}, …, t_{n}, ], Θ_{y} ) : y ∈ T_{Σ}^{m}}

where the underscores denote arbitrary additional components.

Proof:[of lemma 3.2] We first show by induction on the structure of terms t with free variables among x_{1}, ⋯, x_{m} that for a ground term u and and an m-tuple of ground terms y = ⟨y_{1}, ⋯, y_{m}⟩ we have

(u, y) ∈ [[K(t) ]] if and only if H_{Σ} ⊧ u⃗ = t[y_{1}/x_{1}, ⋯, y_{m}/x_{m}].

Suppose t is the constant a. Then (u, y) ∈ [[K(a) ]] = [[(a, a)1 ]] = {(a, w) : w ∈ T_{Σ}^{+}} if and only if u is a. But a = a[y_{1}/x_{1}, ⋯, y_{m}/x_{m}].

If t is the variable x_{i} then (u, y) ∈ [[K(x_{i}) ]] if and only if (y, u) ∈ [[P_{i}]] which means u is y_{i}. But this is equivalent to u = x_{i}[y_{1}/x_{1}, ⋯, y_{m}/x_{m}].

If t is a term of the form f(v_{1}, …, v_{n}) then (u, y) ∈ [[K(t) ]] if and only if (u, y) ∈ [[⋂_{i≤n} f_{i}^{n}K(v_{i}) ]]. But this means that for each i between 1 and n (u, y) ∈ [[f_{i}^{n}K(v_{i}) ]], or, equivalently, for some ground terms w_{1}, …, w_{n−1} and z_{i}

u = f(w_{1}, …, w_{i−1}, z_{i}, w_{i+1}, …, w_{n−1})

in the Herbrand universe, and (z_{i}, y) ∈ [[K(v_{i}) ]]. By the induction hypothesis z_{i} is v_{i}[y_{1}/x_{1}, ⋯, y_{m}/x_{m}]. Since this is true for every i we obtain

u = f(v_{1}, …, v_{n})[y_{1}/x_{1}, ⋯, y_{m}/x_{m}]

which is what we wanted to prove.

If t = ⟨t_{1}, ⋯, t_{n}⟩ then (uu′, yy′) ∈ [[K(t) ]] if and only if (uu′, yy′) ∈ [[⋂_{i≤n} P_{i}K(t_{i}) ]]. Thus, for each i between 1 and n (uu′, yy′) ∈ [[P_{i}K(t_{i}) ]], hence for each i (u_{i}, y) ∈ K(t_{i}). But then, by the preceding case u_{i} is t_{i}[y_{1}/x_{1}, ⋯, y_{m}/x_{m}], so u is t[y_{1}/x_{1}, ⋯, y_{m}/x_{m}].

Corollary 3.3 If m ≥ 0, u is a formal vector of length m of ground terms in T_{Σ}, u⃗ the corresponding sequence ⟨u_{1}, …, u_{m}⟩, x is any extended term, and ⟨t_{1}, ⋯, t_{m}⟩ is an m-tuple of open terms (for the same m) then

(ux, ux) ∈ [[id ∩ K(⟨t_{1}, ⋯, t_{m}⟩)1 ]] ⟺ (∃θ)H_{Σ} ⊧ u⃗ = ⟨t_{1}, ⋯, t_{m}⟩θ

where θ is understood to range over substitutions for the variables free in the t_{1}.

We say two sequences of terms ⟨t_{1}, …, t_{m}⟩ and ⟨s_{1}, …, s_{m}⟩ are jointly unifiable by a single substitution θ if for every i, t_{i}θ = s_{i}θ.

Lemma 3.4 Let ⟨t_{1}, …, t_{n}⟩ and ⟨s_{1}, …, s_{m}⟩ be sequences of open terms, with n ≥ m. Then, if ⟨t_{1}, …, t_{m}⟩ and ⟨s_{1}, …, s_{m}⟩ are jointly unifiable, and θ is a most general unifier,

[[K(⟨t_{1}, …, t_{n}⟩) ∩ K(⟨s_{1}, …, s_{m}⟩) ]]_{U} = [[K(⟨t_{1}θ, …, t_{n}θ⟩) ]]_{U} .

If they are not unifiable, the interpretation of the intersection is the empty set.

In addition, if the two sequences are standardized apart

[[K̇(⟨t_{1}, …, t_{n}⟩) ∩ K̇(⟨s_{1}, …, s_{m}⟩) ]]_{U} = [[K̇(⟨t_{1}θ, …, t_{n}θ⟩) ]]_{U}  (8)

if they are unifiable. The intersection is empty otherwise.

The proof is an immediate consequence of lemma (3.2) and its corollary.

Proof: By lemma (3.2), if u and y are formal vectors of ground terms of lengths n and m respectively, u⃗ = ⟨u_{1}, …, u_{n}⟩ and u′, y′ are arbitrary extended terms, then

(uu′, yy′) ∈ [[K(⟨t_{1}, …, t_{n}⟩) ∩ K(⟨s_{1}, …, s_{m}⟩) ]]_{U}
⟺
H_{Σ} ⊧ u⃗ = ⟨t_{1}, …, t_{n}⟩[y_{1}/x_{1}, ⋯, y_{m}/x_{m}] ∧ u⃗ = ⟨s_{1}, …, s_{n}⟩[y_{1}/x_{1}, ⋯, y_{m}/x_{m}].

Letting θ be the substitution represented by [y_{1}/x_{1}, ⋯, y_{m}/x_{m}], this implies ⟨t_{1}, …, t_{n}⟩θ = ⟨s_{1}, …, s_{n}⟩θ in the Herbrand universe. Thus [[K(⟨t_{1}, …, t_{n}⟩) ∩ K(⟨s_{1}, …, s_{m}⟩) ]]_{U} is precisely the set of instances of [t_{1}, …, t_{n}]ψ where ψ is any mgu of ⟨t_{1}, …, t_{n}⟩ and ⟨s_{1}, …, s_{m}⟩ whose range is in the set of terms over the variables x_{1}, ⋯, x_{m}.

This lemma underscores a fundamental feature of variable-elimination in logic programming: unification is reduced to intersection of combinators. But one issue remains to be resolved before these results can be fully exploited. The use of K̇ expressions in logic program reduction would appear to require standardizing their arguments apart, limiting their usefulness. Fortunately the term sequences that actually arise in our compilation are more robust, as we show in the next, somewhat technical lemma which has surprising consequences for the translation.

Lemma 3.5 (Diagonal Lemma) Suppose ⟨t_{1}, …, t_{n}⟩ is a sequence of terms in T_{Σ} all of whose free variables are among x_{1} …, x_{n} (for the same n). Call a component t_{i} of such a sequence nontrivial if t_{i} ≠ x_{i}. Further suppose that for each j between 1 and n if x_{j} occurs freely in a nontrivial term t_{i} then i ≠ j and t_{j} is x_{j}.

Then for any formal vectors of ground terms u, d in T_{Σ} of length n and any formal vectors of ground T_{Σ}-terms y, z, if (uy, dz) ∈ K(⟨t_{1}, …, t_{n}⟩) then (uy, uy) ∈ K(⟨t_{1}, …, t_{n}⟩) as well. Thus

K̇(⟨t_{1}, …, t_{n}⟩) = id ∩ K(⟨t_{1}, …, t_{n}⟩).  (9)

Thus, under these hypotheses, K̇ expressions behave like K-terms and (8) holds without the restriction that term arguments be standardized apart. It turns out that the hypotheses of this lemma are always met by the term sequences that will be constructed in the translation of Prolog programs described below. The reader should note, however, that identity (9) does not hold in general. Proof: Suppose (uy, dz) ∈ K(⟨t_{1}, …, t_{n}⟩) = ⋂_{i} P_{i}K(t_{i}). Then, by lemma (3.2), for each i

u_{i} = t_{i}[d_{1}/x_{1}, …, d_{n}/x_{n}].

Suppose t_{i_{1}}, …, t_{i_{n}} are all the nontrivial terms among the t_{i}, and that x_{j_{1}}, …, x_{j_{s}} are variables occurring in these terms. Then, by hypothesis, for all k between 1 and s, t_{j_{k}} = x_{j_{k}}. Thus

K(⟨t_{1}, …, t_{n}⟩) = ⋂_{k} P_{j_{k}}K(x_{j_{k}}) ∩ ⋂_{i∉{j_{1},...,j_{s}}} P_{i}K(t_{i})
= ⋂_{k} P_{j_{k}}P_{j_{k}}^{o} ∩ ⋂_{i∉{j_{1},...,j_{s}}} P_{i}K(t_{i}).

Thus for each k between 1 and s, u_{j_{k}} = d_{j_{k}}. Since the x_{j_{k}} are only variables free in nontrivial t_{i}, for each such t_{i}, u_{i} = t_{i}[d_{1}/x_{1}, …, d_{n}/x_{n}] = t_{i}[u_{1}/x_{1}, …, u_{n}/x_{n}]. For every other t_{i}, t_{i} = x_{i}, so we immediately have u_{i} = t_{i}[u_{1}/x_{1}, …, u_{n}/x_{n}]. Therefore

⟨u_{1}, …, u_{n}⟩ = ⟨t_{1}, …, t_{n}⟩[u_{1}/x_{1}, …, u_{n}/x_{n}],

from which (uy, uy) ∈ K(⟨t_{1}, …, t_{n}⟩) by lemma (3.2). But then every uy in the domain of K(⟨t_{1}, …, t_{n}⟩) is in the domain of K(⟨t_{1}, …, t_{n}⟩) ∩ id, whence

K̇(⟨t_{1}, …, t_{n}⟩) = id ∩ K(⟨t_{1}, …, t_{n}⟩).

Definition 3.6 A sequence ⟨t_{1}, …, t_{n}⟩ of terms in T_{Σ}^{+} is called clean if it satisfies the hypothesis of the preceding lemma.

Observe that ⟨t_{1}, …, t_{n}⟩ is clean if and only if the substitution φt⃗ = {t_{i}/x_{i} : t_{i} non-trivial} induced by the equations {x_{i} = t_{i} : 1 ≤ i ≤ n} is idempotent.

Lemma 3.7 Suppose ⟨t_{1}, …, t_{n}⟩ is clean, and (uy, uy) ∈ K(⟨t_{1}, …, t_{n}⟩). Then the substitution θ_{u} = {u_{1}/x_{1}, …, u_{n}/x_{n}} satisfies the equations

x_{i} = t_{i} (1 ≤ i ≤ n)

in the sense that x_{i}θ_{u} = t_{i}θ_{u} for (1 ≤ i ≤ n).

The proof is just a restatement of the fact, shown in the proof of lemma (3.5) that, for each i,

u_{i} = t_{i}[u_{1}/x_{1}, …, u_{n}/x_{n}].

3.1.1 Switching Relations

Definition 3.8 Fix the natural number n ≥ 1 and let ι⃗ = ⟨i_{1}, …, i_{n}⟩ be a sequence of distinct members of the set {1, …, n} natural numbers. Then define the relations W (ι⃗) as follows:

W (i_{1}, …, i_{n}) = ⋂_{j=1}^{n} P_{i_{j}}(P_{j})^{o}.

W (i_{1}, …, i_{n}) is called a switching relation. We also use the notation W (σ) where σ is the permutation of the first n natural numbers into ι⃗.

We now state three useful properties of switching relations, whose simple proofs are left to the reader.

Lemma 3.9 W (i_{1}, …, i_{n}) is functional and injective, provably in the equational theory RelΣ

Lemma 3.10 Let x⃗, and y⃗ be formal vectors of terms of length at least n + 1 over the Herbrand Universe. Then

(x⃗, y⃗) ∈ [[W (i_{1}, …, i_{n}) ]] ⟺ H_{Σ} ⊧ ⋀_{j=1}^{n} x_{i_{j}} = y_{j}.

Furthermore, if t_{1}, …, t_{n} is a tuple of n terms, σ a permutation on {1, …, n}, and W = W (σ)

[[W^{o}K̇(⟨t_{1}, …, t_{n}⟩) W ]] = [[K̇(⟨t_{σ^{−1}(1)}, …, t_{σ^{−1}(n)}⟩) ]].

Lemma 3.11 If σ is a permutation of the first n nonzero natural numbers

W (σ^{−1}) = W (σ)^{o}.

provably in the theory RelΣ.

Another useful property of switching relations follows immediately from 1.7.

Lemma 3.12 One can prove in the equational theory DRA that for any relation expressions R, Q and switching relations W

R ∩ W QW^{o} = W (W^{o}RW ∩ Q)W^{o}

4 Relational Translation of Programs: a sketch

An atomic formula is said to be linear or pure if its arguments constitute a linear sequence of variables, that is to say, one in which all variables are distinct.

The first step in the Clark completion of a prolog program is the linearization of head predicates. A clause

p(t_{1}, …, t_{r}) : −T l

is replaced by

p(x_{1}, …, x_{r}): −x_{1} = t_{1}, …, x_{n} = t_{n}, T l.

where the x_{i} are fresh. The variables free in the tail but not in the head are then existentially quantified:

p(x_{1}, …, x_{r}) : −∃y⃗[x_{1} = t_{1}, …, x_{n} = t_{n}, T l].

Now all clauses with head predicate letter p how have precisely the same head, and are thus equivalent to a single clause with this head, but with tail replaced by a disjunction of the newly formed tails:

p(x_{1}, …, x_{r}) : − ⋁ B_{i}

where each B_{i} is of the form

∃y⃗_{i}[x_{1} = t_{i1}, …, x_{n} = t_{in}, T l_{i}]  (10)

We are now going to describe a series of additional transformations that have the effect of putting the logic program into a form that maintains its set of ground atomic consequences over the Herbrand Universe, while bringing it closer to the eventual shape of the desired relational equation. The first transformation involves the linearization of the predicates in the tails B_{i}, with the subsequent generation of equations, some of which then get modified. This is then followed by the introduction of selection operators. We describe it in two steps: linearization and selection.

1. Linearization: First we linearize the tails. Proceeding left-to-right, every atomic formula q(s_{1} …, s_{m}) in T l_{i} (the non-equational part of B_{i}) is rewritten as

z_{1} = s_{1}, …, z_{m} = s_{m}, q(z_{1}, …, z_{m}),

where

Case 1: Either s_{i} is a variable that has not occurred earlier in the same atomic predicate, and z_{i} is identical to s_{i} (so the equation reads s_{i} = s_{i}), or

Case 2: z_{i} is a fresh variable, which is then existentially quantified on the outside. That is to say the existential quantifier ∃y⃗_{i} becomes ∃y⃗_{i}z⃗, where z⃗ is the sequence of all distinct fresh variables in the sequence z⃗_{1} ⋯ z⃗_{ℓ} of variables now occurring in the ℓ predicates q_{1}(z⃗_{1}), …, q_{ℓ}(z⃗_{ℓ}) in the non-equational part of the tail.

Starting with the first index greater than r, the arity of the head predicate, which has already required the introduction of variables x_{1}, …, x_{r} that may now occur freely in the tail because Case 1, above, obtained, all new distinct existentially quantified variables are renamed in increasing order from left to right, so that every variable occuring in the entire tail B_{i} except for the original bound variables y⃗_{i} is part of a master list x_{1}, … x_{k} where k is bounded by the sum of the arities of all the predicate occurrences in the head or tail of the clause.

Finally, we move all generated equations, now of the form x_{i} = t_{i} (where the t_{i} are terms originally ocurring in the clause predicates) to the beginning of the quantifier-free part of the tail. Thus the tail is now of the form

∃y⃗_{i}∃x_{r+1} ⋯ x_{w}[x_{1} = t_{1}, …, x_{w} = t_{w}, q_{1}(x_{r+1}, …, x_{r+α(1)}), …, q_{ℓ}(x_{a}, …, x_{a+α(ℓ)})],

where r is the arity α(p) of the head predicate, α(i) the arity of the i-th tail predicate, and a is r + the sum of the arities of the preceding ℓ − 1 tail predicates.

Now we rename the remaining existentially bound variables from y⃗_{i} originally occurring in the tail, so they are added to the (end of the) master list of variables x_{j}.

Finally, for any variable x_{j} not occurring on the left hand side of one of the equations x_{i} = t_{i} the equation x_{j} = x_{j} is added to the equational part in its proper place. The equational part is now written in sequence form as x⃗ = t⃗. It is a sequence of length bounded by n, the weight of the corresponding clause in the original prolog program, which is the sum of the number of variables k occurring in the tail and not in the head, and the arities of the predicate occurrences either in the head or tail of the original clause,

wt(C) = k + n + Σ_{i=1}^{ℓ}r_{i}.

It may be less than the weight because of the possible occurrence of Case 1 above which ensured reuse of variables that would not obstruct linearity (distinctness of variables) of each predicate in the tail. For reference, each clause has the following appearance

p(x_{1}, …, x_{n}) : − ⋁ B′_{i}  (11)

where

B′_{i} = ∃x_{r+1} ⋯ x_{n}[x⃗ = t⃗, q_{i1}(x⃗_{1}), …, q_{iℓ_{i}}(x⃗_{ℓ})]  (12)

and where each x⃗_{j} is the j-th block of distinct variables of length the arity of q_{ij}, starting with the sum of the arities of the preceding predicate occurrences, including that of the head. Letting x⃗_{0} be the sequence of variables now occurring in the head, the entire master sequence of variables x⃗ = x⃗_{0}x⃗_{1}, …, x⃗_{ℓ} may contain repetitions because of Case 1 above, but, we repeat, each block is linear.

2. Selection: Each sequence x⃗_{i} of variables occurring in the i-th block in the tail can now be viewed as the result of applying a selection operator ρ_{i} to the master sequence x⃗:

ρ_{i}x⃗ = x⃗_{i}.

This yields normalized disjuncts of the form

D_{i} = ∃x_{n+1} ⋯ x_{w}[x⃗ = t⃗, q_{i1}(ρ_{1}x⃗), …, q_{iℓ_{i}}(ρ_{ℓ}x⃗)].  (13)

We now replace all implications in clauses by bi-implications, as in the Clark completion. We will call the resulting program P_{n}, consisting of the clauses:

p_{i}(x_{1}, …, x_{n}) : − ⋁ D_{ij}  (14)

the completed or normal form of P.

Since we will not need this result in our adequacy theorem we do not take the trouble to establish that the preceding program transformations maintain ground atomic consequences in any term model. It is, however, straightforward to prove, using arguments similar to the proof of the fact that the Clark completion of a program has the same atomic (in fact positive) consequences as the program (see e.g. [Shep88, Lloyd]), and repeated applications of the logical equivalence, for fresh y_{1}, …, y_{n}

∃x⃗[A(t_{1}, …, t_{n})] ⟺ ∃x⃗y_{1}, …, y_{n}[y_{1} = t_{1} ∧ … ∧ y_{n} = t_{n} ∧ A(y_{1}, …, y_{n})]

In the case of Prolog programs with positive and negative equations, treated briefly in a later section, the completed (or normalized program) plays a central role, and should be seen as the proper logical formulation of the program captured by our relational translation.

We note following for future reference.

Lemma 4.1 The sequences t⃗ that occur in the equational part of each disjunct in the normal form of a program are clean in the sense of definition (3.6).

This is clear from the way fresh variables are introduced in the normalization process.

Our resulting set of equivalences are now almost ready to be cast in first-order-variable-free relational form. We need to define one more operation on sequences of variables (or on their indices): the permutation σ_{i} of the indices of x⃗ induced by the selection operator ρ_{i}.

Definition 4.2 Let ρ_{i} be the i-th selection operator defined above. and w′ the length of the i-th disjunct’s master list of variables. Then the associated permutation of indices

σ_{i} : {1, 2, …, w′} → {1, 2, …, w′}

is given by letting x_{σ_{i}(1)}, …, x_{σ_{i}(w′)} be the sequence x⃗_{i} followed by all remaining variables in x⃗ in order. σ_{i} simply shifts the i-th block of variables to the front of the sequence.

4.1 The Relational step

We now transform the normalized program defined above into a finite set of relation equations. For each predicate letter q ∈ Π we introduce a relation variable \overline{q}. Now consider the normalized clause defining predicate p, of arity m. Each disjunct Θ in its tail of the form (13) is translated into the relation expression (Θ)^{r}

id ∩ I_{m}[K̇(t⃗) ∩ W (σ_{1})\overline{p_{1}}W (σ_{1})^{o} ∩ ⋯ ∩ W (σ_{ℓ})\overline{p_{ℓ}}W (σ_{ℓ})^{o}]I_{m}.  (15)

We then translate the whole clause (14) by

\overline{p} = (Θ_{1})^{r} ∪ ⋯ ∪ (Θ_{m})^{r}.

As an immediate consequence of the preceding lemma and lemma (3.5), we have

Lemma 4.3 If K̇(t⃗) occurs in a disjunct of a normalized Prolog program, then

K̇(t⃗) = K(t⃗) ∩ id.

The result of applying this procedure to all predicate definitions in the canonical completion of a Horn Clause program P is a set E_{P} of n equations e_{1}, …, e_{n} in the n predicate letters of the program (now viewed as relation variables). The typical equation e_{j} being of the form

\overline{p}_{j} = ⋃_{i} Θ_{i}^{j}

as described above. The Θ_{i}^{j} contain the symbols \overline{p_{k}} as relation variables corresponding to the original predicate letters in the program.

We can write this dependency of relation variables as

\overline{p}_{i} = F_{j}(\overline{p}_{1}, …, \overline{p}_{n}).  (16)

We call this equational system E_{P}, the equational translation of P.

“Gaussian elimination”

A final and obvious step is to bind all the variables with the fp-operator. We assume that one predicate letter, say p_{1} is the one to be queried. Dropping the overbars on relation variables, we rewrite the last equation of system (16) above as

p_{n} = fpz_{n}.F_{n}(p_{1}, …, p_{n−1}, z_{n})

and substitute into equation n − 1, obtaining

p_{n−1} = F_{n−1}(p_{1}, …, p_{n−1}, fpz_{n}.F_{n}(p_{1}, …, p_{n−1}, z_{n}))

Now we bind the (possibly multiple) occurrences of p_{n−1} and so on, eventually obtaining a single ℜ_{Σ}- expression

p_{1} = fpz_{1}.F_{1}(z_{1}, …)  (17)

where the right hand side is a closed (no-free-relation-variable) term. We will call the right-hand expression R_{p_{1}} and say that R_{p_{1}} arises from translation of the predicate p_{1} defined by the program P.

Definition 4.4 A positive relation expression R ∈ ℜ_{Σ} (or the defining equation p = R for some identifier p) is said to be a (relational) logic program if R is of the form R_{q}, i.e. it arises from the translation of a predicate q defined by a logic program P.

4.1.1 An Example

We illustrate the steps outlined above with an example. We start with the well-known program P_{add} defining addition of formal numerals over the Herbrand Universe for {o, s}:

add(o,X,X).
add(s(X),Y,s(Z)) :- add(X,Y,Z).

Just for reference, the Clark completion (minus the addition of Clark’s equality theory) is:

add(x_{1}, x_{2}, x_{3}) ⟷ ∃x(x_{1} = o, x_{2} = x, x_{3} = x) ∨
∃x, y, z(x_{1} = s(x), x_{2} = y, x_{3} = s(z), add(x, y, z)).

After renaming the bound variables x, z as x_{4}, x_{5}, (y is already named by x_{2}) the normal form of Pis:

add(x_{1}, x_{2}, x_{3}) ⟷
(⟨x_{1}, x_{2}, x_{3}⟩ = ⟨o, x_{2}, x_{2}⟩)
∨
∃x_{4}, x_{5}(⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩ = ⟨s(x_{4}), x_{2}, s(x_{5}), x_{4}, x_{5}⟩
∧ add(x_{4}, x_{2}, x_{5})).

Letting ρ be the selector function ⟨1, 2, 3, 4, 5⟩ ↦ ⟨4, 5, 2⟩, and σ the associated permutation ⟨1, 2, 3, 4, 5⟩ ↦ ⟨4, 5, 2, 1, 3⟩, and writing x⃗ for ⟨x_{1}, x_{2}, x_{3}, x_{4}, x_{5}⟩, this can be rewritten:

add(x_{1}, x_{2}, x_{3}) ⟷
⟨x_{1}, x_{2}, x_{3}⟩ = ⟨o, x_{2}, x_{2}⟩
∨
∃x_{4}, x_{5}(x⃗ = ⟨s(x_{4}), x_{2}, s(x_{5}), x_{4}, x_{5}⟩ ∧ add(ρx⃗)).

The relational translation is:

\overline{add} = K̇(o, x_{2}, x_{2}) ∪ I_{3}[K̇(s(x_{4}), x_{2}, s(x_{5}), x_{4}, x_{5}) ∩ W (σ) \overline{add} W (σ)^{o}]I_{3}.

or

\overline{add} = fp.Z K̇(o, x_{2}, x_{2}) ∪ I_{3}[K̇(s(x_{4}), x_{2}, s(x_{5}), x_{4}, x_{5}) ∩ W (σ) Z W (σ)^{o}]I_{3}.

5 Adequacy of the translation

We now show the translation preserves the intended meaning of the program. To this end we need to define canonical interpretations of both the original program and of the induced equational system (16), or its associated closed form (17).

Let P be a Prolog program, Π = {p_{1}, …, p_{n}} the predicate symbols occurring in it, Σ its signature, and T_{P} the Kowalski-VanEmden continuous operator it induces on the power-set of the Herbrand base (see e.g. [Lloyd]). Let T_{P} ↑_{0}= ∅, T_{P} ↑_{(n+1)}= T_{P}(T_{P} ↑_{n}) and T ↑_{ω} the least fixed point ⋃ T_{P} ↑_{n} of T_{P}, that is to say, the least Herbrand model of P.

Define, for each p_{i} ∈ Π and n in ω

{[p_{i}]}^{n} = {(u, u) : p_{i}(u) ∈ T_{p} ↑_{n}}

and

{[p_{i}]}^{∗} = {(u, u) : p_{i}(u) ∈ T_{p} ↑_{ω}}

Let \overline{p_{i}} be relation variables associated with the predicate symbols p_{i} and let

\overline{p}_{i} = F_{i}(\overline{p}_{1}, …, \overline{p}_{n})  (1 ≤ i ≤ n)  (18)

be the equational translation E_{P} of P. Let F be the set of open relational terms F_{j}(\overline{p}_{1}, …, \overline{p}_{n}), and R_{p_{i}} = fpz_{i}.F_{i}(…) the associated closed form solutions of this equational translation.

Let Φ_{F} be the induced operator on relational interpretations into the standard model P(T_{Σ}^{+} × T_{Σ}^{+}), as in the statement of theorem (1.13). By the same theorem, Φ_{F} has a least fixed point [[ ]]^{∗} which is the supremum of a chain of interpretations [[ ]]^{0} = [[ ]]^{⊥}, …, [[ ]]^{n}, . . .. We will drop subscripts in the discussion below, when speaking of a typical predicate symbol p_{i} ∈ Π to simplify notation.

Lemma 5.1 For each relation variable \overline{p} and any interpretation [[ ]]

[[\overline{p}]]^{∗} = [[R_{p}]]

Proof: Straightforward, using the semantics of the fp construct and the Tarski-Knaster theorem.

If s is the arity of the program predicate letter p, define the s-th restriction [[\overline{p}]]|_{s} of [[\overline{p}]] by

[[\overline{p}]]|_{s} = \{([u_{1}, …, u_{s}], [u_{1}, …, u_{s}]) : ∃x ∈ T_{Σ}^{+} ([u_{1}, …, u_{s}, x], [u_{1}, …, u_{s}, x]) ∈ [[\overline{p}]].

Then we have the following Soundness and Completeness theorem for our translation:

Theorem 5.2 (Adequacy) For each p ∈ Π

\{[\overline{p}]\}^{∗} = [[p]]^{∗}|_{s}

Proof: We establish the two claims below by induction on n, from which the theorem follows immediately.

1. For each natural number n [[\overline{p}]]^{n}|_{s} ⊆ \{[p]\}^{∗}.

2. For each natural number n \{[p]\}^{n} ⊆ [[\overline{p}]]^{∗}|_{s}.

\underline{Claim (1)}: Since [[\overline{p}]]^{0}|_{s} is empty, the base case is immediate. Suppose the claim holds for n and (u, u) ∈ [[\overline{p}]]^{n}|_{s}. The clause defining p in the normal form P_{n} is of the form

p(x_{1}, …, x_{n}) : − ⋁ D_{i}  (19)

each D_{i} is of the form

D_{i} = ∃x_{n+1} ⋯ x_{w}[x⃗ = t⃗, q_{i1}(ρ_{1}x⃗), …, q_{iℓ_{i}}(ρ_{ℓ}x⃗)].  (20)

where the sequence t⃗, say of length m, is the concatenation t⃗_{0} ⋯ t⃗_{ℓ} of arguments occurring in the clause

p(t⃗_{0}) : −q_{i1}(t⃗_{1}), …, q_{iℓ_{i}}(t⃗_{ℓ}).  (21)

of the original program P.

The corresponding equation in E_{P} is

\overline{p} = ⋃ Θ_{i}

where

Θ_{i} = I_{s}[K̇(t⃗) ∩ W (σ_{1})\overline{q_{i1}}W (σ_{1})^{o} ∩ ⋯ ∩ W (σ_{ℓ})\overline{q_{iℓ}}W (σ_{ℓ})^{o}]I_{s}.

So our supposition (u, u) ∈ [[\overline{p}]]^{n}|_{s} implies that for some i (1 ≤ i ≤ ℓ) there is an extended term x, (ux, ux) ∈ [[Θ_{i}]]^{n}. Since [[I_{s}]]^{n} consists of formal vectors of length at least s + 1 sharing their first s components, there is an extended term y such that the length of uy is at least one greater than that of t⃗, (uy, uy) ∈ [[K̇(t⃗) ]]^{n} and for each j between 1 and ℓ, (uy, uy) ∈ [[W (σ_{j})\overline{q_{j}}W (σ_{j})^{o}]]^{n}. But then, by corollary (3.3), for some ground substitution θ, ⟨(uy)_{1}, …, (uy)_{m}⟩ = t⃗θ (where m is the length of t⃗), from which we have the following consequences:

• u = t⃗_{o}θ, in other words p(u) is a θ-instance of the head p(t⃗_{0}) of the original program clause (21).

• for each j between 1 and ℓ, and some extended term z, (t⃗θz, t⃗θz) ∈ [[W (σ_{j})\overline{q_{j}}W (σ_{j})^{o}]]^{n}, hence (by lemma 3.10)

• (t⃗_{j}θz′, t⃗_{j}θz′) ∈ [[\overline{q_{j}} ]]^{n}, whence (t⃗_{j}θ, t⃗_{j}θ) ∈ [[\overline{q_{j}} ]]^{n}|_{r_{j}} where r_{j} is the arity of q_{j}.

By the induction hypothesis (t⃗_{j}θ, t⃗_{j}θ) ∈ {[q_{j} ]}^{∗}, whence (by definition of {[ ]}^{∗}), q_{j}(t⃗_{j}θ) ∈ T ↑_{ω}. But then every θ-instance of the tail of clause (21) holds in the least Herbrand model of P, hence so does p(t⃗_{0}θ). But recall that u = t⃗_{0}θ so this means (u, u) ∈ {[p]}^{∗}, which is what we wanted to prove.

The other direction, which requires a symmetric argument, is left to the reader.

5.1 Extending the Translation to Equations and Disequations

Enriched Terms

We will have need of a metalanguage of enriched terms for discussing certain operations on terms (such as unification and anti-unification). To this end, we introduce operators

⊓^{2}, ¬^{1}

of the arities shown, and define an enriched term to be an expression of the form

t_{1} ⊓ … ⊓ t_{n} ⊓ ¬s_{1} ⊓ ¬s_{2} ⊓ ⋯ ⊓ ¬s_{m}  (22)

where the t_{i} and s_{i} are terms (members of the term model of Σ), and where m ≥ 0 and n ≥ 0. Simply put: enriched terms are either un-enriched terms or they are built by application of the unary operator ¬ to un-enriched terms, and by iterated applications of the binary symbol ⊓ to enriched terms. The binary operator associates to the right so that the typical enriched term may be written in the form (22).

5.1.1 Horn Clauses with Equations

We now consider programs comprised of finite sets of clauses of the form

p(t_{1}, …, t_{r}) : −e □ T l

where e, the equality component, is a finite set of equality formulas

u_{1} ∼ v_{1}, …, u_{m} ∼ v_{m}

with u,v terms, and ∼ one of the symbols {=, ≠}, and T l is a pure Horn clause tail.

We now summarize the normalization procedure for such programs.

Head linearization: We first introduce fresh variables in the head, à la Clark, adding new equations to the equality component of the tail, and existentially quantifying all variables “free” in the tail, that is to say, occurring in the tail and not in the head.

p(x_{1}, …, x_{r}) : −∃y⃗[x_{1} = t_{1}, …, x_{r} = t_{r}, e □ T l].

The equality component is now the expanded sequence x_{1} = t_{1}, …, x_{r} = t_{r}, e.

First processing of equality component: . Modify every equality formula u ∼ v in the equality component as follows:

1. If u ∼ v is u = v where both u and v are variables, replace v with u everywhere in the tail, and remove v from the sequence of existentially quantified variables.

2. If u ∼ v and u is a variable, and the above conditions are not met, do not modify the equation.

3. Otherwise, replace u ∼ v with z = u ∧ z ∼ v, where z is fresh and is added to the sequence of existentially quantified variables.

Linearization of the tail Now we proceed exactly as with pure prolog programs, replacing sequences of terms t_{i} occurring in atomic predicates in the tail with sequences of variables x_{i} (which may or may not be fresh, depending on whether Case 1 or Case 2 obtains in the linearization procedure described in section 4), and adding new equations x_{i} = t_{i} to the equality component of the clause.

Renaming: finally all variables occurring in the tail are renamed in the same way as in the pure Prolog case, so as to form part of a master list x⃗ = x_{1}, …, x_{n}. Each clause now looks like this:

p(x_{1}, …, x_{r}) : −∃x_{r+1} ⋯ x_{n}[x_{i_{1}} ∼ t_{i_{1}}, …, x_{i_{k}} ∼ t_{i_{k}} □ T l′],

where the new tail T l′ is the linearized version of the old, and where the equality formulae x_{i_{j}} = t_{i_{j}} include processed equality formulae from the original clause as well as equations added during the linearization steps. Unlike the pure Horn clause case, there may be repeated occurrences of variables on the left-hand side of the equality formulas. As before, we force all variables in the clause to occur on the left hand side of equality formulas, via the possible addition of identities x_{i} = x_{i} if necessary.

Enrichment: We now replace all equality formulas of the form x_{i_{j}} ≠ t_{i_{j}} and rewrite then as x_{i_{j}} = ¬t_{i_{j}}. Finally we gather all equations (now possibly involving enriched terms) which share a common variable x on the left hand side

x = t_{j_{1}}, …, x = t_{j_{s}}

and write then as the single equation

x = t_{j_{1}} ⊓ ⋯ ⊓ t_{j_{s}}

where some of the t’s may be of the form ¬u, u a term.

At the expense of adding enriched terms, we have now brought the clause into a form where each variable occurring anywhere in the clause occurs exactly once on the left hand side of an equality formula, and where no occurrences of disequality remain.

p(x_{1}, …, x_{r}) : −∃x_{r+1} ⋯ x_{n}[x_{1} = s_{1}, …, x_{n} = s_{n} □ T l′].

Relational step: The clause is now translated to a relation expression in a manner very similar to the

pure case

\overline{p} = I_{s}[Δ(K)(s_{1}, …, s_{n}) ∩ W (σ_{1})\overline{q_{1}}W (σ_{1})^{o} ∩ ⋯ ∩ W (σ_{ℓ})\overline{q_{ℓ}}W (σ_{ℓ})^{o}]I_{s}

where Δ(K)(s_{1}, …, s_{n}) is the diagonal K(s_{1}, …, s_{n}) ∩ id, but where we now need to expand the definition of K to include sequences of enriched terms. This is discussed next.

Definition 5.3 K maps enriched terms, and sequences of such to relation expressions as follows:

K(a) = (a, a)1
K(x_{i}) = (P_{i})^{o}
K(f(u_{1}, …, u_{n})) = ⋂_{i≤n} f_{i}^{n}K(u_{i})
K(⟨t_{1}, ⋯, t_{n}⟩) = ⋂_{i≤n} P_{i}K(t_{i})
K(¬t) = diK(t)
K(t_{1} ⊓ t_{2}) = K(t_{1}) ∩ K(t_{2})

We now need to extend lemma 3.7 in the appropriate way. It should be noted that in the enriched case, the analogue of diagonal lemma (3.5) is of no use. We can no longer assume that sequences ⟨t_{1}, …, t_{n}⟩ of enriched terms appearing in expressions of the form Δ(K)(⟨t_{1}, …, t_{n}⟩) are clean in the sense of that lemma. Thus the diagonal Δ(K)(⟨t_{1}, …, t_{n}⟩) may be a proper subset of K̇⟨t_{1}, …, t_{n}⟩), which is why we are forced to use the diagonal in the translation. With this choice, we obtain the correct translation of equational component of a logic program clause in the following sense.

Lemma 5.4 Let x_{i_{1}} ∼ t_{i_{1}}, …, x_{i_{k}} ∼ t_{i_{k}} be a sequence of equality formulas, where the t_{i_{j}} are terms, and ⟨s_{0}, …, s_{n}⟩ the sequence of enriched terms produced by the enrichement process described above, with x_{1}, …, x_{n} the list of all free variables occurring in the t_{i_{j}} (and hence the s_{i}). Then:

[[Δ(K)(⟨s_{0}, …, s_{n}⟩) ]] = {(v, v) : v = uz where
u, z ∈ T_{Σ}^{+}, u = [u_{1}, …, u_{n}] and
x_{i_{1}}θ_{u} ∼ t_{i_{1}}θ_{u}, …, x_{i_{k}}θ_{u} ∼ t_{i_{k}},

where θ_{u} is the substitution {u_{1}/x_{1}, …, u_{n}/x_{n}}. in other words, the diagonal of K(⟨s_{0}, …, s_{n}⟩) consists of precisely those ground substitutions that satisfy the original equations and disequations.

With this lemma, it is easy to extend the adequacy theorem (5.2) to the equational Horn clause case. For details the reader is referred to [Chap].

6 Evaluation

The equational theory E_{P} induced by a program P now opens up a new way of computing queries to logic programs of a quite general nature, via directed relational rewriting. In this section we sketch a rewrite system, together with a deterministic rewriting strategy that simulates SLD resolution of conventional prolog queries . It is our first concern to show that the conventional operational interpretation of the original program can be recovered relationally, before addressing alternative evaluations.

Suppose P is a program with predicate symbols Π = {p_{1}, …, p_{n}} and G is a query, say of the form

q_{1}(t⃗_{1}), …, q_{m}(t⃗_{m})  (23)

where the q_{i} are members of Π of arity α(i) and the t⃗_{i} are tuples of terms of appropriate arities. Let the corresponding relation variables in the induced equational theory E_{P} be \overline{p_{i}}.

Definition 6.1 The translation A_{G} of a query G of the form (23) is the relation expression:

K̇(t⃗_{1} … t⃗_{m}) ∩ \overline{q_{1}}′ ∩ … ∩ \overline{q_{n}}′.

where \overline{q_{i}}′ is W (σ_{i})\overline{q_{i}}W (σ_{i})^{o}, σ_{i} being the permutation on \{1, …, m\} such that

⟨t_{σ_{i}(1)}, …, t_{σ_{i}(n)}⟩ = t⃗_{i}t⃗_{1} ⋯ t⃗_{i−1}t⃗_{i+1} ⋯ t⃗_{m}

in other words, the permutation asociated with the i-th selector ρ_{i}, as in definition (4.2).

In the canonical semantics, the meaning of the translated query [[A_{G}]]^{∗} is easily seen to coincide with the set of ground terms satisfying G in the least Herbrand model of P. Evaluation of the query G is simulated by rewriting the relation expression A_{G} according to certain strategy outlined below.

We have a choice to make in the way we describe evaluation. We may explicitly model recursion at the object level by using the fix-point operator in our syntax, replacing all relation variables by their closed form solutions, or we may handle it metalogically by dynamically replacing relation variables by their definitions when they are evaluated in rewriting. We adopt the latter approach here.

Termination occurs when the resultant term has no free variables (or, when closed forms are used, when the term is recursion-free: without occurrences of fp). We now describe the rewriting system and the evaluation strategy used, and sketch a proof of its soundness and completeness. It should be remarked that certain reductions in the system below are best called meta-reductions, since they involve rules that carry out in one step some rather intricate rewriting of expressions. For example, we carry out the rewriting

K̇(t_{1}, …, t_{n}) ∩ K̇(s_{1}, …, s_{m}) ⟼^{P}  K̇(θt_{1}, …, θt_{n})  (24)

(25)

where

• the tuples t⃗ = (t_{1}, …, t_{n}) and s⃗ = (s_{1}, …, s_{m}) are standardized apart

• m ≤ n and

• θ is an mgu^{4} of (t_{1}, …, t_{m}) and (s_{1}, …, s_{m}).

and

K̇(t_{1}, …, t_{n}) ∩ K̇(s_{1}, …, s_{m}) ⟼^{P} 0  (26)

if no unifier of (t_{1}, …, t_{m}) and (s_{1}, …, s_{m}) exists.

These rules are sound with respect to RelΣ-interpretations (lemma 3.4).

Another meta-reduction is

W (σ)^{o}K̇(t_{1}, …, t_{n})W (σ) ⟼^{P}  K̇(t_{σ(1)} …, t_{σ(n)})  (27)
I_{k}K̇(t_{1}, …, t_{n})I_{k} ⟼^{P}  K̇(t_{1}, …, t_{k})  if k ≤ n.  (28)

4whose range is among the set of terms over the master list of variables x_{1}, ⋯, x_{m}

which is sound with respect to RelΣ-interpretations by lemmas 3.9, 3.10, 3.11 and 3.12.

Each meta-reduction abbreviates a sequence of term rewritings. That is to say, is equationally derivable in the theory RelΣ. The chief aim of the translation presented in this paper is to exploit the benefits of variable free rewriting in compilation, so it is essential that, in practice, these reductions be carried out within the relational syntax. The presentation of this rewriting system and a proof of its correctness is straightforward, but lengthy. It will not be discussed further in this sketch.

We also use some bona-fide rewriting rules, which are just directed equations from the theory of Distributive Relation Algebras, or fp-algebras, hence obviously sound for RelΣ- and fp-interpretations.

Table 1: Nondeterministic Logic Programming Reductions

\begin{matrix}(A ∪ B) ∩ C & ⟼^{P} & (A ∩ C) ∪ (A ∩ C) \\ A ∩ (B ∩ C) & ⟼^{P} & (A ∩ B) ∩ C \\ A ∩ (Q ∪ R) & ⟼^{P} & (A ∩ Q) ∪ (A ∩ R) \\ A ∩ fpx.E(x) & ⟼^{P} & A ∩ E(fpx.E(x)) \\ \overline{p}_{i} & ⟼^{P} & F_{i}(\overline{p}_{1}, …, \overline{p}_{n}) (1 ≤ i ≤ n) \end{matrix}

Table 2: Meta-reductions

A ∩ I_{m}QI_{m}  ⟼^{P} I_{m}[I_{m}AI_{m} ∩ Q]I_{m} ∩ A
A ∩ W (σ) QW (σ)^{o}  ⟼^{P} W (σ) [W (σ)^{o} AW (σ) ∩ Q]W (σ)^{o}
W (σ)^{o}K̇(t_{1}, …, t_{n})W (σ) ⟼^{P}  K̇(t_{σ(1)} …, t_{σ(n)})
K̇(u) ∩ K̇(v)  ⟼^{P}  K̇(θv)  (θ = mgu(u, v), ∥ u ∥≤∥ v ∥)
K̇(v) ∩ K̇(u)  ⟼^{P}  K̇(θv)  (θ = mgu(u, v), ∥ u ∥≤∥ v ∥)
K̇(v) ∩ K̇(u)  ⟼^{P} 0  (u, v not unifiable)
I_{s}K̇(t_{1}, …, t_{n})I_{s}  ⟼^{P}  K̇(t_{1}, …, t_{s})  (s ≤ n)

6.1 The evaluation strategy

The typical query

K̇(t⃗_{1} … t⃗_{m}) ∩ \overline{q_{1}}′ ∩ … ∩ \overline{q_{m}}′.

is evaluated as follows:

1. Associate to the left (second reduction):

(K̇(t⃗_{1} … t⃗_{m}) ∩ \overline{q_{1}}′) ∩ … ∩ \overline{q_{m}}′,

where, since \overline{q_{1}}′ is W (σ_{1})\overline{q_{1}}W (σ_{1})^{o},

2. apply the modular law in the form of the second meta-reduction:

W (σ_{1})(W (σ_{1})^{o}K̇(t⃗_{1} … t⃗_{m})W (σ_{1}) ∩ \overline{q_{1}})W (σ_{1})^{o} ∩ … ∩ \overline{q_{m}}′,

apply the third meta-reduction (which permutes the indices of the sequence t⃗_{1} … t⃗_{m})

W (σ_{1})(K̇(t⃗_{σ_{1}(1)} … t⃗_{σ_{1}(m)}) ∩ \overline{q_{1}})W (σ_{1})^{o} ∩ … ∩ \overline{q_{m}}′,

3. replace \overline{q_{1}} by its definition Θ_{1} ∪ \overline{Θ}_{2} where \overline{Θ}_{2} is ⋃_{2≤i≤r} Θ_{i} for some r:

W (σ_{1})(K̇(t⃗_{σ_{1}(1)} … t⃗_{σ_{1}(m)}) ∩ [Θ_{1} ∪ \overline{Θ}_{2}])W (σ_{1})^{o} ∩ \overline{q_{2}}′ … ∩ \overline{q_{m}}′.

and 4. Distribute the first ∩ accross the union:

W (σ_{1})([(K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ Θ_{1}) ∪ (K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ \overline{Θ}_{2})])W (σ_{1})^{o} ∩ \overline{q_{2}}′ ∩ … ∩ \overline{q_{m}}′. (29)

Now we concentrate on the evaluation of (K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ Θ_{1}) which is an expression of the form (see (15)):

K̇(t⃗_{σ_{1}(1)} … t⃗_{σ_{1}(m)}) ∩ I_{s}[K̇(u⃗) ∩ W (τ_{1})\overline{q_{i1}}W (τ_{1})^{o} ∩ ⋯ ∩ W (τ_{ℓ})\overline{q_{iℓ}}W (τ_{ℓ})^{o}]I_{s}.

5. Now we apply the first meta-reduction:

I_{s}[I_{s}K̇(t⃗_{σ_{1}(1)} … t⃗_{σ_{1}(m)})I_{s} ∩ K̇(u⃗) ∩ W (τ_{1})\overline{q_{i1}}W (τ_{1})^{o} ∩ ⋯ ∩ W (τ_{ℓ})\overline{q_{iℓ}}W (τ_{ℓ})^{o}]I_{s} ∩ K̇(t⃗).

Observing that t⃗_{σ_{1}(1)} is precisely the truncation of the sequence t⃗_{σ_{1}(1)} … t⃗_{σ_{1}(m)} to its first s components, and that t⃗_{σ_{1}(1)} is precisely t⃗_{1} (since the first selector permutation is in fact the identity) and applying the last meta-reduction:

I_{s}[K̇(t⃗_{1}) ∩ K̇(u⃗) ∩ W (τ_{1})\overline{q_{i1}}W (τ_{1})^{o} ∩ ⋯ ∩ W (τ_{ℓ})\overline{q_{iℓ}}W (τ_{ℓ})^{o}]I_{s} ∩ K̇(t⃗).

Letting u⃗′ be the result of applying mgu(u⃗, t⃗_{1}) to u⃗, we obtain

I_{s}[(K̇(u⃗′) ∩ W (τ_{1})\overline{q_{i1}}W (τ_{1})^{o}) ∩ ⋯ ∩ W (τ_{ℓ})\overline{q_{iℓ}}W (τ_{ℓ})^{o}]I_{s} ∩ K̇(t⃗).  (30)

This brings us back to the evaluation of a basic form term-sequence ∩ W (relation-variable)W^{o}

K̇(u⃗′′) ∩ W (τ_{1})\overline{q_{i1}}W (τ_{1})^{o}

so we proceed as before, left-to-right.

As we are, in essence, reducing the entire SLD-tree, termination requires a finite SLD-tree. To simulate search along one branch, we would have to define termination to mean the reduction to a relation term one of whose unionands is relation-variable-free. This can be enforced with a different reduction strategy that we will not consider here. See [Ruhlen] for details.

6.1.1 Returning answers

The meta-reduction rules have the effect of reducing every composition and intersection of a K-term K̇(t⃗) that can occur in evaluation to another K-term. Thus a resulting variable-free expression will be a union of such terms. These expressions, which constitute a normal form of the rewriting system, can be returned to the user, or alternatively, they can be printed as a normalized constraint-set description of the solution. This notion of printing has been described in [BroLip]. Although this extra strength is not exploited in the results of this paper, the printing algorithm reduces any variable-free relation expression using the full relation-algebra connectives (that is to say, including negation) to a two-quantifier formula in which negation occurs only immediately before atomic formulas (equations between terms) using the quantifier elimination algorithm of Mal’cev [Mal’cev], also described in [Maher]. It is therefore able to return readable answers to a considerably stronger relational rewriting system in which arbitrary first-order constraints over the Herbrand Universe are used as queries and outputs. The quantifier elimination process is the basis of Constructive Negation [Chan, Stuckey].

6.2 Soundness and Completeness of Evaluation

Soundness of evaluation is an immediate consequence of the fact that every rewrite rule R ⟼^{P} R′ is equationally sound: in any interpretation into P(T_{Σ}^{+} × T_{Σ}^{+})

[[R]] = [[R′]]

Suppose we are given a program P and a query G as in (23), with a finite SLD tree with leftmost selection rule. Since our reduction system is equationally sound, and the adequacy theorem shows that a pair of ground terms (u, u) is in [[A_{G}]]^{∗}|_{s} precisely when the components of u make the query true in the least Herbrand Model of P, the only way completeness can fail to hold is if evaluation of A_{G} fails to terminate. If it does terminate, i.e. A_{G} reduces to a closed term A, then we have the following:

1. [[A_{G}]]^{∗} = [[A]]^{∗}.

2. For s the number of terms in query G, [[A_{G}]]^{∗}|_{s} = {(u, u) : u ground and M_{P} ⊧ G(u)} where M_{P} is the least Herbrand model of P.

Thus, in order to establish completeness it suffices to prove the following theorem.

Theorem 6.2 Suppose G = q_{1}(t⃗_{1}), …, q_{m}(t⃗_{m}) is a query for a logic program P, and has a finite SLD tree with the leftmost selection rule. Let A_{G} be the relational query associated with G. Then there is a closed term A such that A_{G} ⟼^{P} A.

Proof: By induction on the depth of the given SLD tree. Suppose G has the following finite SLD tree:

[figure: G = q_{1}(t⃗_{1}), …, q_{ℓ}(t⃗_{ℓ}); θ_{1}; ⋯; θ_{n}; G_{1} · · · · · · · · · G_{n}]

where each G_{i} is of the form

B_{i}θ_{i}, q_{2}(t⃗_{2}θ_{i}), …, q_{m}(t⃗_{m}θ_{i}).

and where B_{i} is the tail of the i-th clause in the program P whose head predicate is p_{1}:

p_{1}(u⃗_{i0}) : −q_{i1}(u⃗_{i1}), …, q_{iℓ}(u⃗_{iℓ}).

Then G_{1} is precisely the goal:

(q_{11}(u⃗_{11}), …, q_{1ℓ}(u⃗_{1ℓ}))θ_{1}, q_{2}(t⃗_{2}θ_{1}), …, q_{ℓ}(t⃗_{ℓ}θ_{1}),

where θ_{i} is a most general unifier of u⃗_{10} and t⃗_{1}.

The SLD tree below this goal is finite (and of smaller depth than the original goal), hence so is the SLD tree (with left-most selection rule) below the first subgoal G_{11} = q_{11}(u⃗_{11}θ_{1}).

Let A_{G_{11}} be the relational translation of this goal, namely

K̇(u⃗_{11}θ_{1}) ∩ q_{11}

We may apply the induction hypothesis to conclude that our evaluation strategy will reduce A_{G_{11}} to a relation-variable-free A_{11}, which, in fact, must be the K-term corresponding to the computed answer substitution for this goal.

Recall (from 29) that evaluation of the original query A_{G} yields, in several steps, an expression of the form

W (σ_{1})([(K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ Θ_{1}) ∪ (K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ \overline{Θ}_{2})])W (σ_{1})^{o} ∩ \overline{q_{2}}′ ∩ … ∩ \overline{q_{m}}′.

the leftmost reducible subexpression of which reduces to (30)

I_{s}[(K̇(u⃗_{11}θ_{1}) ∩ W (τ_{1})\overline{q_{11}}W (τ_{1})^{o}) ∩ W (τ_{2})\overline{q_{12}}W (τ_{2})^{o} ∩ ⋯ ∩ W (τ_{ℓ})\overline{q_{1ℓ}}W (τ_{ℓ})^{o}]I_{s} ∩ K̇(t⃗).

Since the first selector W (τ_{1}) is the identity, the leftmost reducible subterm K̇(u⃗_{11}θ_{1}) ∩ W (τ_{1})\overline{q_{11}}W (τ_{1})^{o} is precisely A_{G_{11}} which reduces to A_{11}. We are left with (using primes to hide the switching relations W):

W (σ_{1})(I_{s}[A_{11} ∩ \overline{q_{12}}′ ∩ ⋯ ∩ \overline{q_{1ℓ}}′]I_{s} ∩ K̇(t⃗) ∪ (K̇(t⃗_{σ_{1}(m)} … t⃗_{σ_{1}(m)}) ∩ \overline{Θ}_{2}))W (σ_{1})^{o} ∩ \overline{q_{2}}′ ∩ … ∩ \overline{q_{m}}′.

The stack of goals (relation-variables) present is bounded by the size of the original SLD tree, and for each one we argue in the same way, eventually producing a union of relation-variable free goals

A = A′_{1} ∪ … ∪ A′_{ν}

where ν is the number of success nodes on the fringe of the original SLD tree.

7 Related and Future Work, and Conclusions

There have been other efforts in the literature to remove variables from Prolog, and to make evaluation and compilation more algebraic. Bellia and Occhiuto develop an algebra of programs that captures unification, rewriting and narrowing in [BelOcc]. Our work rests heavily on the fact that such an algebra can be found within the relation calculus, whose semantics is well-understood, and which admits natural extensions to higher-order and linear contexts, as well as a rich representation theory (see e.g. the treatment of Allegories in [FreySce]). The compilation process described here can be viewed as an application of the canonical inclusion of a regular category into its associated category of relations. The greater generality of the categorical framework opens the way to applying this technique to extensions of the logic and to constraints, as well as to a denotational treatment based on relations, which we are currently exploring.

Categorical treatments of logic programming provide alternative ways of algebraicizing the subject, which are, in a sense, variable free (see e.g. [AspMart, Diac, PowKin, FFL, NFDP, Pym]). Corradini and Montanari [CorMont] have given a categorical analysis of logic program execution in terms of transition systems. None of these approaches have as yet been applied to compilation or the definition of an abstract machine for logic programs, although this might be an interesting alternative to the work in this paper.

At this point there are a number of questions raised by this approach which we hope to address. Can a significant portion of our relational machine be captured with a Church-Rosser, strongly normalizing set of rewrite rules? Comon and Jouannaud and Kirchner’s work [Comon, CoHaJo] on rewriting systems for unification and disunification suggests that this is quite feasible, as does the work of Bellia and Occhiuto, op. cit.

We would also like to exploit the rich semantics of relational formalisms to obtain new notions of observables, and abstract interpretation, as well as to extend the relational compilation to higher-order logic programming.

To some extent this work was a foray into the terrain of relation-based computing as a separate discipline, with logic programming as an extended case-study . Some instances of “pure” relational programming languages, of limited expressive power, were studied in [BroLip]. A useful rewriting system for the full relation calculus seemed a lot to ask for in the absence of some computational paradigm and we thought it would help, at the start, to anchor such a system in logic programming-inspired reductions.

Work by the RUBY group at Oxford on hardware [BroHut, JonShe], and on program synthesis via relations by Bird and de Moor[Algebra], Maddux[Maddux, RelSem], Naumann [Naumann] and Backhouse [Backh], to name a few of the many researchers in this field, suggests that the relational paradigm can provide significant computational insights at almost every level of the field. Exploration –via relations– of possible connections between program synthesis and a more general notion logic of programming seems particularly tempting.

References

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

[WAM] Hassan Ait-Kaci, Warren’s Abstract Machine: A Tutorial Reconstruction, MIT Press, Series in Logic Programming. 1991.

[Backh] Backhouse, R, et. al., “A Relational Theory of Data Types,” in Workshop on Constructive Algorithmics: The Role of Relations in Program Development, Utrecht University, 1990.

[Backus] Backus, J., “Can Programming be liberated from the von Neumann style?” in ACM Turing Award Lectures, ACM Press (Addison-Wesley), New York, 1987.

[BakRoe] de Bakker, J. and de Roever, “A Calculus for Recursive Program Schemes” , ed. Nivat, A., in Automata, Languages and Programming, 1973.

[BelOcc] Bellia, M., and Occhiuto, M. E., “C-expressions, a variable-free calculus for equational logic programming”, in Theoretical Computer Science 107, Elsevier, 1993.

[Naumann] David A. Naumann “A recursion theorem for predicate transformers on inductive data types”, Information Processing Letters, volume 50, 6, pp. 329–336, 1994.

[BirdMoor1] R S Bird, Oege de Moor and P Hogendijk. Generic programming with types and relations. Journal of Functional

Programming, 6(1), 1996.

[Algebra] Bird, R. S. and De Moor, O. Algebra of Programming. Prentice Hall, 1996

[BroHut] Brown, C. and Hutton, G., “categories, Allegories and Circuit Design”, in Proceedings of the 9th Symposium on Logic in Computer Science, IEEE, 1994.

[Broome86] Broome, P. Transformations of Parallel Programs with Higher-order Relational Operators, Ph. D. dissertation, Univ. of Delaware, 1986.

[Broome91] Broome, P. “Applications of Algebraic Logic to Recursive Query Optimization,” 8th Army Conference on Applied Mathematics and Computing, 1991.

[BrLi92] Broome, P., and Lipton, J., “Constructive Relational Programming”, Transactions of the 9th Army Conference on Applied Mathematics and Computing, ARO-Report 92-1, 1992.

[BroJon] Brown, Carolyn and Jones, G., “Hardware Component Allegories”, in Proc. LICS 1994, IEEE.

[Chap] Compilation of Logic Programs to a Relational Machine, Honors Thesis, Wesleyan University, 1997.

[Chan] Chan, D. Constructive Negation Based On the Completed Database, Logic Programming: Proceedings of the Fifth International Conference and Symposium Eds. R. A. Kowalski and K. A. Bowen, MIT Press, Cambridge, MA, pp 111–125, 1988.

[Clark] Clark, K., “Negation as Failure”, in Logic and Data Bases, Gallaire and Minker eds., Plenum Press, New York, 1978.

[CorMont] Corradini, A. and Montanari, U. An algebraic semantics for structured transition systems and its application to logic programs. In Theoretical Computer Science 103. Elsevier, 1993.

[Comon] Comon, H. “Disunification, A Survey”, in Logic and Automation, Lassez and Plotkin, eds., MIT, 1992.

[CoHaJo] Comon, H., Haberstrau, M., Jouannaud, J-P, “Decidable problems in shallow equational theories”, in Proc. 7th. Symp. of LICS, IEEE Computer Society Press, 1992.

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

[BroLip] Broome, P and Lipton, J., “Combinatory Logic Programming: Computing in Relation Calculi” in Proceedings of the 1994 International Symposium on Logic Programming, M. Bruynooghe, ed., M.I.T. Press, pp. 269-285, 1994.

[Colp] Lipton, J., “A Relational Foundation for Logic Programming”, to appear.

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

[FriasMad] “Completeness of a Relational Calculus for Program Schemes”, proceedings of LICS 98, IEEE, 1998.

[FFL] Finkelstein, S., Freyd, P. and Lipton, J., “Logic Programming in Tau-Categories”, in Computer Science Logic ’94 , LNCS 933, Springer, pp. 249-263, 1995.

[Freyd92] e-mail manuscript, Categories, Relations and Computation bulletin board, Feb. 15, 1992.

[FreySce] Freyd,P. and Scedrov, A., Categories,Allegories, North-Holland, 1990.

[NFDP] Finkelstein, S., Freyd, P. and Lipton, J., “A New Framework for Declarative Programming”, to appear in Theoretical Computer Science, Elsevier.

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

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

[JonShe] Jones, G. and Sheeran, M., “Circuit Design in RUBY”. In Formal Methods in VLSI Design, ed. J. Staunstrup, North-Holland, 1990.

[Lloyd] Lloyd, J. W., Foundations of Logic Programming, second ed., Springer-Verlag, 1987.

[Maddux] Maddux, R., “Introductory course on relation algebras, finite-dimensional cylindric algebras, and their interconnections”, in Algebraic Logic (Proc. Conf. Budapest 1988) ed. by H. Andreka, J. D. Monk, and I. Nemeti, Colloq. Math. Soc. J. Bolyai 54 North-Holland Amsterdam, 1991, 361–392.

[RelSem] Maddux R., Relation-Algebraic Semantics, in Theoretical Computer Science, Volume 160, June 1996.

[Maher] Maher, M., “A Complete Axiomatization of the Theories of Finite, Rational and Infinite Trees” Proceedings of the third IEEE Symposium on Logic and Computer Science, 1988.

[MdM96] R. McPhee and O. de Moor, ”Compositional Logic Programming”, in Proceedings of the JICSLP’96 postconference workshop: Multi-paradigm logic programming, M. Chakravarty and Y. Guo and T. Ida, eds., Technische Universität Berlin, also PRG Report 96-28, Oxford, 1996.

[Mal’cev] Mal’cev, A.I.,“On The Elementary Theories of Locally Free Universal Algebras”, Soviet Math. Doklady, 1961,

pp.768-771.

[Miller] Miller, M., Nadathur, G., Pfenning, F. and Scedrov, A., “Uniform Proofs as a Foundation for Logic Programming.” Annals of Pure and Applied Logic, 1990.

[Moor92] de Moor, Oege, Categories, Relations and Dynamic Programming, Dissertation, and Technical Monograph PRG-98, Oxford Computing Lab, Oxford, 1992.

[MycOk] A. Mycroft and R. A. O’Keefe. A Polymorphic Type System for Prolog. Artificial Intelligence, 23(3):295–307, 1984.

[Peirce] Pierce, C.S., The Logic of Relatives, Studies in Logic. Johns Hopkins University, Baltimore, 1882, 235-277.

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

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

[deRoe] de Roever, W.P., “Recursion and Parameter Mechanisms: an Axiomatic Approach”, Report IW 20/74, Matematisch Centrum, Amsterdam, 1974.

[Ruhlen] Development of a Rewrite System for Relational Algebra Equations Modeling Horn Clause Resolution Master’s Thesis, Wesleyan University, 1997.

[Schmidt] Schmidt, G. and Ströhlein, T., Relations and Graphs, EATCS Monographs, Springer, 1993.

[Shep88] Sheperdson, J.C., Negation in Logic Programming, in Deductive Databases and Logic Programming, Jack Minker, Rd., Morgan Kaufman, Los Altos, CA, 1988.

[Stuckey] Stuckey, P. “Constructive Negation for Constraint Logic Programming” in Proceedings of the 6th IEEE Symposium on Logic and Computer Science, New York, pp.328-339, 1991.

[TarGiv] Tarski, A. and Givant, S., A formalization of set theory without variables, Colloquium publications, V. 41, American Mathematical Society, Providence, RI, 1987.