Combinatory Logic Programming: Computing in Relation Calculi ^{∗}

Paul Broome 1620 Creston Dr. Forest Hill, Md.21050

             broome@msiadmin.cit.cornell.edu

James Lipton Dept. of Mathematics Wesleyan University Middletown, CT 06459

                                                   lipton@allegory.cs.wesleyan.edu

Abstract

We define a combinatory relational calculus based on a variant of the Relation Algebra formalism (developed by Tarski-Givant, and in more general form by Freyd and others) which extends traditional database query formalisms in a number of ways. It is a variable-free calculus for rewriting relation expressions built up from ground relations using union, intersection, complementation, composition and a fixed point operator. The language extends conventional Horn-clause programming with constraints (e.g. constructive negation) by permitting queries and outputs to be relation expressions. We also define an associated relational programming language RAlog which combines rewriting in the calculus with a quantifier-elimination algorithm due to Mal’cev. The algorithm is used to translate reduced relation expressions in the calculus into two-quantifier formulas, which constitute the printed output of the language.

The relational calculi and programming language discussed in this paper (RAlog) arose from an attempt to abstract the second order or pure relational content of logic programs as objects that bind relation variables and formally define relations somewhat the way lambda terms formally define functions. There are several benefits to be gained from such an attempt: to combine the declarative transparency and reversibility of logic programming with some of the features of functional programming languages, and to open the way for a new denotational treatment of the semantics of declarative programming. In this paper we use the relation algebra formalism as an executable algebra of programs, somewhat in the Backus tradition[Backus], to “liberate logic programming from the von Neumann style.” Another objective has been to make constraint manipulation and some features of control more transparent and declarative by finding a unified calculus which express constraints, program transformation, evaluation and the logic program itself.

1 Combinatory Logic Programming

It will prove helpful to start by considering an example of the process of abstracting the relational content of a simple logic program. We illustrate with the Prolog program for the reflexive transitive closure of a simple graph, and two queries.

∗An abbreviated version of the paper appeared in the proceedings of the 1994 International Logic Programmming Symposium, M. Bruynooghe, ed., M.I.T. Press.

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

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

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

Translating the program: We introduce the binary relation symbols conn and edge (and let the font difference suffice to distinguish between program predicates and the new symbols), and translate the program into a pair of relation equations. conn will be a variable standing for a relation defined via an equation. edge will stand for an expression which explicitly describes a finite binary relation on the Herbrand universe H of the program. For readability, we denote composition of relations by “ ; ” .

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

where id denotes the identity relation. We rewrite the last equation as conn = fpx.(id ∪ edge; x) where the operator fp means “least fixed point of”. The first query above is represented by {(a, c)}∩conn and the second by (1; {(c, c)}) ∩ conn where 1 is the universal relation H × H, (hence (1; {(c, c)}) represents the set of all pairs whose second component is c). A solution to the first query would have be to be of the form {(a, c)}, confirming that (a, c) ∈ conn, or 0, denoting the empty relation, if not. A solution to the second query should be some more explicit description, such as {(a, c), (b, c), (c, c), (l, c)}. We proceed to evaluate the second query informally, to motivate the calculus we will present below. A natural first strategy is to unfold the recursive definition of conn:

1; {(c, c)} ∩ conn = (1; {(c, c)} ∩ id) ∪ (1; {(c, c)} ∩ edge; conn)

The first term can be reduced to {c, c}, and the second can be further unfolded.

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

Continuing this way, we will eventually obtain the term 1; {(c, c)} ∩ (edge; edge) which is equal to {(a, c)}. The next unfolding gives us 1; {(c, c)} ∩ (edge)^{(3)}; conn. edge is finite: in fact for any X > 2, (edge)^{(X)} = 0 hence we are done. The query evaluates to {(c, c)} ∪ {(b, c), (l, c)} ∪ {(a, c)} which is simply {(c, c), (b, c), (l, c), (a, c)}.

However what happens if we have a relation R defining an infinite acyclic graph and we pick a pair {(u, v)} not in R? We run the risk of expanding {(u, v)} ∩ R forever despite the fact that the chosen pair is not a member. Clearly we need to use other facts about relations if we are to proceed at least as efficiently as Prolog. This means being able to compute 0 whenever Prolog would compute “no”. By using the so-called modular law in one of its many equivalent forms

A ∩ R; S = A ∩ R; (R^{o}; A ∩ S) or A ∩ R; S = A ∩ (A; S^{o} ∩ R); S

and computing the expression R^{o}; A or A; S^{o} before proceeding we are able to show (via equational reasoning) that the right hand term vanishes, and the computation terminates. This is illustrated by the following example.

     le(X,X).
     le(X,Y):-pred(X,Z),le(Z,Y).

                                                  pred(s(X),X).

      | ?- le(s(a),s(b)).

We translate the program by id∪pred; le and the query by (s(a), s(b))∩le. First, unfold le, distribute its definition, note that {(s(a), s(b))} ∩ id is 0, and apply the modular law.

{(s(a), s(b))} ∩ le
= {(s(a), s(b))} ∩ (id ∪ pred; le)
= {(s(a), s(b))} ∩ pred; le)
= {(s(a), s(b))} ∩ pred; (pred^{o}; {(s(a), s(b))} ∩ le) by the modular law
= {(s(a), s(b))} ∩ pred; ({(a, s(b))} ∩ le)
= {(s(a), s(b))} ∩ pred; ({(a, s(b))} ∩ id) ∪ {(a, s(b))} ∩ pred; le))

Since the pair (a, s(b)) is not in id then the expression simplifies to

= {(s(a), s(b))} ∩ pred; (0 ∪ {(a, s(b))} ∩ pred; le))

= {(s(a), s(b))} ∩ pred; ({(a, s(b))} ∩ pred; (pred^{o}; {(a, s(b))} ∩ le)) = {(s(a), s(b))} ∩ pred; ({(a, s(b))} ∩ pred; (0 ∩ le)) = 0

Since pred^{o}; {(a, s(b))} = 0 then the entire expression is the empty relation.

These examples motivate the goals of this paper, but serious questions need to be resolved. How carefully handpicked are they? Is there a general calculus and reduction strategy that will always work at least as well as a Prolog computation? Can this help us extend the notion of declarative programming to a broader context?

The next two sections of this paper are devoted to making precise the relational syntax, program translation and notions of reduction motivated by this example. A key aim of this paper is to delineate the main components of a new relational programming paradigm. Computation in this formulation means relation calculus rewriting of queries (relation expressions) to members of some distinguished class of relation expressions (usually recursion-free terms), followed by representation of such expressions in a human readable form in a way that depends on the data domain, a process here called printing.

query⟶ Rewriting in a relational theory reduced form →  Printing ⟶ solution

In the main example studied in this paper, data means terms in a Herbrand Universe, and printing will involve a quantifier elimination algorithm that makes use of special properties of the Herbrand Universe. We will also define a general translation that maps Prolog programs and queries into a variable-free relation expression, and maps Prolog evaluation with a given interpreter into a particular reduction strategy, which we call embedded Prolog. We conclude by showing how the relational calculus extends the query and output language of Prolog and incorporates a robust notion of constraint programming in a natural way. Finally, we discuss new approaches to logic programming semantics opened up by the translation to a relational formalism.

2 The Relational Calculus

We first define the syntax of the equational theory we will be using.

Definition 2.1 Assume given a set Rvar of relation variables. ℜ, the set of pure relational expressions, is the collection of terms R generated by the following BNF grammar:

R ::= ⟨Rvar⟩ | id | di | 1 | 0 | hd | tl | R^{o}
R ∪ R | R ∩ R | \overline{R} | RR | fp⟨var⟩.(R)

Let L be a finite language comprised of a set of constant symbols {a_{1}, a_{2}, …, b_{1}, b_{2}, …} and a set of function symbols each with a given arity. Then ℜ_{L}, the set of L -term relation expressions is the collection of terms generated by the grammar for ℜ and the additional rules

R ::= {(t_{1}, t_{2})} | f_{i}^{n}

where the t_{i} are terms over L, f is a function symbol of arity n and 1 ≤ i ≤ n.

Definition 2.2 A relation expression is atomic if it is one of {f_{i}^{n}, hd, tl, id, di, 1, 0}, and finitary if it contains no occurrences of fp. A relation expression is positive if it contains no occurrences of complementation, strictly positive if di does not occur, and simple if no complementation symbol occurs within the scope of an fp- operator.

Juxtaposition indicates relation composition as does “;” when needed for clarity. The converse of R is R^{o}. A pair of constant terms is denoted by {(t_{1}, t_{2})}. The projection symbol f_{i}^{n} is intended to denote the relation between terms f(u_{1}, …, u_{n}) with n arguments and the ith argument u_{i}.

2.1 Extensional Semantics and Correctness

ℜ and ℜ_{L} become computation calculi when equipped with a rewrite relation ⟼^{e} on pairs of terms. We will use ⟼^{e}_{∗} to stand for its reflexive transitive closure.

We begin by defining a standard semantics along the lines of the fixed point semantics for Prolog, here called extensional because it characterizes the meaning of a relation expression thought of as a logic program by the set of successful queries, i.e. the operational extension of the program predicates.

We will need a standard pairing operator, in order to reduce relations of any arity to binary ones. Any binary function symbol will do, so we introduce the infix [ | ] as a “reserved” binary function symbol^{1} We assume that [ | ] ∈ L .

Let U be an L -algebra i.e. a structure for the language L, and η : Rvar → U a U-environment. We define the interpretation

[[ ]]^{U}_{η} : ℜ → R_{L}

relative to environment η to be the standard association of sets with relation expressions, e.g.

[[hd]]^{U}_{η}  ≡^{def} {([t_{1}|t_{2}], t_{1}) : t_{1}, t_{2} ∈ U}  [[R ∪ S]]^{U}_{η}  ≡^{def} [[R]]^{U}_{η} ∪ [[S]]^{U}_{η}
[[1 ]]^{U}_{η}  ≡^{def} U × U  [[R ∩ S]]^{U}_{η}  ≡^{def} [[R]]^{U}_{η} ∩ [[S]]^{U}_{η}

[[f_{i}^{n}]]^{U}_{η} ≡^{def} {(x, y) : (∃v_{1} ⋯ v_{n−1})(x = f(v_{1}, …, v_{i−1}, y, v_{i}, …, v_{n−1}))

[[fpx.E (x) ]]^{U}_{η} ≡^{def} ⋃_{n≥0} [[E ^{(n)}(x) ]]^{U}_{η}

where E ^{(0)}(x) = 0 and E ^{(n+1)}(x) = E (E ^{(n)}(x)). For most of this paper we fix a finite language L, and take the universe U above to be H_{L} the Herbrand universe or free term algebra made up of all variable-free terms over L. Letting R_{L} be the Boolean algebra of binary relations on H_{L} , and omitting reference to the environment η we define the standard interpretation [[ ]] : ℜ → R_{L} to be [[ ]]_{η}^{H_{L}}

Definition 2.3 A relation R on a set S is functional if R^{o}R ⊆ id, reflexive if id ⊆ R, and coreflexive if R ⊆ id.

We also define analogous notions for syntactic relation expressions.

Definition 2.4 We will call a relation expression functional if it is built up by compositions or intersections from the functional atomic relations hd, tl, f_{i}^{n}, id, (u, u). We call an expression R coreflexive if it is a union or intersection of expressions of the form A ∩ id, (u, u).

Coreflexive relations can be thought of as encoding data in a set-theoretic interpretation, e.g. ℕ can be represented as {(n, n) : n ∈ ℕ } and a value 3 as the coreflexive {(3, 3)}. Note that we can easily represent the domain and range of any relation R as coreflexives: Dom(R) = RR^{o} ∩ id, Ran(R) = R^{o}R ∩ id.

Definition 2.5 Let R be a relation expression, and ↦^{e} a rewriting system. Then we define the erelational success set RSS (e, R) to be

RSS (e, R) = {(t_{1}, t_{2}) : (t_{1}, t_{2}) ∩ R⟼^{e}_{∗} (t_{1}, t_{2})}

where the right hand reduction means: there is an e-reduction sequence ending with (t_{1}, t_{2}). If Uis an L -algebra then RSS (e, R)_{U} is the set of interpretations in Uof the pairs of terms (t_{1}, t_{2}) such that

(t_{1}, t_{2}) ∩ R⟼^{e}_{∗} (t_{1}, t_{2}).

1If we write this binary function symbol as a prefix pr, then hd and tl are just pr_{1}^{2} and pr_{2}^{2}.

Definition 2.6 Let L be a language, ⟼^{e} a rewriting system and ℜ̂ ⊆ ℜ_{L}. Then we say e is extensionally complete with respect to ℜ̂ (on U) if for every simple relation expression R in ℜ̂,

RSS (e, R)_{U}  =  [[R]]_{U}

in other words for every pair of terms (t_{1}, t_{2}) there is a reduction sequence from (t_{1}, t_{2}) ∩ R to (t_{1}, t_{2}) if and only if the interpretation in Uof (t_{1}, t_{2}) is in [[R]]_{U}. Let ≡_{e} be an equational theory. Then ≡_{e} is extensionally complete with respect to ℜ̂ (on U) if for every simple relation expression R in ℜ̂, and terms t_{1} and t_{2},

(t_{1}, t_{2}) ∩ R ≡_{e} (t_{1}, t_{2})

if and only if the interpretation in Uof (t_{1}, t_{2}) is in [[R]]_{U}.

Without restricting the class of relational terms, we cannot in general expect extensional completeness, since it implies that all definable relations on a universe U are recursively enumerable. We now show extensional completeness for ⟼^{r} ∪ ⟼^{t}, the system in Table 1 and two simple restricted classes of relations.

Theorem 2.7 Let ℜ̂ be the set of relation expressions built up from atomic relations and compositions of pairs of strictly positive relations, using only ∪, ∩, ( )^{o}. Then ⟼^{r} ∪ ⟼^{t} is extensionally complete with respect to ℜ̂ on the Herbrand universe.

Proof: The soundness direction is immediate, every reduction rule above is a directed equation that is clearly valid in the [[·]] interpretation. That is to say if X ↦ Y then [[X]] = [[Y ]]. We prove completeness by induction on the structure of R. The atomic cases (R = id, di, hd, tl, (f_{i}^{n}), 1, 0, {(u, v)}) are easy.

\underline{R is S ∪ T}: Then (t_{1}, t_{2}) ∈ [[R]] implies (t_{1}, t_{2}) ∈ [[S]] or (t_{1}, t_{2}) ∈ [[T ]]. So, in either case, (t_{1}, t_{2})∩R ↦ (t_{1}, t_{2}) ∩ (S ∪ T) ↦ ((t_{1}, t_{2}) ∩ S) ∪ ((t_{1}, t_{2}) ∩ T) which reduces, by induction hypothesis (and two more steps) to (t_{1}, t_{2}).

\underline{R is S ∩ T}: Then (t_{1}, t_{2}) ∈ [[R]] implies (t_{1}, t_{2}) ∈ [[S]] and (t_{1}, t_{2}) ∈ [[T ]]. So, (t_{1}, t_{2}) ∩ R ↦ (t_{1}, t_{2}) ∩ (S ∩ T) ↦ ((t_{1}, t_{2}) ∩ S) ∩ T which reduces, by induction hypothesis to (t_{1}, t_{2}) ∩ T and then to (t_{1}, t_{2}). The cases R of the form (S)^{o}or ST are straightforward and left to the reader.

Definition 2.8 A relation expression R is formative if it is the intersection of expressions built up from singletons (u, u) and id and by zero or more iterations of the operation

X ↦ SXT^{o}

where S, T are one of the f_{j}^{n} or hd or tl.

Lemma 2.9 The rewrite system ⟼^{r} ∪ ⟼^{t} is extensionally complete with respect to formative expressions on the Herbrand universe H_{L} .

Proof: First observe that (u, v) ∩ SXT^{o} ↦ (u, u)SXT^{o}(v, v). Since each term S, T in a formative expression is functional it is easy to check that (u, u)S reduces to some term (u, v) or to 0. Since X is either of the form S′X′(T′)^{o} or (w, w), the original term will reduce to a composition of singletons, and hence to a singleton or 0. By soundness of the reduction rules, if (u, v) ∈ [[SXT^{o}]] it reduces to (u, v).

We will need one more formulation of completeness.

Definition 2.10 A rewriting system e is relation-complete with respect to a pair of sets of relation expressions 𝔔 ⊆ ℜ_{L} (for queries) and 𝔓 ⊆ ℜ_{L} (for programs) if for every expression A ∈ 𝔔 and every R ∈ 𝔓 there is a finitary A′ with [[A′]] = [[A ∩ R]] such that A ∩ R⟼^{e}_{∗} A′ An equational theory ≡_{e} is relation-complete with respect to 𝔔, 𝔓 if for any A ∈ 𝔔and R ∈ 𝔓 there is a finitary A′ such that A ∩ R ≡_{e} A′.

Table 1: Relational rewrite rules

Pure relation reduction rules

\begin{matrix}fpx.E (x) & ⟼^{r} & E (fpx.E (x)) & A ∩ (B ∩ C) & ⟼^{r} & (A ∩ B) ∩ C \\ A ∩ BC & ⟼^{r} & B(B^{o}A ∩ C) ∩ A & A ∩ (A ∪ B) & ⟼^{r} & A \\ A ∩ BC & ⟼^{r} & A ∩ (AC^{o} ∩ B)C & (A ∪ B) ∩ A & ⟼^{r} & A \\ A ∩ B^{o} & ⟼^{r} & (A^{o} ∩ B)^{o} & B ∩ (A ∪ B) & ⟼^{r} & B \\ A ∩ (B ∪ C) & ⟼^{r} & (A ∩ B) ∪ (A ∩ C) & (A ∪ B) ∩ B & ⟼^{r} & B \\ A(B ∪ C) & ⟼^{r} & AB ∪ AC & (B ∪ C)A & ⟼^{r} & BA ∪ CA \\ A(BC) & ⟼^{r} & (AB)C & A ∪ (A ∩ B) & ⟼^{r} & A \\ (AB)^{o} & ⟼^{r} & (B^{o}A^{o}) & (A ∩ B) ∪ A & ⟼^{r} & A \\ AB^{o} & ⟼^{r} & (BA^{o})^{o} & A0 & ⟼^{r} & 0 \\ 0A & ⟼^{r} & 0 & A ∩ 0 & ⟼^{r} & 0 \\ A ∩ 1 & ⟼^{r} & A & 0 ∩ A & ⟼^{r} & 0 \\ 1 ∩ A & ⟼^{r} & A & A ∩ A & ⟼^{r} & A \\ A ∪ 0 & ⟼^{r} & A & A ∪ A & ⟼^{r} & A \\ 0 ∪ A & ⟼^{r} & A & A ∪ 1 & ⟼^{r} & 1 \\ id ∪ di & ⟼^{r} & 1 & 1 ∪ A & ⟼^{r} & 1 \\ di ∪ id & ⟼^{r} & 1 & A id & ⟼^{r} & A \\ 1di & ⟼^{r} & 1 & id A & ⟼^{r} & A \\ di1 & ⟼^{r} & 1 & 0^{o} & ⟼^{r} & 0 \\ id^{o} & ⟼^{r} & id & 1^{o} & ⟼^{r} & 1 \\ di^{o} & ⟼^{r} & di & (A^{o})^{o} & ⟼^{r} & A \end{matrix}

Term-algebra reduction rules

{(u, u)} ∩ id ⟼^{t} {(u, u)}  {(u, u)} ∩ di  ⟼^{t}  0
{(u, v)} ∩ id ⟼^{t} 0  {(u, v)} ∩ di  ⟼^{t}  {(u, v)}
F ∩ id,  ⟼^{t} 0  F ∩ G  ⟼^{t}  0
F^{o}G  ⟼^{t} 0  F (A ∩ B)  ⟼^{t}  F A ∩ F B
id ∩ di  ⟼^{t} 0  ((hd)^{o})tl  ⟼^{t}  1
((tl)^{o})hd  ⟼^{t} 1  ((hd)^{o})hd  ⟼^{t}  id
((tl)^{o})tl  ⟼^{t} id  ((f_{i}^{n})^{o})f_{i}^{n}  ⟼^{t}  id
(f_{j}^{n})^{o}(f_{i}^{n})  ⟼^{t} 1  (f_{j}^{n})^{o}{(f̄, v)}  ⟼^{t}  0
{(u, f̄)}(f_{j}^{n}) ⟼^{t} 0  (hd)^{o}{(ℓ̄, v)}  ⟼^{t}  0
{(u, ℓ̄)}(hd)  ⟼^{t} 0  (tl)^{o}{(ℓ̄, v)}  ⟼^{t}  0
{(u, ℓ̄)}(tl)  ⟼^{t} 0  {(u, v)}{(v, w)}  ⟼^{t}  {(u, w)}
({(u, v)})^{o}  ⟼^{t} {(v, u)}  {(u, f(v_{1}, …, v_{n}))}(f_{j}^{n})  ⟼^{t}  {(u, v_{j})}
{(u, [v|w])}hd ⟼^{t} {(u, v)}  {(u, f(v_{1}, …, v_{n}))}(g_{j}^{m})  ⟼^{t}  0
{(u, [v|w])}tl ⟼^{t} {(u, w)}  1(u, v)1  ⟼^{t}  1
1(f_{i}^{n})  ⟼^{t} 1  1(hd)  ⟼^{t}  1
1(tl)  ⟼^{t} 1  {(u, v)} ∩ A  ⟼^{t}  {(u, u)}A{(v, v)}
A ∩ {(u, v)} ⟼^{t}  {(u, u)}A{(v, v)}

(u, u_{i}, v, v_{i}, w distinct ground terms in L, a, b distinct constants and f, g distinct function symbols of arities n and m.)

F and G range over {f_{i}^{n} ∈ L } ∪ {hd, tl}. ℓ̄ ranges over all terms not beginning with [ | ].

f̄ ranges over terms not beginning with f.

As with previous definitions, relation completeness can be defined relative to an arbitrary L -algebra U.

2.2 Axiomatizing the Herbrand Universe

We review an equational theory which is complete for the Herbrand Universe. While in general completeness for one model fails for recursive first-order theories it so happens that for a given finite language L, the first order theory of the Herbrand Universe H_{L} over L (i.e. {φ : H_{L} ⊧ φ}) is decidable, admitting a partial elimination of quantifiers. This result (and its generalization to any so-called locally free algebra), was originally proven by Mal’cev in 1961 [Mal’cev], and has been further extended case of the algebras of rational and infinite terms and certain quotients of such algebras [Maher, Comon, CoHaJo]. A complete rewriting system for the quantifier elimination procedure is discussed in ,[Comon]. Since we will be making use of these results we restate them here.

Definition 2.11 (The Theory T_{L} ) Let L be a finite language. The theory T_{L} is the following axiom scheme:

(T L1) a ≠ b  ( a and b distinct constants )
(T L2) ∀x(t[x] ≠ x)  ( for each term t[x] containing x distinct from x )
(T L3) ∀x⃗(f(ξ_{1}, …, ξ_{n}) ≠ a) ( a a constant )
(T L4) ∀x⃗( f(ξ_{1}, …, ξ_{n}) = f(η_{1}, …, η_{n}) ⟺ ⋀_{i=1}^{n} (ξ_{i} = η_{i}))
(T L5) ∀x⃗(f(ξ_{1}, …, ξ_{n}) ≠ g(η_{1}, …, η_{m}))  (f ≢ g)
(DC_{L}) ∀x[⋁_{a_{i}∈L} x = a_{i} ∨ ⋁_{f∈L}(∃y_{1} ⋯ y_{α_{f}})x = f(y_{1} ⋯ y_{α_{f}})]

For f ∈ L the arity of f is denoted α_{f} above. Axioms (TL1-5) are also known as Clark’s equality theory in the logic programming community. The so-called Domain Closure Axiom DC_{L} expresses in a first order manner that all individuals are terms over L. It is not a formula unless L is finite.

Theorem 2.12 (Maher,Mal’cev) T_{L} is decidable and complete, i.e. the set of consequences of T_{L} is the theory of the Herbrand model H_{L} .

Definition 2.13 A set formula is normal or in normal form if it is of the form:

(∃v⃗)(⋁_{k} Θ_{k})  (1)

with exactly two free variables xand y, and where v⃗ = (v_{1}, …, v_{n}) for some natural number n and each Θ_{j} is a canonical expression: a conjunction of equations and inequations of the following form:

(x = t_{1}) ∧ (y = t_{2}) ∧ ⋀_{i}(v_{i} = s_{i}) ∧ ⋀_{j}(∀u⃗)(x ≠ p_{j}) ∧ ⋀_{j}(∀w⃗)(y ≠ q_{j}) ∧ ⋀_{ij}(∀z⃗)(v_{i} ≠ r_{ij}) (2)

where t_{1}, t_{2}, s_{i}, p_{j}, q_{j} and r_{ij} are terms in which xand y do not occur, and where the v_{i} are distinct and must occur in either t_{1} or t_{2}.

Theorem 2.14 (Normal Form Theorem) Let φ be a first order formula over L. Then there is a normal formula θ_{R} such that

T_{L} ⊢ φ ⟷ θ  (3)

Definition 2.15 For each finitary relation expression R we define a description φ_{R}(x, y) to be any formula φ_{R} such that [[R]] = {(x, y) : φ_{R}(x, y)} e.g.

φ_{R∪S} (x, y) ≡^{def} φ_{R}(x, y) ∨ φ_{S} (x, y)  φ_{{a;b}}(x, y) ≡^{def} (x = a ∧ y = b)
φ_{R;S} (x, y) ≡^{def} (∃V)(φ_{R}(x, V) ∧ φ_{S} (V, y)) φ_{id}(x, y) ≡^{def} x = y

φ_{f_{i}^{k}}(x, y) ≡^{def} (∃V_{1} ⋯ V_{k−1})(x = f(V_{1}, …, V_{i−1}, y, V_{i}, …, V_{k−1}))

Corollary 2.16 Let R be a finitary relation expression, and φ_{R} an associated description, as defined above. Then there is a normal formula θ_{R} such that

T_{L} ⊢ φ_{R} ⟷ θ_{R}  (4)

and there is an algorithm for so reducing it.

Proof:See [Maher, Comon].

The quantifier elimination result of Mal’cev et. al. serves as a basis for a mechanized translation R ⟼ φ_{R} ⟼ θ_{R}.

Thus, over the Herbrand Universe any finitary relation expression is easily converted into a readable value, namely a normal form. It is an instance of the printing component of the relational computing paradigm discussed in the first section of the paper. This component of processing of relation expressions is implemented in a relation language prototype called RAlog^{2}. Here is an example of a query to the RAlog interpreter and its response :

>> solve (hd;1)*complement((tl;f^1/1;1)*(hd;g^1/1)).
(hd ; 1) * complement((tl ; f ^1 / 1 ; 1) * (hd ; g ^1 / 1))={X;Y:
   X=[X2|X3] ^X2 # g(Y)
 V X=[g(Y)|X2] ^(X3)(X2 # f(X3))
  }.

The printed response stands for:

{(x, y) : (∃x_{2}, x_{3})(x = [x_{2}|x_{3}] ∧ (x_{2} ≠ g(y)) ⋁ x = [g(y)|x_{2}] ∧ (∀x_{3})(x_{2} ≠ f(x_{3})))}.

3 Logic without variables

One of the main results in [TarGiv] due to Tarski, Maddux and Givant, 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 given in the appendix. Tarski and Givant also prove a much stronger prooftheoretic 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 make use of this result for a specific set of equations and signature. But first we sketch a simple proof of a semantic form of this theorem, for the special case of algebras of relations definable on a term algebra by first-order formulas over a given signature. Let L be a finite language. The atomic statements of T_{L} 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 equations of the form x = a or x = f(y_{1}, …, y_{n}) where a is a constant in L 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_{L} to relation expressions as follows. A pair of relations A and B are called conjugated quasiprojections by Tarski, and tabulations by Freyd if they satisfy the axioms (17) in the appendix. Recall that ℜ_{L}always contains the reserved conjugated quasiprojections hd and tl. Let n be a natural number greater than the largest number of variables occurring in any sentence to be considered below. Put:

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

Observe that, in the Herbrand interpretation for u, v ∈ U, we have u [[P_{k}]]v iff v is the k^{th} component^{3} of u. Vectors u satisfying u [[P_{k}]]x_{k} for each k will be denoted u = [x_{1}, x_{2}, …, x_{k}, ⋯, x_{n}] Now define, for (0 ≤ i < n)

2available by ftp from allegory.cs.wesleyan.edu

3Superscripts on the P_{k}^{n} will be omitted when they are clear from context

Q_{i}^{n} = ⋂_{j≠i<n} P_{j}(P_{j})^{∘} E^{n} = ⋂_{j<n} P_{j}(P_{j})^{∘}

Observe that u [[E]]v means u and v have the same components (u)_{i} for (1 ≤ i < n) and 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 θ are 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} & = & P_{i}(a, a)P_{i}^{o} ∩ E & (φ ∧ θ)^{r} & = & (φ)^{r} ∩ (θ)^{r} ∩ E \\ (x_{i} = x_{j})^{r} & = & P_{i}P_{j}^{o} ∩ E & (¬φ)^{r} & = & E − (φ)^{r} \\ (x_{i_{0}} = f(x_{i_{1}}, …, x_{i_{n}}))^{r} & = & ⋂_{j} P_{i_{0}}; f_{j}^{n}; P_{k_{j}}^{o} ∩ E & (∃x_{i}φ)^{r} & = & Q_{i}(φ)^{r}Q_{i} ∩ E \end{aligned}

Then we have the following result.

Theorem 3.1 If θ is a sentence over the language of T_{L} , H_{L} ⊧ θ ⟺ [[(θ)^{r}]] = [[E]]. For open formulas φ with free variables among x_{1}, …, x_{n}

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

The atomic case holds by definition of the relations f_{i}^{n}. The rest of the proof is a straightforward induction on the structure of formulas^{4}.

3.0.1 Equipollence

We will now make use of the central result in Tarski-Givant, namely that first-order reasoning in a relation algebra can be faithfully captured with equational reasoning over the theory QRA (see appendix), a result they call equipollence of the two formalisms. First we state this theorem and several corollaries in the form we shall need in the work that follows. The theory QRA(L) is given in the appendix.

Theorem 3.2 Let L be a finite language containing a binary function symbol p(x, y) and Γ a first-order theory over L from which injectivity of p (∀x∀y∀z∀w(p(x, y) = p(z, w) → x = z ∧ y = w) is derivable. Then

Γ ⊢_{1} φ  iff  (Γ)^{†} ⊢_{e} X_{φ} = 1

where (Γ)^{†} is a set of equational translations X_{γ} = 1 of the formulas γ in Γ, and where ⊢_{1} is first-order derivability and ⊢_{e} is equational derivability in the theory QRA(L) with atomic relation symbols f_{i}^{n} corresponding to the atomic function symbols of arity n of L.

The equipollence result is studied at great length in Tarski and Givant op.cit., where it is extended in several ways relevant to the kind of work discussed in this paper. To cite a few such results: the translation ( )^{†} is recursive and preserves finiteness and decidability of theories. Also, the language L may contain finitely many new binary relation symbols. A similar equipollence result is shown for arithmetic, various systems of set theory and real arithmetic vis-à-vis suitable equational formalisms. The application of such results to capturing set, number-theoretic and real constraint logic programming along the lines of the development below remains to be exploited.

By combining the equipollence theorem with the normal form theorems of the preceding section we obtain

Theorem 3.3 There is an equational theory 𝔈 (extending QRA(L)) such that for any finitary relation expressions R, R′

𝔈 ⊢_{e} R = R′ iff H_{L} ⊧ φ_{R} ⟷ φ_{R′} iff [[R]] = [[R′]]

Just take Γ to be T_{L} in the preceding theorem, with the binary function symbol [ | ] ∈ L. We introduce a family of relational terms that will prove useful in translating logic programs, below.

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

Definition 3.4 Let m ≥ n be integers.

K_{m}(a) = (a, a) K_{m}(x_{i}) = id
K_{m}(f(u_{1}, …, u_{s})) = id ∩ (⋂ (f_{i}^{s}K(u_{i})(f_{i}^{s})^{o}))
K_{m}([t_{1}, …, t_{n}]) = id ∩ (⋂ (P_{i}^{m}K(t_{i})(P_{i}^{m})^{o}))

In the equational theory 𝔈, these relations capture the structure of terms, as the following lemma shows.

Lemma 3.5 Two term vectors t⃗ and s⃗ with all free variables in one distinct from the other are unifiable (with most general unifier θ) if and only if

𝔈 ⊢_{e} K(t⃗) ∩ K(s⃗) = K(θt⃗).

If t⃗ and s⃗ are not unifiable then 𝔈 ⊢_{e} K(t⃗) ∩ K(s⃗) = 0.

Proof: Observe that since each K-term is formative, i.e. intersections of basic terms SBS^{o} which are compositions of functional relations on the left and their converses on the right, with B = id, a singleton or basic, the intersection of two K-terms of the form SBS^{o} ∩ SCS^{o} is provably equal in 𝔈 to S(B ∩ C)S^{o}. Thus the following equation is derivable in 𝔈:

K(t) ∩ K(s) = ⋂_{i} (f_{i}^{s}(K(u_{i}) ∩ K(v_{i}))(f_{i}^{s})^{o})

As we keep peeling off the functional relations f_{i}^{s} and their converses on either side, we obtain 0 if function symbols and/or constants clash, a “collapse” of the form K(u_{i}) ∩ K(u_{i}) = K(u_{i}) wherever they are identical, and, when v is a variable, a merge

S(K(u))S^{o} ∩ S(K(v))S^{o} = S[K(u) ∩ K(v)]S^{o} = S(K(u) ∩ id)S^{o} = S(K(u))S^{o}

which corresponds, in ordinary unification of terms, to the result of replacing the variable v by the subterm u.

Lemma 3.6 There is a translation K̃ of sequences terms in L to formative terms in ℜ_{L}such that two term vectors t⃗ and s⃗ are unifiable (with most general unifier θ and with occurs check) if and only if

𝔈 ⊢_{e} K̃(t⃗) ∩ K̃(s⃗) = K̃(θt⃗).

If t⃗ and s⃗ are not unifiable then 𝔈 ⊢_{e} K̃(t⃗) ∩ K̃(s⃗) = 0.

The existence of the translations K̃ and their properties follows from the the existence of the translation ( )^{†} in the equipollence theorem applied to formulas expressing unifiability of terms (e.g. x = t∧x = s). A specific definition of K̃ and a tedious but straightforward equational derivation of K̃(θt⃗) following standard unification algorithms can also be described. We omit the details here.

Switching Relations

We define a special class of relation expressions used to give a combinatory formulation of permutation, i.e. of the operations of switching components of a vector. First fix n and let P_{1}, …, P_{n} be defined as in 5 in section 3. As before, we suppress the superscript n on the since it is fixed for this discussion. The expressions B_{ij}^{n} defined below will also be written without the n superscript when clear from context.

For each i, j between 1 and n let

B_{ij}^{n} = P_{i}P_{j}^{o} ∩ P_{j}P_{i}^{o} ∩ [ ⋂_{k∉{i,j}}]P_{k}P_{k}^{o}.

The intended interpretation is

⟨x_{1}, …, x_{n}⟩ [[B_{i,j} ]]⟨y_{1}, …, y_{n}⟩ ⟺ x_{i} = y_{j} ^{&} x_{j} = y_{i} ^{&} (∀k)(k ≠ i^{&} k ≠ j → x_{k} = y_{k})

Definition 3.7 For each natural number n we define the n-switching relation expressions (or n-permutations) to be finite compositions of the B_{ij}^{n}.

4 Embedded Prolog

4.1 Relational Logic Programming

We now restrict our attention to the translation of Horn Clause Programs as (recursive) relation equations. Via the fp operator we can then express each relation defined by the program as a single, negation-free relation term. We outline the procedure here. What follows is a description of a series of steps that transform a Horn clause program in which n predicate letters occur, to a set of n (recursive) relational equations consisting only of positive finitary relation expressions in n relation variables p_{1}, …, p_{n}

p_{1} = F_{1}(p_{1}, …, p_{n})
⋮ ⋮ ⋮
p_{n} = F_{n}(p_{1}, …, p_{n})

The transformation of this to a single equation over ℜ_{L}(with occurrences of fp) takes place essentially by a cascading variable elimination procedure which is reminiscent of Gaussian elimination in linear systems.

The question was raised in the introduction as to whether the sample transformation of a prolog program into a relation expression in the first pages was “handpicked” or fully representative of a general procedure. The answer is that a general procedure exists, but that the case considered on the opening page was deceptively simple. In order to come up with a relatively straightforward general transformation procedure we must do considerable violence to the appearance of the program (while preserving extensional and operational semantics). We will increase the arity of all predicates, and introduce many new variables.

Step 1: transforming the program

We first rewrite the original program P so that only distinct variables occur as arguments to the original predicates, via the introduction of fresh variables x_{i} and of equations of the form x_{i} = t_{i} where the t_{i} are terms. For each clause

p(t_{1}, ⋯, t_{n_{p}}) ⟵ q(u_{1}, …, u_{n_{q}}), …

(where n_{p} is the arity of the predicate letter p) we obtain

p(x_{1}, ⋯, x_{n_{p}}) ⟵ x_{1} = t_{1}, …, x_{n_{p}} = t_{n_{p}}, q(y_{1}, …, n_{q}), y_{1} = u_{1}, …, y_{n_{q}} = u_{n_{q}}, …  (6)

If there is more than one clause with a common predicate letter p we rewrite them as a single clause with disjunctions embedded in the tail. Let n be the total maximum number of variables occurring in any one clause. We make every predicate have arity n by adding as many “filler” variables as required. Thus the clause just shown reads:

\begin{matrix}p(x_{1}, ⋯, x_{n_{p}}, y_{1}, …, y_{r_{q}}, …) ⟵ \\ x_{1} = t_{1}, …, x_{n_{p}} = t_{n_{p}}, q(x_{1}, ⋯, x_{n_{p}}, y_{1}, …, y_{n_{q}}, …), y_{1} = u_{1}, …, y_{r_{q}} = u_{n_{q}}, … \end{matrix}

that is to say, every distinct predicate takes as argument the same vector x⃗ of variables. Repeated occurrences of a predicate p in one clause need not have their n variables in the same order, so when we eliminate variables and introduce binary relations, we will compose on the left and right with switching relations (see 3.7) as explained below.

Step 2:translating the program

We now convert each predicate symbol p_{i} in the Herbrand base of the program into a coreflexive binary relation (also denoted p_{i}). Although we will be eliminating variables below, we display an intermediate state of the transformation, with all variables present, and using the relations P_{i}^{m} introduced in the previous section, with m = lth(x⃗) and where we have renamed variables so that x⃗ = [x_{1}, …, x_{n}], the y_{j} above are now x_{n+j}, and the terms u_{1}, …, u_{r} are now t_{n+1}, …, t_{n+r}. Also the reverse implication is replaced by equivalence.

x⃗px⃗ ≡ x⃗qx⃗, x⃗K̃([t_{1}, …, t_{m}])x⃗, …

where the K̃ are as in lemma (3.6). Finally, replacing all commas with ∩ and embedded disjunctions with ∪ we have

p = id ∩ q ∩ K̃([t_{1}, …, t_{m}]) ∩ ⋯

We illustrate with two examples.

Example 1

p(x, y) ⟵ q(y, f(b))
⇓
p(x, y, u, v) ≡ q(x, y, u, v), u = y, v = f(b)
⇓
p(x, y, u, v) ≡ q(x, y, u, v), [x, y, u, v] = [x, y, y, f(b)]
⇓
[x, y, u, v]p[x, y, u, v] ≡ [x, y, u, v]q[x, y, u, v],
[x, y, u, v]P_{3}^{4}(P_{2}^{4})^{o}[x, y, u, v], [x, y, u, v](P_{4}^{4})f(b)
⇓
[x, y, u, v]p[x, y, u, v] ≡ [x, y, u, v]q[x, y, u, v] ,
[x, y, u, v]P_{3}^{4}(P_{2}^{4})^{o}[x, y, u, v] , [x, y, u, v](P_{4}^{4})(f_{1}^{1})(b, b)(f_{1}^{1})^{o}(P_{4}^{4})^{o}[x, y, u, v]
⇓
p = id ∩ q ∩ P_{3}^{4}(P_{2}^{4})^{o} ∩ (P_{4}^{4})(f_{1}^{1})(b, b)(f_{1}^{1})^{o}(P_{4}^{4})^{o}

Example 2 We now consider an example with recursion. Initially only the variables x and y occur in the clause being considered. Two new variables u and v are introduced. The variables are ordered in the following sequence (x, y, u, v). The first occurrence of an atom with predicate letter p, namely p(x, y) is expanded to arity 4 by adding the remaining variables in order: p(x, y, u, v). The second occurrence p(u, v) is expanded to include all remaining variables in order: p(u, v, x, y). Since we want to end up with an equation in which all relations involve the same vector of variables we use switching relations to rearrange variables as needed.

p(x, y) ⟵ p(y, f(b))
⇓
p(x, y) ≡ p(u, v), u = y, v = f(b)
⇓
p(x, y, u, v) ≡ p(u, v, x, y), [x, y, u, v] = [x, y, y, f(b)]
⇓
[x, y, u, v]p[x, y, u, v] ≡ [u, v, x, y]p[u, v, x, y],
[x, y, u, v]P_{3}^{4}(P_{2}^{4})^{o}[x, y, u, v], [x, y, u, v](P_{4}^{4})f(b)
⇓
[x, y, u, v]p[x, y, u, v] ≡ [x, y, u, v]B_{1,3}B_{2,4}pB_{2,4}B_{1,3}[x, y, u, v] ,
[x, y, u, v]P_{3}^{4}(P_{2}^{4})^{o}[x, y, u, v] , [x, y, u, v](P_{4}^{4})(f_{1}^{1})(b, b)(f_{1}^{1})^{o}(P_{4}^{4})^{o}[x, y, u, v]
⇓
p = id ∩ B_{1,3}B_{2,4}pB_{2,4}B_{1,3} ∩ P_{3}^{4}(P_{2}^{4})^{o} ∩ (P_{4}^{4})(f_{1}^{1})(b, b)(f_{1}^{1})^{o}(P_{4}^{4})^{o}

The result of applying this procedure to all the clauses of a Horn Clause program is to obtain a set of n equations E_{1}, ⋯, E_{n} in the n predicate letters of the program (now viewed as relation variables). The typical equation E_{i} being of the form

p_{i} = Q_{1} ∪ Q_{2} ∪ ⋯ Q_{l}

where each Q_{j} is of the form Q_{j} = id ∩ p′_{1} ∩ S_{1} ∩ p′_{2} ∩ S_{2} ∩ ⋯ ∩ p′_{n} ∩ S_{n} where each p′_{i} is of the form Bp_{i}B^{o}, with B_{i} a switching relation and where the S_{i} are formative. We write this as

p_{i} = E_{i}(p_{1}, …, p_{n}).  (7)

Step 3: “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. We rewrite the last equation of system 7 above as

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

and substitute into equation n − 1, obtaining

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

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

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

where the right hand side is a closed (no-free-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.1 A positive relation expression R ∈ ℜ_{L} (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.2 Simulating Depth-First Search

Let R_{q} be a relational logic program, (u, u) a singleton query, and A a finitary query. We can simulate depth-first-search for these queries by evaluating (u, u)∩R or A∩R left-to-right. This means expanding expressions of the form fpx.E (x) to E (fpx.E (x)) as they are encountered. This is, of course, equivalent to working with the system of equations (7) and replacing each relation symbol p_{i} from the original Horn-clause program by it’s definition E_{i}(p_{1}, …, p_{n}) as it is encountered. First we distribute the query over unions, and then evaluate each term in the union by associating intersections to the left. Evaluation amounts to computing intersections of formative relation expressions and unfoldings of recursive definitions. If the query is a singleton, by the extensional completeness of formative expressions and lemma (3.5) the query will evaluate to itself, if it is in the success set of the program, and to zero if it is finitely failed. But we can consider more general queries and outputs.

Theorem 4.2 Let P be a Horn clause program. Suppose R_{q} is a relation expression arising from translation of the predicate q defined by P . Let 𝔄 be the set of finitary queries A ∈ ℜ_{L} satisfying:

• D[[A]] = {a⃗ : (a⃗, a⃗) ∈ [[A]]} is a finite subset of the success set {a⃗ : P ⊢_{SLD} q(a⃗)} of P corresponding to the query predicate q

• For each a⃗ ∈ D[[A]] the SLD-tree for the query P ⊢ q(a⃗) is finite.

Then the equational theory 𝔈 is relation-complete with respect to 𝔄,{R_{q}}. That is to say, for any A in 𝔄, A ∩ R_{q} is provably equal to some finitary A′ in 𝔈.

This follows from theorem (3.3). We give a brief sketch. Full details will appear in a forthcoming extended treatment. The proof is by induction on the sequence ⟨ℓ_{1}, …, ℓ_{r}⟩ of depths of the SLD trees for members of [[A]]. The argument establishes a stronger claim, namely that a deterministic rewrite system exists producing the desired A′.

Let q(x_{1}, …, x_{n}) be a predicate defined by program P and R_{q} its translation into a relation expression. The clause

q(t_{1}, …, t_{n}) ⟵ p_{1}, …, p_{n} ∨ ⋯

in P defining q, after translation (without the “Gaussian elimination” step) is of the form

R_{q} = (S_{1} ∩ R_{p_{1}} ∩ S_{2} ∩ R_{p_{2}} ⋯ ∩ R_{p_{n}}) ∪ · · · .

with formative terms S_{i} derived from the K̃(t⃗_{i}) for suitable term vectors t⃗. Left-to-right evaluation “simulating Prolog” yields

A ∩ R_{q} ↦ (A ∩ S_{1}) ∩ R_{p_{1}} ∩ R_{p_{2}} ⋯ ∩ R_{p_{n}} ⋯ ∪ · · · .

Now (A ∩ S_{1}) satisfies the hypothesis of the theorem ( [[A ∩ S_{1} ]] is finite and (A ∩ S_{1}) finitary). Furthermore any member (b⃗, b⃗) ∈ [[A ∩ S_{1} ]] where b⃗ = b_{1}, …, b_{n} is the term resulting from unification of query q(a_{1}, …, a_{n}) for (a⃗, a⃗) ∈ [[A]] with the head of the clause q(t_{1}, …, t_{n}) ⟵ p_{1}, …, p_{n} ∨ · · ·. This unification results in a subgoal ⟵ p′_{1}, …, p′_{n} ∨ ⋯ every ground instance of which has an SLD tree whose depth is one less than the depth associated with the query q(a_{1}, …, a_{n}). By the induction hypothesis we have

(A ∩ S_{1}) ∩ R_{p_{1}} ↦ A_{1}

for some correct finitary A_{1}. Thus we have

A ∩ R_{q} ↦ (A_{1}) ∩ (R_{p_{2}} ⋯ ∩ R_{p_{n}}) ∪ · · · .

Continuing this way through the remaining R_{p_{i}} we obtain a correct finitary expression A′.

Remarks: The preceding theorem can be considerably strengthened with different classes of finitary, (but not necessarily finite) queries, the subject of a future treatment. Observe that the query in the preceding theorem may contain complementation. The reader familiar with constructive negation of Chan et al. [Stuckey], based on the quantifier elimination algorithm described above, will note that the class of queries described in the relation-completeness theorem (4.2) discussed above can be extended to coincide precisely with the sets describable by normal-form constraints of constructive negation.

5 Conclusions

We have mapped out a relational framework which captures a robust extension of Horn-clause programming, computationally as well as semantically. The formalism admits a natural extension to other constraint programming languages either by adding new equations (or rewrite rules) directly, or by representing relation expressions in other relational structures. Since the presence of complementation plays no special role once outside of the framework of constructive negation and the Herbrand universe, it is of interest to consider more general relational theories, such as Freyd’s distributive or division allegories , (which permit variable elimination for intuitionistic logic), as well as power allegories in which higher order relations are expressed via an enriched equational theory[FreySce], which would permit a similar treatment of higher-order logic programming languages [Miller]. Our approach treats all such relational formalisms as executable extensions of the declarative paradigm. Thus, much work in relational program synthesis (e.g. [Backh, Moor92]) can be viewed as an extension to logic programming over the appropriate domain. There is also no need to restrict attention to set-theoretic representations of such theories. The representation theory of allegories and domain-theoretic representations open the way to denotational treatment of logic programming languages. This is perhaps the most important potential application of the relational calculus presented here.

Many computational questions remain to be solved in connection with relational rewriting systems. What are the most natural and efficient deterministic calculi associated with this formalism? What are the right notions of normal form? Are there interesting Church-Rosser systems? Are there strongly normalizing subsystems (corresponding to a class of total logic programs) and what typed calculi can be developed along these lines?

Hopefully some of these questions will be addressed in subsequent papers.

Appendix

The Theories RA and QRA(L)

R ∩ R = R  R ∩ S = S ∩ R  R ∩ (S ∩ T) = (R ∩ S) ∩ T  (8)
R id = R  R^{∘∘} = R  (RS)^{∘} = S^{∘}R^{∘}  (R ∩ S)^{∘} = S^{∘} ∩ R^{∘}  (9)
R(S ∩ T) ⊆ RS ∩ RT  RS ∩ T ⊆ (R ∩ T S^{∘})S  (10)
R ∪ R = R  R ∪ S = S ∪ R  R ∪ (S ∪ T) = (R ∪ S) ∪ T.  (11)
R ∪ (S ∩ R) = R = (R ∪ S) ∩ R  R(S ∪ T) = RS ∪ RT R ∩ (S ∪ T) = (R ∩ S) ∪ (R ∩ T).  (12)
(R ∪ S)^{∘} = R^{∘} ∪ S^{∘}  (S ∪ T)R = SR ∪ T R  (13)
\overline{R} ∩ R = 0  R ∩ 0 = 0 = R0  R ∪ 0 = R  (14)

\overline{\overline{R}} = R  \overline{R ∪ S} = \overline{R} ∩ \overline{S}  \overline{R ∩ S} = \overline{R} ∪ \overline{S}  (15)
\overline{(\overline{A} ∪ B)} ∪ \overline{\overline{A} ∪ \overline{B}} = A  A^{∘}(\overline{AB}) ⊆ \overline{B}  (16)
A^{∘}A ⊆ id  B^{∘}B ⊆ id  A^{∘}B = 1  (17)

Def: Axioms 8-16 define the equational theory RA. QRA is RA together with (17). Let L be a signature. The Theory QRA(L) is the equational theory containing as terms the finitary expressions in ℜ_{L}, and as axioms the theory RA together with a set of axioms

f_{i}^{n}^{∘}f_{i}^{n} ⊆ id (1 ≤ i ≤ n) f_{i}^{n}^{∘}f_{j}^{n} = 1 (i ≠ j) (18)

for each n-ary function symbol f in L. A Relation Algebra 𝔄 = ⟨A, ∪, \overline{( )}, ∘, ( )^{∘}, id⟩ is a model of the RA equations. A Q-relation algebra is a relation algebra with a pair A,B satisfying (17), and A Q-L -relation algebra is a relation algebra with elements a_{1}, …, a_{n} interpreting the terms f_{i}^{n} above, and satisfying axioms 18. A relation algebra is said to be representable in [TarGiv] if it is (∪, \overline{( )}, ∘, ()^{∘}, id)- isomorphic to a family of binary relations on some set with the standard interpretation. In [TarGiv] it is shown that all QRA’s are representable^{5}.

Part of this research was carried out by both authors at the Mathematical Sciences Institute, Cornell University. James Lipton was partly supported by ONR grant 4331-001-srp-01.

References

[Backh] Backhouse, R, et. al., “A Relational Theory of Datatypes,” 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.

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

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

[CurryFeys] Curry, H. B. and R. Feys, Combinatory Logic, North-Holland, Amsterdam, 1958.

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

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

[JafLas] Jaffar, J. and Lassez, J-L., “Constraint logic programming.” in Proceedings of the 14th ACM Symposium on the Principles of Programming Languages, 1987.

[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, Notes, 1988.

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

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

1961, pp.768-771.

5A remark attributed to Maddux in [TarGiv] shows that this fact implies the semantic version of main equipollence result 3.2 [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 Technical Monograph PRG-98, Oxford Computing Lab, Oxford, 1992.

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