Towards a Relational Programming Language

Richard McPhee Worcester College

September 29, 1995

Qualifying dissertation submitted in application for transfer to D.Phil. status.

�

Oxford University Computing Laboratory Programming Research Group

Towards a Relational Programming Language

Richard McPhee

September 29, 1995

Abstract

Until recently, the art of deriving computer programs from specification has been performed equationally in a functional calculus. However, it has become evident that a relational calculus affords us a greater degree of expression and flexibility in both specification and proof since a relational calculus naturally captures the notions of non-determinism along with function converses.

Unfortunately, no language exists in which we can directly execute relational expressions. Moreover, those candidate languages most likely to support an implementation of a relational calculus suffer from an inelegant or complicated evaluation model. This dissertation examines the suitability of these languages for supporting an implementation of relations and proposes a novel computational strategy for a relational language based on the category theory of relations.

Contents

1 Introduction 1

2 A Calculus of Relations 2 2.1 Basic Relational Operators · · · · · · · · · · · · · · · · · · · · · · · · · · 2 2.2 Datatypes and Relational Folds · · · · · · · · · · · · · · · · · · · · · · · 3 2.3 Ruby · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 4 2.4 More Expressive Relational Operators · · · · · · · · · · · · · · · · · · · · 8

3 Functional Programming Languages 10

4 Functional Logic Programming Languages 13 4.1 Combining Functions and Logic · · · · · · · · · · · · · · · · · · · · · · · 13 4.2 Narrowing as a Computational Model · · · · · · · · · · · · · · · · · · · · 15

4.2.1 Basic Narrowing · · · · · · · · · · · · · · · · · · · · · · · · · · · · 17 4.2.2 Constructor based languages · · · · · · · · · · · · · · · · · · · · · 18 4.2.3 Innermost narrowing · · · · · · · · · · · · · · · · · · · · · · · · · 19 4.2.4 Outermost and lazy narrowing · · · · · · · · · · · · · · · · · · · · 19 4.2.5 Rejection and normalisation rules · · · · · · · · · · · · · · · · · · 21

4.3 Programming Relations in ALF · · · · · · · · · · · · · · · · · · · · · · · 23

5 Higher-Order Logic Programming Languages 27 5.1 A Higher-Order Logic · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 27 5.2 The Simply Typed λ-Calculus · · · · · · · · · · · · · · · · · · · · · · · · 28 5.3 Higher-Order Horn Clauses · · · · · · · · · · · · · · · · · · · · · · · · · · 30 5.4 Method of Computation · · · · · · · · · · · · · · · · · · · · · · · · · · · 31

5.4.1 Higher-order unification · · · · · · · · · · · · · · · · · · · · · · · · 31 5.4.2 P-derivations · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 34 5.4.3 Some examples · · · · · · · · · · · · · · · · · · · · · · · · · · · · 35

5.5 Programming Relations in λProlog · · · · · · · · · · · · · · · · · · · · · 38 5.5.1 Implementing Ruby primitives · · · · · · · · · · · · · · · · · · · · 38 5.5.2 Implementing more expressive relational operations · · · · · · · · 45

6 Depth-First Iterative Deepening 47 6.1 Implementing Depth-First Iterative Deepening · · · · · · · · · · · · · · · 47 6.2 Evaluating Depth-First Iterative Deepening · · · · · · · · · · · · · · · · · 49

7 Categorical Relational Programming 51

7.1 Terms and Categorical Combinators · · · · · · · · · · · · · · · · · · · · · 51 7.1.1 Converting terms to polynomial arrows · · · · · · · · · · · · · · · 52 7.1.2 Converting polynomial arrows to terms · · · · · · · · · · · · · · · 53

7.2 Tabulations · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 54 7.3 Unification in Category Theory · · · · · · · · · · · · · · · · · · · · · · · 55

7.3.1 Equalisers · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 55 7.3.2 Pullbacks · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 56

7.3.3 Some example equalisers · · · · · · · · · · · · · · · · · · · · · · · 56 7.4 The Category Theory of Relations · · · · · · · · · · · · · · · · · · · · · · 57

7.4.1 Converse · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 58 7.4.2 Union · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 58 7.4.3 Composition · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 58 7.4.4 Intersection · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 59

8 Conclusions and Further Work 60 8.1 Conclusions · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · · 60 8.2 Program of Further Work · · · · · · · · · · · · · · · · · · · · · · · · · · · 61

1 Introduction

Two distinct motivations exist which suggest the implementation of a relational programming language. Firstly, when deriving functional programs from a mathematical specification, a method of equational reasoning is used in some suitable calculus [Bir87]. However, it is often useful to use a relational calculus rather than a purely functional one since a relational calculus provides a natural treatment of non-determinism and function converses. These combine to form a more expressive calculus than that gained from using functions alone. Furthermore, the flexibility of a relational calculus can help to clarify and simplify the structure of proofs made in the calculus.

The main drawback is that, of all the relational calculi being developed [BdM95, ABH^{+}92, Möl92, JS90, SS88], no language exists which allows us to directly execute the relational expressions being derived. Certainly, a functional programming language is inadequate in several respects. In turn, this prohibits the prototyping of specifications in a relational notation and hinders the understanding of why some relational transformations lead to an efficient program and others do not. A relational language would thus add a new practical dimension to this ongoing development of relational calculi.

The second motivation arises from the field of declarative programming. Logic and functional programming languages are the two leading paradigms in the methodology of declarative programming. These two methods used to compete for universal acceptance within the field but, increasingly, there is a realisation that each paradigm is appropriate for tackling different problems. A natural progression then is to discover if a new programming paradigm can be obtained which combines the benefits of both functional and logic languages. The resulting functional logic languages to date look quite expressive, combining elements of higher-order programming with a natural treatment of non-determinism.

However, the main criticism of functional logic languages is that they lack an elegant computational model comparable to that of a purely functional programming language. As a result, this complicates reasoning about the behaviour of functional logic programs. The elegance of purely functional languages arises from the fact that their programs can be written using a small set of combinators, eliminating the need for variables. Indeed, it is possible to describe logic programs in this manner as shown by Asperti and Martini [AM89] and, more recently, by Broome and Lipton [LB94, BL95]. It may be possible, therefore, to extend this technique to encompass functional logic languages. However, a large divide exists between the theory of computation in functional logic languages and their actual implementations. Our desire is to bridge this gap and develop a more elegant computation model for a declarative, relational programming language.

The remainder of the report is organised into seven sections. In Section 2, we review the fundamental operations in the relational calculus [BdM95] and also discuss the Ruby [Jon90] relational language. The next three sections examine the suitability of various programming paradigms for the implementation of a relational calculus. Those paradigms considered are functional, functional logic, and higher-order logic programming. In Section 6, we describe a search procedure designed to overcome the problems of the standard search strategy employed in logic programming languages. In Section 7, we introduce a novel computational model for a relational programming language based on the category theory of relations. We conclude with Section 8 and suggest further work.

2 A Calculus of Relations

Programming problems can be tackled by specifying a program’s behaviour in an abstract mathematical specification and then, through the application of some well defined calculus, converting this into an efficient and implementable program. Until recently, the art of deriving computer programs from specification has been performed equationally in a functional calculus [Bir87]. However, it has become evident that a relational calculus affords us a greater degree of expression and flexibility in both specification and proof since a relational calculus naturally captures the notions of non-determinism along with function converses.

Bird and de Moor [BdM95] have developed one such relational calculus for calculating programs. In this section, the main ideas of their relational calculus are discussed and some examples are presented to illuminate the benefits of using such a calculus.

2.1 Basic Relational Operators

Let us incrementally introduce the relational operations underpinning the calculus as simple predicates.

A binary relation R : A → B, of type A to B, is a subset of the cartesian product A×B of sets A and B. We write a R b to denote that the pair (a, b) ∈ R and we define the domain and range of R by

dom R ≡ {a | ∃b.a R b},
ran R ≡ {b | ∃a.a R b},

respectively. The relation id : A → A relates elements to themselves, i.e., for all a ∈ A, (a, a) ∈ id. The composition of two relations R : A → B and S : B → C is written as R ; S : A → C and given explicitly by

a (R ; S) c ≡ ∃b.a R b ∧ b S c.

Every relation R : A → B has a well defined converse R^{∘} : B → A defined straightforwardly as

b R^{∘} a ≡ a R b.

Converse is contravariant, i.e., reverses composition, in that (R ; S)^{∘} = S^{∘}; R^{∘} and is also an involution since (R^{∘})^{∘} = R.

The intersection of two relations R, S : A → B is written as R ∩ S : A → B and union as R ∪ S : A → B. These operations are denoted respectively by

a (R ∩ S) b ≡ a R b ∧ a S b,
a (R ∪ S) b ≡ a R b ∨ a S b.

In the next section, we build on these basic elements of the relational calculus and introduce relational folds which afford us generous powers of expression.

2.2 Datatypes and Relational Folds

By employing a categorical basis for their relational language, Bird and de Moor [BdM95] achieve an abstraction over datatypes allowing a method of uniformly operating on different types. Particularly, for each datatype there exists the fold operation. “Folding” over a datatype is a form of structural recursion—effectively replacing each constructor of the datatype with a new constant, function, or relation—facilitating conversion between types. Folding affords us substantial powers of expression, aesthetically packaged in an elegant and simple operation. Although non-specific to the list data type, folds over cons-lists are akin to the foldr function from functional programming.

To begin with, let us construct some machinery enabling us to introduce some interesting examples involving relational folds. Firstly, we define datatypes in the same manner as in functional programming, i.e., by simple enumeration of their elements. For example, the datatype Nat of natural numbers may be defined as

Nat ::= zero | succ Nat.

Another datatype, used centrally in this discussion, is the cons-list defined as

list A ::= nil | cons (A, list A).

We will add a spoonful of syntactic sugar when writing lists: cons will be represented as the infix symbol ‘:’, nil by [ ], and we will take the liberty of representing the lists a : [ ] by [a], a : b : [ ] by [a, b], and so forth. We deal purely with binary relations taking only one argument, hence we also require the appropriate projection functions outl : A×B → A and outr : A × B → B to access the first and second components of a pair, respectively.

We are now in a position to give the definition of a relational fold over cons-lists, fold : B × (A × B → B) → list A → B, as

fold (c, R) [ ] = c
fold (c, R) (x : xs) = R (x, fold (c, R) xs).

As a simple example of folding, we can sum the elements of a list using the function sum : list Nat → Nat defined as

sum = fold (zero, plus),

where plus : Nat × Nat → Nat adds two natural numbers. We can imagine traversing the list, replacing all occurrences of cons with plus and nil with zero.

It is often useful to consider the version of folding which operates on strictly non-empty lists, called fold1 : (A × A → A) → list^{+} A → A. By doing so, we avoid carrying the baggage of an explicit expression for when the empty list is encountered. To illustrate the usefulness of fold1 , consider the relation

element = fold1 (outl ∪ outr).

The union operator ∪ is essentially non-deterministic thus, in the case above, either outl or outr can be applied at each step in the fold. Therefore, the result of the expression element [1, 2, 3] is any member of the set {1, 2, 3}.

We can represent certain combinatorial functions—useful in equational reasoning—by relational folds. For instance, the subsequence function sub : list A → list A, which returns a subsequence of a given list, can be defined by the relation

sub = fold ([ ], cons ∪ outr).

The solution to sub [1, 2] is one of {[ ], [1], [2], [1, 2]}.

The relational calculus can often facilitate a more compact and intuitive description of a function than in a functional setting. The function interleave : listA×listA → list(listA) finds all ways of interleaving two lists such that, for example, interleave ([e], [a, r]) returns the set {[e, a, r], [a, e, r], [a, r, e]} of possible solutions. The implementation of interleave in a functional language is somewhat complicated:

interleave (xs, [ ]) = [xs]
interleave ([ ], ys) = [ys]
interleave (x : xs, y : ys) = (map (x :) (interleave (xs, y : ys))) ++

(map (y :) (interleave (x : xs, ys)).

It is more elegant to define interleave as the converse of another relation, called tease : list A → list A × list A, given by

tease = fold (([ ], [ ]), apl ∪ apr)

where apl, apr : A × (list A × list A) → list A × list A are defined as

apl (a, (xs, ys)) = (a : xs, ys)
apr (a, (xs, ys)) = (xs, a : ys).

We can then simply define interleave = tease^{∘}.

The above discussion clearly illustrates how simply we can define specifications in the relational calculus. Next, we look at the Ruby relational language which demonstrates the practical application of the operations introduced in this and the previous sections.

2.3 Ruby

Ruby is a relational language developed by Jones and Sheeran [Jon90, JS90] for describing hardware circuits. The behaviour of a circuit is specified by a relational program which can then be transformed into an equivalent program amenable to implementation in hardware. A circuit in Ruby is represented as a binary relation between simple data values.

The data values on which these circuits operate consist solely of integers, and both tuples and lists of integers. A tuple is represented in Ruby by the notation (a, b) whose type is (A × B) for any types A and B, and a list is represented by [a_{0}, a_{1}, …, a_{n}] for each element a_{i} having type A and the type of the list is list A. The empty list is denoted by ‘[ ]’. It is worth mentioning that tuples are considered distinct from lists, i.e., a tuple and a list of length two are treated differently. Other descriptions of Ruby [JS91a, Jon90] tend to blur the distinction between tuples and lists, allowing them to be dealt with interchangeably. As a consequence, however, automatic type deduction becomes greatly complicated, so hampering the implementation of Ruby in a strongly typed language.

A relation in Ruby can be given pictorially, corresponding directly to its interpretation as a circuit. For example, the circuit associated with the relation R : A → B can be represented as the single node

R  .

The convention regarding data flow in such a circuit is that domain values “enter” at the left and top sides of the node and range values “exit” at the bottom and right sides. In addition, multiple wires to and from a node are read from bottom to top. Therefore, a relation (a, b)S (c, d) : (A×B) → (C ×D)—taking tuples to tuples—may be represented by the circuit

S a  bc  d .

Ruby expressions are composed hierarchically from primitive relations and higherorder functions. The most fundamental of these are sequential composition, parallel composition, and converse. The sequential composition of two relations R : A → B and S : B → C , written as R ; S : A → C , is given by

R : A → B, S : B → C ⇒ R ; S : A → C ,
a (R ; S) c ≡ ∃b.a R b ∧ b S c.

The first line in this expression denotes the type information of the function in a similar style to that adopted by Jones and Sheeran [JS91b]. The sequential composition of two circuits look like this:

R  S  .

The parallel composition of two relations R and S, written as [R, S], is expressed by

R : A → B, S : C → D ⇒ [R, S] : (A × C ) → (B × D),
(a, c) [R, S] (b, d) ≡ a R b ∧ c S d.

The parallel composition of two circuits simply places them over one another in the following way:

S R  .

Every relation R has a well-defined converse R^{∘}, given straightforwardly by

R : A → B ⇒ R^{∘} : B → A,
b R^{∘} a ≡ a R b.

Several primitive relations are used to construct and deconstruct the data values of a circuit. For tuples, we have the relations

a id b ≡ a = b,
(a, b) swap (c, d) ≡ a = d ∧ b = c,
(a, b) outl c ≡ a = c,
(a, b) outr c ≡ b = c,
a fork (b, c) ≡ a = b ∧ a = c,
((a, b), c) lsh (d, (e, f )) ≡ a = d ∧ b = e ∧ c = f ,
(a, (b, c)) rsh ((d, e), f ) ≡ a = d ∧ b = e ∧ c = f .

Of these relations, only id, outl, and outr are essentially primitive in the presence of relational intersection. The intersection of two relations R and S, written as R ∩ S, is defined by

R : A → B, S : A → B ⇒ R ∩ S : A → B,
a (R ∩ S) b ≡ a R b ∧ a S b.

The primitive Ruby relations for lists are

(as, bs) app cs ≡ as ++ bs = cs,
(a, as) apl bs ≡ [a] ++ as = bs,
(as, a) apr bs ≡ as ++ [a] = bs,
a wrap bs ≡ [a] = bs,
a null bs ≡ bs = [ ],

where ‘++’ denotes list concatenation. These primitive relations provide us with the bare bones of the Ruby language. The real expressive power is obtained by building higher-order functions—taking relations to relations—from these combining forms. Two commonly used higher-order functions are simple shorthands, given by

fst R ≡ [R, id],
snd R ≡ [id, R].

Since Ruby is a language for designing circuits, a plethora of functions exist for combining circuit elements. For two circuits, denoted respectively by the relations R and S, the function ‘↔’ (pronounced ‘beside’) joins R and S together in the following fashion:

\begin{matrix}R : (A × B) → (C × D) \\ S : (D × E) → (F × G) \end{matrix} \} ⇒ R ↔ S : (A × (B × E)) → ((C × F ) × G),
R ↔ S ≡ rsh ; fst R ; lsh ; snd S ; rsh.

R a  bc  S ef  g

(a, (b, e)) R ↔ S ((c, f ), g)

S e  f  h

R a  c  d

((a, e), f ) R ↕ S (c, (d, h))

Figure 1: The circuits corresponding to beside and below.

The beauty of Ruby is exemplified when we define the dual of existing functions in terms of themselves, providing a convenient way to produce new circuits. We can obtain the dual of any higher-order function by first taking the converse of all its arguments and then taking the converse of the entire expression. For example, we can manufacture the function ‘↕’ (pronounced ‘below’) in terms of its dual function beside by

\begin{matrix}R : (A × B) → (C × D) \\ S : (E × F ) → (B × H ) \end{matrix} \} ⇒ R ↕ S : ((A × E) × F ) → (C × (D × H )),
R ↕ S ≡ (R^{∘} ↔ S^{∘})^{∘}.

Both beside and below, interpreted as circuits, are shown in Figure 1.

Using beside, we can create a new function row which forms a linear array, cascading the circuit R a number of times, defined by

R : (A × B) → (C × A) ⇒ row R : (A × list B) → (list C × A),
row R ≡ snd wrap^{∘} ; R ; fst wrap

∨ snd apl^{∘} ; (R ↔ row R) ; fst apl.

Notice that row is defined as a disjunction; the first clause deals with the case where the second component of the domain tuple is the singleton list since row takes non-empty lists. The function col, forming a vertical column of circuits, is defined in terms of its dual function row via

R : (A × B) → (B × C ) ⇒ col R : (list A × B) → (B × list C ),
col R ≡ (row R^{∘})^{∘}.

The circuits represented by both row and col are shown in Figure 2.

The map function represents repeated parallel composition of the relation R and is defined by

R : A → B ⇒ map R : list A → list B,
map R ≡ null^{∘} ; null
∨ apl^{∘} ; [R, map R] ; apl.

R  R  R  R  R R R R

Figure 2: Possible circuits corresponding respectively to row R and col R.

Finally, the two functions rdl and rdr relate tuples of values to single values and correspond to the circuit equivalent of “reducing” (or “folding”) in functional programming. They are defined as

R : (A × B) → A ⇒ rdl R : (A × list B) → A,
rdl R ≡ row (R ; outr^{∘}) ; outr,

and

S : (A × B) → B ⇒ rdr S : (list A × B) → B,
rdr S ≡ col (S ; outl^{∘}) ; outl,

respectively. The circuits corresponding to these functions are illustrated in Figure 3.

The above discussion highlights the expressive power and elegance we can achieve from a relational calculus; expressions are built hierarchically from a small set of primitive forms. In the following section, we look at several additional relational operators which bolster our powers of expression.

2.4 More Expressive Relational Operators

Perhaps the most frequently encountered representation of a relation R : A → B is to view R as a subset of the catesian product A × B. However, choosing a representation of relations is somewhat arbitrary since we could equally opt to represent them as booleanvalued functions of two arguments or as set-valued functions. In the latter representation, a relation is simply a function which takes a single domain value as its argument and returns a set of all related range values. It transpires that we can move easily between a relation R : A → B and its corresponding set valued function ΛR : A → PB. The set PB is called the powerset of B and we define

(ΛR) a ≡ {b | a R b}.

R  R  R  R  R R R R

Figure 3: An illustration of rdl R and rdr R.

The relation ∈ : PA → A, called the membership relation, relates a set to any one of its members. The above two relations together form the identity

ΛR ; ∈ = R,

allowing us to exploit the isomorphism between a relation and its associated set-valued function. In particular, the function Λ provides us with a method of collecting all the solutions to a relational expression. For example, we could extend the sub function of Section 2.2 to determine all subsequences by defining subs = Λsub. Likewise, we could extend the definition of interleave = Λtease^{∘}. This useful technique adds more power for expressing and manipulating program specifications.

We can complete the set-valued function interpretation of relations by providing the power operation, also denoted by P, which embodies the “map” operator for sets:

(Pf ) xs ≡ {f a | a ∈ xs}.

The division operator R\S : C → A (pronounced “R under S”) of two relations R : A → B and S : C → B, defined by

a (R\S) c = ∀b.a R b ⇒ c S b,

provides the power to express specifications employing universal quantification and so extends the relational calculus to encompass full first-order logic.

In the remainder of the report, we examine different programming paradigms to determine their potential for supporting an implementation of relations.

3 Functional Programming Languages

One essential difference between functions and relations is that a relation may relate a domain value to several range values whereas a function, by definition, maps each domain value to precisely one range value. This fact suggests that functional languages exhibit intrinsic mathematical limitations for the task of implementing a relational calculus. However, relations can be modelled mathematically in several different ways. The set-valued function representation is particularly appealing since it provides an ostensibly natural way to emulate relations in a functional programming language: by considering sets as lists, we can model a relation in a functional language as a list-valued function. Hence, a relation is simply a function taking a single domain value as its argument and returning a list of all related range values. In the remainder of this section, we demonstrate how to implement relations in the functional language Gofer and highlight the limitations of such an implementation.

Let us begin by introducing the notion of a relation as a list-valued function. Consider the function setify : list A → PA which converts a list into a set. A relation R : A → B is represented in a functional language by the list-valued function r : A → list B such that

setify · r = ΛR,

where the function ΛR : A → PB is the set-valued representation of R, as discussed in Section 2. The standard list manipulation functions of Gofer have analogies in set theory: the function wrap : A → list A, which converts an object into a singleton, corresponds to the set-valued function τ : A → PA; the function concat : list (list A) → list A, which concatenates a list of lists into a single list, corresponds to union : P(PA) → PA. Certain identities hold between these list- and set-valued functions indicating the relationship between the two representations. We have that

setify · wrap = τ
setify · concat = union · setify · map setify.

These identities will prove useful when considering the relational operations below. By representing sets as lists, we can imagine that the function setify might simply remove duplicate elements from a list, i.e., setify = nub.

Using the above theory of relations, we obtain a straightforward interpretation for some relational operations but others, unfortunately, become quite complicated. For example, the composition ΛR ∘ ΛS : A → PC of two set-valued functions, ΛR : A → PB and ΛS : B → PC , is given by

ΛR ∘ ΛS = union · P(ΛS) · ΛR.

The translation of this result to a list-valued representation is simple: the composition r ‘comma‘ s : A → list C of two relations r : A → list B and s : B → list C is

(r ‘comma‘ s) a = concat (map s (r a)).

The union r ‘cup‘ s : A → list B of two relations r, s : A → list B can be stated quite succinctly as the concatenation of r and s:

(r ‘cup‘ s) a = r a ++ s a.

The intersection r ‘cap‘ s : A → list B of two relations r, s : A → list B is somewhat more complicated than union since we wish to retain only those range elements common to both r and s.

(r ‘cap‘ s) a = filter (λx.x ‘elem‘ (s a)) (r a).

Implementing relations as list-valued functions does, however, present several substantial problems. For instance, calculating the converse of a relation is a nontrivial operation. To illustrate this point, consider the function outl : A × B → A. The converse of this function outl^{∘} : A → A × B is highly non-deterministic since the second component of the resulting pair may be any value in B. The set-valued function Λoutl^{∘} is infinite if B is infinite which, in turn, results in the list-valued representation of outl^{∘} being infinite. Generally, introducing relations which return infinite lists proves to be problematic since the obvious definitions of standard relational operations, presented above, would result in non-terminating computations. The relation interleave, introduced in Section 2.2, cannot be implemented in this representation of relations since it is described as the converse of a relational fold.

We can partly rectify this situation by creating a new function twiddle which effectively joins infinite lists by exploiting lazy evaluation:

twiddle : list A → list A → list A
twiddle [ ] ys = ys
twiddle (x : xs) ys = x : (twiddle ys xs).

By twiddling the lists in the definition of cup rather than concatenating them, we can capture the union of relations which return infinite lists. Furthermore, we can rewrite concat in terms of twiddle rather then ‘++’ to extend the function comma to handle infinite lists. However, we cannot make any progress with the function cap since we are still obliged to search the entire length of an infinite list.

Despite these limitations, list-valued functions can be usefully applied in several cases, particularly where converse and infinite lists are not involved. One such example is finding the reflexive, transitive closure of a relation, represented by the function

close : (A → list A) → A → list A
close r = wrap ‘cup‘ (r ‘comma‘ (close r)).

We can implement the relational fold operation in an obvious manner:

fold : (A × (B × A → list A)) → list B → list A
fold (c, r) [ ] = wrap c
fold (c, r) (x : xs) = concat [r (x, y) | y ← fold (c, r) xs],

A functional relation simply returns a singleton list as its result. Several useful relations of this form are

succ = wrap · (1+)
outl = wrap · fst
outr = wrap · snd
cons = wrap · uncurry (:),

and are self explanatory. Using the above functions, we can express several relational expressions as a simple fold. For example, the length of a list can be calculated via the function

length = fold (0, outr ‘comma‘ succ).

The function subs translates from the relational definition given in Section 2.2 to

subs = fold ([ ], cons ‘cup‘ outr).

The main drawback of implementing relations as list-valued functions is that computing the converse of a relation and dealing with relations which return infinite lists cause difficulties.

4 Functional Logic Programming Languages

Functional logic languages attempt to integrate the declarative programming paradigms of functional and logic languages. Bellia and Levi [BL86] describe several benefits of doing so, some of which appear to meet the language requirements for implementing the relational calculus. Firstly, a notational extension is obtained which allows us to define both predicates and functions. Moreover, we are able to freely compose these providing us with the expressional power we seek. Additionally, some functional logic languages promise features such as higher-order functions, lazy evaluation, and polymorphic type systems, all of which ease an implementation of relations.

The expressional benefits of functional logic languages arise from their support of features like function inversion, logic variables, and partial data structures. In this section, we illustrate these novel features and describe the computational model employed in functional logic languages. An elementary knowledge of first-order logic programming [Llo87] is assumed in the discussion.

4.1 Combining Functions and Logic

Functional logic languages allow us to define both functions and predicates in our programs. Moreover, we can combine them to form conditional equations. Before giving an example of doing so, let us recall the definition of first-order Horn clause logic:

D ::= A | A ← G | ∀x.D
G ::= A | G ∧ G.

The formulas constructed from D are called definite clauses and those from G are called goal clauses. In more familiar programming language formalisms, a set of closed definite clauses comprises a program and a goal formula on its own a query. The formulas represented by A are atomic formulas of the form p t_{1} … t_{n} where p is a predicate symbol and t_{1} … t_{n} are themselves terms. A term is either a variable—denoted by a capital letter, like X —or a compound term of the form f s_{1} … s_{m} where f is a function symbol^{1} and s_{1} … s_{m} are terms. Notice that we adopt a curried notation for atomic formulas. The symbols used above are ‘∧’ for conjunction, ‘←’ for implication, and ‘∀’ for universal quantification. Furthermore, we call a term positive if it does not contain any instances of implication ‘←’ or universal quantification ‘∀’.

We can appeal to a richer formulation of Horn clause logic and let this form the basis of predicates in our language:

D ::= A | A ← G | ∀x.D
G ::= A | G ∨ G | G ∧ G | ∃x.G.

In the above definition, the new symbols used are ‘∨’ for disjunction and ‘∃’ for existential quantification.

1A function, in this sense, simply means a constructor (or irreducible) function.

In this language, we can write a predicate

∀YS.append [ ] YS YS.

∀X , XS, YS, ZS.append (X : XS) YS (X : ZS) ← append XS YS ZS.,

which appends two lists together. We can then write a query

?− ∃XS, YS.append XS YS (1 : 2 : [ ]).,

which determines lists XS and YS such that, when appended together, they produce the list (1 : 2 : [ ]). From now on, we shall assume that all variables are implicitly quantified in clauses for brevity.

In order to define functions in a logic setting, we must be able to introduce equations in our language. In logic languages, ‘=’ normally represents syntactic equality. That is, a clause of the form X = Y is satisfied only in the case where X has the same form as Y . For example, the clause 2 = 1 + 1 is not satisfied since the number 2 is not of the same form as 1 + 1. However, we can interpret ‘=’ differently such that it represents semantic equality and thus allows us to regard syntactically different expressions as equal. We can then express the above append predicate as the function

append [ ] YS = YS.
append (X : XS) YS = X : (append XS YS).

Functions and predicates are subtly different, though; a function actually returns its final computation as a result whereas a predicate only “returns” a boolean value along with the values of any logical variables discovered during the course of the computation.

Functional logic languages also allow for the definition of conditional equations using predicates. For example, we may define the function

max X Y = X ← X ≥ Y .
max X Y = Y ← X < Y .,

taking two numbers as arguments and returning the greater of them. (It may be helpful to remember from logic programming that ‘←’ may be read as meaning ‘if’.) Equations themselves can constitute a condition since they too form boolean valued expressions. This, in turn, may require an evaluation of the equational condition to determine the value of any unknown logical variables it may contain. This subtle point is illustrated by the function

last XS = X ← append Y (X : [ ]) = XS.,

which returns the last element of a list. We can see that we must compute the values of the two logic variables X and Y before we can solve the entire condition.

Let us define a list membership predicate by

member X (X : ).

member X ( : XS) ← member X XS.

We can highlight another difference between functional logic languages and pure logic ones since function applications can be present in functional logic goal queries. To clarify this point, consider the query

?− member X (append (3 : [ ]) (4 : [ ])).

Just as in functional languages, we expect the subexpression append (3 : [ ]) (4 : [ ]) to be actually evaluated to (3 : 4 : [ ]) at some stage in the computation. This kind of “nested” evaluation does not occur in pure logic programming languages.

Other difficulties with introducing functions into logic programming arise when we incorporate logical variables into functional expressions. For example, in the query

?− append XS (3 : 4 : [ ]) = 1 : 2 : 3 : 4 : [ ].,

we must solve for the logic variable XS with respect to the equational rules which define append. In order to satisfy such an expression, we need to employ the computation model of narrowing, described next.

4.2 Narrowing as a Computational Model

In this section, the computational method of narrowing is described. Narrowing is basically a combination of rewriting—as found in functional programming languages—and unification—as found in logic programming languages. In the following discussion, we follow closely the notation adopted by Reddy [Red87].

Let us develop an understanding of narrowing via an extended example. Consider, again, the function

append [ ] YS = YS.  (1)
append (X : XS) YS = X : (append XS YS).,  (2)

for appending lists. In a functional language, an expression is evaluated only on ground terms, i.e., if it contains no free variables. When a function is called in a functional programming language, the actual arguments are matched with the formal parameters of the function. Since each expression in a functional language is guaranteed to be ground, this matching need only be “one way”; the formal parameters of the function are explicitly pattern matched with the actual arguments of the call. However, in a functional logic language, unbound (or logical) variables may appear in a function call. To cope with this situation, the arguments of the function call are instead unified with its formal parameters. Unifying two terms results in a set of substitutions for the variables of the terms so that the the terms become identical after applying the substitutions to each one. Therefore, we obtain substitutions for any logical variables contained in the arguments of the function call in addition to those for the formal parameters. A substitution for a variable V by an expression e is denoted by ⟨V , e⟩ where V may be either a logic variable or a formal parameter.

To illustrate this point, consider the expression append A (2 : [ ]). If we unify this expression with the definition of function append, we obtain two alternative substitutions corresponding to the two equations (1) and (2) which define append. Explicitly, these substitutions are given by the sets 1. {⟨A, [ ]⟩, ⟨YS, 2 : [ ]⟩},

2. {⟨A, X : XS⟩, ⟨YS, 2 : [ ]⟩}.

In a narrowing step, we unify a goal (or a subterm of a compound goal) with the left hand side of an appropriate program equation to produce a set of unifiers. Notice that the unifiers fall naturally into two categories: firstly, we obtain an argument substitution σ binding any logic variables contained in the arguments; secondly, we have a formal parameter substitution θ binding the formal parameters of the function with the ground arguments of the call. With these two substitutions, we can describe a narrowing step using the notation

e ⟹ σ ⟶ e′.

This means that expression e narrows to expression e′ via the argument substitution σ. The argument substitution σ gives the condition under which the expression e is reducible. Expression e′ is obtained by applying the formal parameter substitutions in θ to the right hand side of the relevant program equation of expression e.

For example, the possible narrowing steps for append A (2 : [ ]) are

1. append A (2 : [ ]) ⟹ {⟨A, [ ]⟩} ⟶ 2 : [ ],

2. append A (2 : [ ]) ⟹ {⟨A, X : XS⟩} ⟶ X : (append XS (2 : [ ])),

obtained from narrowing against the equations which define the append function. Clearly then, narrowing is a nondeterministic procedure since, at each narrowing step, every applicable program equation must be considered simultaneously. We shall say more about this later in the section.

We may now examine the more interesting example of evaluating an expression using narrowing. Consider the boolean valued expression

append A (2 : [ ]) = 1 : 2 : [ ].  (3)

In order to solve this equation, we need to ascertain the value of the variable A thus providing the boolean value of the entire equation. Two possible narrowing sequences for equation (3) are shown below. In the following description, a rigorous definition of narrowing is avoided in favour of developing a more intuitive understanding of computing a narrowing sequence. As a consequence, a few technical points are neglected. However, let us briefly mention that “propagating substitutions” means that we can distribute a set of substitutions φ through an expression E simply by applying φ to E. This property conveniently allows us to drop parentheses in certain expressions. Reddy [Red87] provides a precise formalisation of narrowing and the interested reader is referred to this for a complete description. Continuing with the example, one sequence is given by

append A (2 : [ ]) = 1 : 2 : [ ]

⟹ {narrowing of append via equation (1)}

({⟨A, [ ]⟩} ⟶ 2 : [ ]) = 1 : 2 : [ ]

⟹ {propagation of σ}

{⟨A, [ ]⟩} ⟶ 2 : [ ] = 1 : 2 : [ ].

This derivation sequence results in failure since we cannot unify the terms (2 : [ ]) and (1 : 2 : [ ]). A second possible narrowing derivation is

append A (2 : [ ]) = 1 : 2 : [ ]

⟹ {narrowing of append via equation (2)}

({⟨A, X : XS⟩} ⟶ X : append XS (2 : [ ])) = 1 : 2 : [ ]

⟹ {propagation of σ}

{⟨A, X : XS⟩} ⟶ X : append XS (2 : [ ]) = 1 : 2 : [ ]

⟹ {narrowing of append via equation (1)}

{⟨A, X : XS⟩} ⟶ X : ({⟨XS, [ ]⟩} ⟶ 2 : [ ]) = 1 : 2 : [ ]

⟹ {propagation of σ′}

{⟨A, X : [ ]⟩} ⟶ X : 2 : [ ] = 1 : 2 : [ ]

⟹ {unification}

{⟨A, 1 : [ ]⟩} ⟶ true.

Therefore, the result of this narrowing derivation is the boolean value true provided A is bound to the value (1 : [ ]). The value true is generated by the successful unification of the two final terms.

In summary, narrowing allows us to find solutions for the logic variables contained in a functional expression. In its most general form, narrowing is a sound and complete method for solving goal queries with respect to some canonical—both confluent and terminating—set of equations, more commonly called a program. By sound we mean that each substitution computed by narrowing is a unifier with respect to the program and by complete we mean that, for each such unifier, a most general unifier exists and is found.

The main problem with narrowing is that every applicable program equation must be considered simultaneously when narrowing an expression. As a direct result of this, an enormous search space can be generated which may also include many infinite paths. For purely efficiency reasons, narrowing must be restricted in some way before applying it as a realisable computation model for a programming language. By doing so, narrowing unfortunately becomes an obscure and inelegant computational basis for a language. Hanus [Han94] provides a thorough treatment of the different methods of restricting the general case of narrowing and we summarise the most important of these below.

4.2.1 Basic Narrowing

The most elementary way to restrict general narrowing is through the method of basic narrowing. In essence, this means that a narrowing step is only performed at a subterm of the original goal expression rather than at one introduced by a successive narrowing step. To illustrate this concept, consider the (somewhat silly) function

reverse (reverse YS) = YS.,

which represents a rule for reversing a given list. The general narrowing sequence for the boolean valued expression reverse XS = XS, with respect to the previous equation, is given by

reverse XS = XS

⟹ {narrowing of reverse}

({⟨XS, reverse YS′⟩} ⟶ YS′) = XS

⟹ {propagation of σ}

{⟨XS, reverse YS′⟩} ⟶ YS′ = reverse YS′

⟹ {narrowing of reverse}

{⟨XS, reverse YS′⟩} ⟶ YS′ = ({⟨YS′, reverse YS′′⟩} ⟶ YS′′)

⟹ {propagation of σ′}

{⟨XS, reverse (reverse YS′′)⟩} ⟶ reverse YS′′ = YS′′

⋮

and so on. Clearly this evaluation produces an infinite narrowing sequence. Under a basic narrowing strategy, however, we would be unable to perform the second narrowing step above since the expression reverse YS′ was introduced at a previous step. Basic narrowing would thus terminate the computation at this stage to leave the expression YS′ = reverse YS′ as the final solution. Since the two sides of this equation do not unify, the computation fails with respect to our definition of reverse. Therefore, basic narrowing is useful since it can trim some infinite search paths from a search space in a narrowing derivation.

4.2.2 Constructor based languages

One unsatisfactory aspect of basic narrowing is that it fails to address the nondeterministic behaviour of general narrowing; we must still apply each relevant program equation at each basic narrowing location. Yet one of the most elegant features of purely functional languages is the deterministic manner in which functions are reduced to a final value. In order to model the various reduction strategies of their functional counterparts, functional logic languages may be restricted to being constructor based. This means that the left hand side of a program equation comprises solely of the name of the function being defined along with constructor (or irreducible) functions and atomic values as formal parameters. Of course, most modern functional languages, like Haskell for instance, are constructor based and so this constraint is not too much of a sacrifice.

By restricting functional logic languages to being constructor based, we exclude equational definitions like the function reverse, given earlier. Moreover, we can employ deterministic evaluation strategies, emulating innermost and outermost reduction, to help improve the operational behaviour of functional logic languages. These strategies are discussed next, in turn.

4.2.3 Innermost narrowing

Innermost narrowing is analogous to innermost reduction in that the innermost subterm of a goal is narrowed first. Unfortunately, innermost narrowing on its own is incomplete since it may provide unifiers which are too specific. For example, consider the functions

foo X = c.
bar c = c.,

where c is a constructor. Notice that foo is the constant function which maps all arguments to the constructor c. Therefore, the most general unifier for the function foo is the identity (or empty) substitution ∅. Innermost narrowing, though, computes a unifier which is too specific:

foo (bar X ) = c

⟹ {innermost narrowing of bar}

{⟨X , c⟩} ⟶ foo c = c

⟹ {innermost narrowing of foo}

{⟨X , c⟩} ⟶ (∅ ⟶ c = c)

⟹ {propagation of σ}

{⟨X , c⟩} ⟶ c = c

⟹ {unification}

{⟨X , c⟩} ⟶ true.

The value true is returned provided X is bound to c which is too specific in this instance. The problem arises from the fact that the function bar is partial. To restore completeness and still retain the deterministic selection of the next narrowing position, we can combine basic and innermost narrowing. The reasons for regaining completeness are non-obvious and we refrain from an explanation here. The interested reader is referred instead to Hanus [Han94].

4.2.4 Outermost and lazy narrowing

Outermost narrowing is motivated by lazy functional programming whereby the next narrowing position chosen is an outermost one. A lazy strategy delays the evaluation of arguments in a function call until their values are essential for determining the result of the call. As a consequence of lazy evaluation, a language is able to support infinite data structures.

Earlier, we noted that a functional logic program must be canonical—both confluent and terminating—in order to ensure completeness. However, by allowing infinite data structures we immediately lose the termination requirement for rewriting during a narrowing step. Thus, outermost narrowing strategies are insufficient on their own to be used as a computational model and we must adopt lazy narrowing, which does not require termination of a program, to rectify this situation. Essentially, lazy narrowing differs from outermost narrowing by allowing narrowing steps to be performed at inner positions of a term if the value at such a location is required to facilitate narrowing at an outer position. To illustrate this point, consider the definition of natural numbers:

0 + N = N .  (4)
(succ M ) + N = succ (M + N ).,  (5)

(we assume that succ binds more tightly than ‘+’), along with the following program:

foo 0 0 = 0.  (6)
foo (succ M ) 0 = succ 0.  (7)
foo M (succ N ) = succ succ 0.  (8)

An outermost reduction strategy for the expression foo (foo X Y ) Z = 0 must apply the third equation since we do not want to evaluate the subexpression (foo X Y ). This results in the narrowing derivation

foo (foo X Y ) Z = 0

⟹ {outermost narrowing of foo via equation (8)}

{⟨Z , succ N ⟩} ⟶ succ succ 0 = 0

⟹ {unification}

{⟨Z , succ N ⟩} ⟶ false.

The trouble in the previous example arises from the fact that we can only apply the first defining equation of foo—resulting in a sensible solution—if the subterm foo X Y gets evaluated to 0. Thus, we allow an inner term to be evaluated if (and only if) its value is demanded and contributes to the evaluation of an outer narrowing step. A possible evaluation of the previous example using lazy narrowing is

foo (foo X Y ) Z = 0

⟹ {lazy narrowing of foo via equation (6)}

{⟨X , 0⟩, ⟨Y , 0⟩} ⟶ foo 0 Z = 0

⟹ {lazy narrowing of foo via equation (6)}

{⟨X , 0⟩, ⟨Y , 0⟩} ⟶ ({⟨Z , 0⟩} ⟶ 0) = 0

⟹ {propagation of σ}

{⟨X , 0⟩, ⟨Y , 0⟩, ⟨Z , 0⟩} ⟶ 0 = 0

⟹ {unification}

{⟨X , 0⟩, ⟨Y , 0⟩, ⟨Z , 0⟩} ⟶ true.

Since lazy narrowing cannot ensure the termination of a program, determining whether the same program is confluent is undecidable. To overcome this problem, more restrictions are required for a language based on lazy narrowing to ensure that its programs are confluent and, in turn, complete. These restrictions are essentially the same as those imposed on purely functional languages: the language must be constructor based; equations must be left linear (meaning that variables on the left hand side of equations must appear only once); no free variables may appear on the right hand side of equations, that is, variables on the right hand side of equations must also appear on the left hand side; and that the left hand sides of any two equations should not unify.

4.2.5 Rejection and normalisation rules

Even restricting narrowing to basic narrowing, and stipulating that languages should be constructor based, are inadequate to raise the computational expressiveness of functional logic languages beyond that achieved by using the traditional SLD-resolution with “flattening” to remove nested function calls. We require still more sophisticated restrictions to justify using narrowing over SLD-resolution as an operational semantics for a functional logic language. Fortunately, two further improvements exist which make narrowing more powerful. We discuss each of these in turn.

A practical problem with innermost narrowing is that even if the two outermost symbols of an equation do not unify—and thus the entire expression will not unify—we continue to narrow at the innermost terms, performing redundant computation. To illustrate this point, recall the definition of natural numbers given earlier. By using an innermost strategy, one possible narrowing sequence for the expression X + Y = 0 is given by

X + Y = 0

⟹ {innermost narrowing of + via equation (5)}

{⟨X , succ M′⟩, ⟨Y , N′⟩} ⟶ succ (M′ + N′) = 0

⟹ {innermost narrowing of + via equation (5)}

{⟨X , succ M′⟩, ⟨Y , N′⟩} ⟶

({⟨M′, succ M′′⟩, ⟨N′, N′′⟩} ⟶ succ succ (M′′ + N′′)) = 0
⟹ {propagation of σ}

{⟨X , succ succ M′′⟩, ⟨Y , N′′⟩} ⟶ succ succ (M′′ + N′′) = 0

⋮

and so on. We can avoid infinite sequences like this one by checking the equality of the two outermost constructors at each narrowing step. After the first narrowing step in the previous example we can “reject” the entire expression since the constructors succ and 0 do not unify and hence the entire expression will not unify.

A rejection rule, however, can only be used to disregard superfluous narrowing derivations if the outermost symbols of corresponding terms or subterms are constructors. In other words, we are unable to reject a goal expression if a function call surrounds different constructors since the expressions could evaluate to the same term. With this in mind, functions need to be evaluated as early as possible if the rejection rule is to be applied.

For example, consider the function

∑ 0 = 0.  (9)
∑ succ N = succ N + ∑ N .,  (10)

which sums the first n elements of the natural numbers. An innermost narrowing strategy for the expression ∑ X = succ 0 produces

∑ X = succ 0
⟹ {innermost narrowing of ∑ via equation (10)}
{⟨X , succ N′⟩} ⟶ succ N′ + ∑ N′ = succ 0
⟹ {innermost narrowing of ∑ via equation (10)}
{⟨X , succ N′⟩} ⟶ succ N′ +
({⟨N′, succ N′′⟩} ⟶ succ N′′ + ∑ N′′) = succ 0
⟹ {propagation of σ}
{⟨X , succ succ N′′⟩} ⟶ succ succ N′′ + succ N′′ + ∑ N′′ = succ 0
⋮

as a possible narrowing derivation. The rejection rule cannot be applied here since the outer symbol on the left hand side is always the (infix) function ‘+’. The way to improve performance is to rewrite each side of the equation to normal form, hoping that a constructor will replace any outermost function symbol.

Rewriting is confluent for a confluent program and semantically preserving in that logical variables are never bound and terms are replaced by equal terms. We can confidently rewrite both sides of an equation to normal form between narrowing steps using the appropriate program equations for the function. This is known as normalising narrowing. Thus, we can rewrite the last step in the above derivation to

⋮
⟹ {propagation of σ}
{⟨X , succ succ N′′⟩} ⟶ succ succ N′′ + succ N′′ + ∑ N′′ = succ 0
⟹ {normalisation of + twice via equation (5)}
\{⟨X , succ succ N′′⟩\} ⟶ succ \underline{succ} (N′′ + (succ (N′′ + ∑ N′′))) = succ \underline{0}

which terminates after the normalisation step since the two subterms at corresponding positions (underlined above) do not unify. Additionally, by using normalisation we can compute in a deterministic fashion for as long as possible until we must apply a narrowing step. As a result, this can reduce a search space since the narrowing derivations are shorter and less of them are performed.

We can combine all these above restrictions and efficiency tweaks to form a narrowing semantics called innermost basic narrowing with normalisation for constructor based

module list(elem).
datatype list = {′:′(elem, list) ; [ ]}.
func  append : list, list → list.
pred  member : elem, list.
rules.
append([ ], YS)  = YS.
append(X : XS, YS) = X : (append(XS, YS)).

member(X , X : ).

member(X , : XS) ← member(X , XS).
end list.

Figure 4: An implementation of lists in ALF.

languages. Hanus [Han94] argues that this computational method is superior to SLDresolution, certainly in terms of efficiency. However, by making narrowing efficient, some of the lucidity of general narrowing is lost and the added complexity greatly decreases the elegance of narrowing. In turn, programs written in functional logic languages become difficult to reason about suggesting that a more mathematically sound computational model should be developed instead.

4.3 Programming Relations in ALF

ALF [HS93] is a functional logic programming language which encapsulates the main ideas presented earlier in the section. ALF’s operational semantics is a combination of resolution for predicates and innermost basic narrowing with normalisation for functions. In the remainder of this section, we introduce some ALF notation and discuss the suitability of implementing relations in ALF.

ALF is based on Horn clause logic with equality thus supporting predicates for logic programming and functions for functional programming. Since ALF is a genuine integration of functions and logic, functional expressions can be used in goal queries and predicates may appear in conditional equations.

An ALF program is a collection of modules of which there is one main module containing a string of goal queries. Rather than providing a comprehensive tutorial on ALF, we only introduce those notions which are important for our purposes. Let us now provide an indication of the structure of an ALF program by presenting an implementation of lists, as illustrated in Figure 4. This example demonstrates that the module list is parametrically defined for any type elem; ALF is not polymorphically typed in the same manner as found in most functional languages, like Haskell.

module map.
datatype abs = {inc ; double}.
func  map : abs, list → list;

apply : abs, nat → nat.

rules.
map(F , [ ])  = [ ].
map(F , X : XS) = (apply(F , X )) : (map(F , XS)).
apply(inc, N )  = N + 1.
apply(double, N ) = N × 2.
end map.

Figure 5: An implementation of the function map in ALF.

Additionally, ALF is based on a first-order semantics, i.e., ALF does not support functions or predicates which take other functions or predicates as arguments or return them as results. In general, however, higher-order functions can be transformed into firstorder ones by providing an explicit definition of an apply function, as proposed by both Warren [War82] and Goguen [Gog88]. To illustrate this point, consider the definition of the higher-order function map in ALF, shown in Figure 5. In essence, this simulation of higher-order functions requires us to explicitly define an equation of apply for every possible function we would like to use with map. This is a somewhat tedious process but, nevertheless, we can still achieve the same functionality as found in a true higher-order language for the above simple use of higher-order programming.

The main reason why ALF is first-order arises from the notion of actually solving for a function (or predicate) variable. In a true higher-order logic language, we could require that higher-order function variables quantify over all denotable functions—rather than simply those defined in the program—such that any unbound function variable should be instantiated to some appropriate λ-abstraction, say. (This is exactly what happens in higher-order logic programming languages and is discussed further in Section 5.) Performing this kind of evaluation, however, requires higher-order unification which is computationally expensive. ALF was developed as a first-order language since such elaborate semantics were deemed unnecessary for application programming. However, the inclusion of higher-order unification into functional logic languages is an active area of research [Pre94, Qia94].

Of course, ALF could have adopted the same syntactic notion of higher-order variables found in some functional languages whereby such a variable may only be a formal parameter to a function and during a call to this function it is necessarily instantiated. This clearly avoids the requirement of solving function variables yet still provides programming

module relations.
datatype rel = {inc ; leq}.
pred  comp : rel, rel, nat, nat;

isect : rel, rel, nat, nat; conv : rel, nat, nat; apply : rel, nat, nat.

rules.
comp(R, S, A, C ) ← apply(R, A, B), apply(S, B, C ).
isect(R, S, A, B) ← apply(R, A, B), apply(S, A, B).
conv(R, B, A) ← apply(R, A, B).

apply(inc, N , N + 1).

apply(leq, M , N ) ← M ≤ N .
end relations.

Figure 6: An implementation of a fragment of the relational calculus in ALF.

convenience. ALF is currently being extended to encompass this style of programming.

Let us now examine how relations may be implemented in ALF. We have the liberty of choosing whether to represent relations as functions or as predicates. After a little consideration, predicates seem to be a more suitable method since they better capture the non-determinism of relations. Reinforcing this decision is the fact that ALF imposes strict semantic restrictions on functions in order to ensure completeness of the narrowing procedure. One such restriction is that free variables are not permitted on the right hand side of equations; in other words, the only variables which may appear there are formal parameters of the function. An implementation of a small part of the relational calculus is given in Figure 6.

By employing a first-order syntax, we lose some clarity of definition through the numerous applications of the apply predicate. Moreover, ALF does not support currying and thus our queries become somewhat less aesthetic than we would like. For example, it is difficult to translate the relational predicate a (inc^{∘} · inc^{∘}) 5 into the above definition of relations: we would like to be able to write it as the curried expression

?− comp (conv inc) (conv inc) A 5.,

but, in ALF, we must either implicitly represent composition by the conjunction

?− conv(inc, B, 5), conv(inc, A, B)., or, alternatively, define an extra equation in the apply procedure to embody the predicate conv(inc, X , Y ). Despite our ability to overcome these difficulties, much of the clarity of the relational program is drowned by murky syntax.

From the above discussion, it might appear that functional logic languages are entirely unsuitable for implementing a relational calculus. However, we must bear in mind that the problems with ALF arise almost solely from the fact that it employs a first-order syntax. Indeed, other functional logic languages exist which do exhibit higher-order features, like the language Babel [KLMR90] for instance. The main drawback of these languages, though, is that their implementations are still under development and are incomplete. There are also functional logic languages with higher-order features that do not employ narrowing as the basis for their operational semantics, like Escher [Llo95]. With such languages nearing completion, it is quite possible that they could support an implementation of a relational calculus quite easily.

From a purely computational point of view, one standard problem encountered in most logic programming languages needs to be addressed: as a consequence of the left to right evaluation strategy adopted in logic programming language implementations, whereby the leftmost unsolved goal is selected for resolution, certain queries can result in infinite computation. A simple example which demonstrates this undesirable property is the query

?− X + Y = Z , X + Y = 2.,

where ‘+’ is addition on natural numbers. Since the leftmost subgoal X + Y = Z can be satisfied in an infinite number of ways, the whole query results in non-termination when all possible solutions are requested. The situation is, in theory, rectified by simply swapping the two subgoals in the conjunction but, in practice, is difficult to detect. The problem can essentially be reduced to the fact that conjunction is not commutative in logic programming languages. This situation arises regularly in the relational calculus since composition is essentially a conjunctive goal. Therefore, we run into difficulties with an implementation of relations in ALF. One possible solution to this problem is to adopt a new search strategy as discussed later in Section 6.

5 Higher-Order Logic Programming Languages

Higher-order logic programming utilises a higher-order logic as its basis of computation. By doing so, higher-order logic languages gain several advantages over the more common first-order languages, like Prolog. Firstly, higher-order logic languages naturally support the usual higher-order features found in functional programming languages. Secondly, the logic provides the elegant mechanisms of λ-terms as a means for describing predicates which results directly in programming benefits. Finally, the higher-order logic treats predicates and functions in a similar fashion—predicates being characteristic functions— hence allowing quantification over function symbols and extending the mechanisms for constructing predicates to the full class of functional expressions.

The notion of higher-order logic programming is captured using a generalisation of Horn clauses. These Horn clauses are described in the higher-order logic, namely Church’s simple theory of types [Chu40] (with a few extensions) in this instance. Higher-order Horn clauses are detailed in the next section.

5.1 A Higher-Order Logic

The ability to define higher-order predicates, taking other predicates as arguments, in a logic programming language provides a notational convenience easing an implementation of relations in such a language. To accommodate this facility, the underlying logic of the programming language should possess the ability to quantify over predicate variables. The higher-order logic we adopt here is a generalisation of Horn clause logic and we employ the same definition of Horn clauses appearing at the beginning of Section 4. However, since we wish to quantify over predicates, we must update our definition of atomic formulas. Recall from Section 4 that an atomic formula has the form p t_{1} … t_{n} where p is a predicate symbol. We now extend this definition and additionally allow p to be a predicate variable, denoted by an upper case letter, like P.

A common procedure that we would like to define in our language is map which takes a predicate P and two lists XS and YS as arguments. The map procedure succeeds in the case where the list obtained by solving predicate P using each element of list XS in turn is identical to list YS. Using Horn clause terminology, and assuming the standard definition of lists, map can be expressed in a curried notation as

∀P.map P [ ] [ ].

∀P, X , XS, Y , YS.map P (X : XS) (Y : YS) ← (P X Y ) ∧ (map P XS YS).,

where P is a predicate variable. Notice that all variables in our predicate definitions are explicitly universally quantified in accordance with the definition of Horn clauses given in Section 4. Let us consider the higher-order logic program obtained by combining the clauses for map with the clause

∀N .inc N (N + 1).,

which, assuming the definition of function ‘+’, describes a procedure that increments its first argument by one. In the higher-order language, the goal query

?− ∃Y .map (inc) (1 : 2 : 3 : [ ]) Y .,

is solvable if the variable Y is substituted by (1 + 1) : (2 + 1) : (3 + 1) : [ ]. An interesting observation can be made at this stage. Notice that ‘+’ does not evaluate its arguments as would occur in a purely functional or functional logic programming language. That is to say, 1 + 1 is not evaluated to 2 as one might expect. This is a consequence of how logic programming languages perform computations and we delay the discussion of this technical point until later. Suffice to note that functions in logic programming languages play a similar role to constructor functions in purely functional programming languages, i.e., they are irreducible.

From the point of view of representing relations in higher-order logic programming languages, the ability to solve for logic variables in goal formulae and the natural handling of nondeterminism in the language are the most appealing aspects. For example, consider the procedure

∀YS.append [ ] YS YS.

∀X , XS, YS, ZS.append (X : XS) YS (X : ZS) ← append XS YS ZS.,

which appends two lists together to form a new list. Then the query

?− ∃XS, YS.append XS YS (1 : 2 : [ ]).,

is legitimate in the higher-order language. Indeed, several solutions exist which satisfy this query. The possible solutions, separated by ‘;’, are

?− XS = [ ]
YS = 1 : 2 : [ ] ;
?− XS = 1 : [ ]
YS = 2 : [ ] ;
?− XS = 1 : 2 : [ ]
YS = [ ] ;
?− no.

The ability to find solutions to a query is a result of the built in search facility of logic programming languages; a logic language attempts to find substitutions for any logic variables which, when applied to the query, satisfy (or solve) it.

5.2 The Simply Typed λ-Calculus

The language underlying the formal system of the higher-order logic is that of a typed λ-calculus which we discuss in this section. A passing acquaintance with Church’s simple theory of types [Chu40] is assumed in the discussion.

Basically, the terms of our language now incorporate λ-terms which have the following form:

λ \underbrace{x_{1} … x_{n}}_{binder} .(\underbrace{p}_{head} \underbrace{t_{1} … t_{m}}_{arguments}).

Here, x_{1} … x_{n}, for n ≥ 0, are variables and the rest of the expression is simply an atomic formula, as described earlier in the section, although we identify the head and arguments of this atomic formula as indicated above.

Each λ-term also has an associated type. The types used in our language, often referred to as simple types, comprise of sorts and type constructors. Both of these are familiar from functional programming. A function type is indicated by α_{1} → ⋯ → α_{n} → β, for n ≥ 0, α_{1}, …, α_{n} types, and β an atomic type. We assume that ‘→’ associates to the right. One special sort ‘o’ exists which is the type of propositions in the language. Therefore, α_{1} → ⋯ → α_{n} → o denotes the type of a predicate.

Through the familiar formalisms of application and abstraction, the necessary tools to cope with higher-order language features are obtained. The meaning of abstraction and application are defined by the rules of λ-conversion, the collective name for the following rules:

1. α-conversion λx.T ≡ λy.T [y/x] provided y ∉ fv(T ),

2. β-conversion (λx.T_{1})T_{2} ≡ T_{1}[T_{2}/x], and

3. η-conversion λx.T x ≡ T provided x ∉ fv(T ).

Substitution is represented by the notation T [E/x], which means that variable x is replaced by term E in term T . (We do not detail the definition of substitution here.) The function fv returns the set of free variables of an expression. Given the above rules, we can define equality of two terms, S and T , by

S = T ≡ S λ-converts to T .

Additionally, we say that a λ-term is in λ-normal form if no β- or η-conversions can be applied to it.

By means of abstraction and application, we can construct λ-terms from existing predicates and manipulate them in various ways. To illustrate this point, consider the parent procedure defined by the clauses

parent carrie jeff . parent jeff alison. parent joanna harry. parent harry bill.

We can create a new predicate—the “converse” of parent—which reverses the order of the arguments supplied to parent by writing λX , Y .parent Y X . We may write goals which consist of λ-terms, for example,

?− (λX , Y .parent Y X ) alison jeff .

?− yes.

More complicated λ-terms can be constructed by using the logical connectives of Horn clauses. For example, we can construct a predicate

λX , Z .∃Y .(parent X Y ) ∧ (parent Y Z ).,

representing a grandparent relationship. Predicates created in this manner can be used wherever a “regular” predicate is expected. Thus, it is perfectly acceptable to query

?− ∃XS.map (λX , Y .∃Z .(parent X Z ) ∧ (parent Z Y )) (carrie : joanna : [ ]) XS.

This query succeeds if XS is bound to (alison : bill : [ ]).

5.3 Higher-Order Horn Clauses

In higher-order logic programming, there exists an analogy between predicates and functions; after all, predicates are simply characteristic functions. However, functions are not handled in exactly the same way as predicates. Functions are evaluated solely via the rules of λ-conversion given in the previous section. By restricting β-conversion so that it only encodes the most basic form of substitution, rather than the more usual reduction, we can actually find the value of a function variable. For example, let us define a new procedure mapfun which takes a function rather than a predicate as its first argument:

∀F .mapfun F [ ] [ ].

∀F , X , XS, YS.mapfun F (X : XS) ((F X ) : YS) ← mapfun F XS YS.

From this definition, we can query

?− ∃F .mapfun F (1 : 2 : [ ]) (1 + 1 : 2 + 1 : [ ]).,

which will result in F being bound, quite sensibly, to λX .X + 1. To find the value of the function variable F , substitution is used to analyze the structure of λ-terms and the rule of β-conversion provides a means for representing the evaluation of functions. However, finding a value for a function variable depends critically on using a weakened form of both functions and function evaluation. This method of evaluation cannot be used for predicates since predicates embody the “real” computational phases in our higher-order logic.

Therefore, from a computational point of view, it makes sense to limit the positions a predicate variable can occupy. For example, consider the two possible structures of a definite clause, namely ∀x⃗.A and ∀x⃗.A ← G. (The notation x⃗ is used to denote that the binder of the ∀-term contains all the variables appearing in the body of the term.) There are four locations where a predicate variable P could appear in a definite clause:

1. the head of the atomic formula A,

2. an argument position of the atomic formula A,

3. the head of an atomic goal formula in G, or

4. an argument position of an atomic goal formula in G,

illustrated pictorially by

∀P, X , Y , XS, YS. 1 ; ↓ ; map 2 ; ↓ ; P (X : XS) (Y : YS) ← (3 ; ↓ ; P X Y ) ∧ (map 4 ; ↓ ; P XS YS).

Immediately, we can see that position 1 is an unrealistic location for a predicate variable and we do not allow a predicate variable to assume such a position. We now revise our definition of higher-order Horn clauses so as to prohibit predicate variables appearing there. First, let us say that an atomic formula A is rigid if no free variables appear in its head position, otherwise we say it is flexible. We can then define higher-order Horn clauses by

D ::= A_{r} | A_{r} ← G | ∀x.D
G ::= A | G ∨ G | G ∧ G | ∃x.G,

where the term A_{r} signifies that that the atomic formula A is rigid.

Notice, though, that we still allow predicate variables to occupy extensional locations in goal queries. For example, we can query

?− P jeff alison.,

which could give the solutions

?− P = λX , Y .parent X Y ;
?− P = λX , Y .parent jeff alison ;
?− P = λX , Y .(parent X alison) ∧ (parent jeff Y ) ;
⋮

and so on. Since an infinite amount of predicates could be generated to solve such a query, it seems unreasonable to allow for the solution of arbitrary predicate variables which occupy extensional locations. Despite this observation, such goals can have a meaningful role to play in programs since the range of acceptable solutions for a predicate variable can be restricted to a finite number by other clauses in the program, as explained by Nadathur and Miller [NM95].

5.4 Method of Computation

As in first-order logic, the notion of computation in higher-order logic corresponds to solving a query with respect to a given program. An interpreter must perform a search guided by the top level language symbol in the query being solved. The logical meaning of a connective symbol in the programming language is given by an abstract proof of its corresponding formula in some suitable sequent calculus. Conversely, each formula can be interpreted operationally as a search instruction in the interpreter. We do not introduce the inference rules of the sequent calculus here but rather refer the interested reader to Nadathur and Miller [NM90, NM95] for a complete discussion.

The main differences between proof systems for first-order and higher-order logics are the presence of λ-conversion rules and a richer syntax of formulas. In what follows, we discuss the higher-order unification problem and from this develop an implementable strategy for computing higher-order unifiers.

5.4.1 Higher-order unification

Earlier, we noted that we require a procedure which determines whether or not a query succeeds with respect to a given program. This procedure must apply the technique of only choosing instantiations for variables when an appropriate binding becomes apparent.

We therefore transform the existential variables in goal formulas into logic variables, i.e., ∃x.G(x) becomes G(X ). This is, in essence, analogous to what happens in first-order logic; the logic variables are “place holders” for the existential variables until we can determine a suitable value for the logic variable.

The main difference between first- and higher-order logic is that we must consider the unification of λ-terms where equality between such terms is based on the rules of λ-conversion, presented earlier. Before we describe the process of computing unifiers in a higher-order setting, let us first settle on some terminology. We follow closely the notation of Nadathur and Miller [NM95] on which the discussion is based.

We call a pair of terms ⟨T , S⟩, of the same type, a disagreement pair. A disagreement set is a finite set {⟨T_{i}, S_{i}⟩|1 ≤ i ≤ n} of disagreement pairs and a unifier for a disagreement set is a substitution θ such that T_{i} · θ =_{λ} S_{i} · θ for 1 ≤ i ≤ n. The equality sign ‘=_{λ}’ means equality with respect to the rules of λ-conversion and we write T · θ to represent the application of substitution θ to expression T . The question of unifying two terms is therefore equivalent to unifying their λ-normal forms.

Hence, higher-order unification aims to determine whether an arbitrary disagreement set has any unifiers and, if so, to provide one such unifier. In a higher-order setting, finding a unifier for an arbitrary disagreement set is undecidable [Hue73]. Moreover, most general unifiers may not exist for unifiable higher-order disagreement sets.

Despite these problems, Huet [Hue75] proposed a sound and complete method of finding unifiers for a given disagreement set. By sound, we mean that any substitution computed for a disagreement set by the procedure is a unifier for and by complete, we mean that the procedure will find a unifier for a given disagreement set if one exists; in the case that a unifier does not exist for a disagreement set, however, the procedure may not terminate. For a strictly first-order disagreement set, the procedure always returns a most general unifier. The method hinges on the observation that for some disagreement sets it is relatively straightforward to discover if at least one or no unifiers exist for the set. The unification procedure attempts to reduce a given disagreement set to one of these two types by an iterative application of two functions operating on disagreement sets.

The following lemma, established by Huet [Hue75], provides the basis for the first of these functions. The notation U(D) denotes the set of unifiers for a disagreement set D.

Lemma 1 Let S = λx⃗.C_{1} A_{1} … A_{n} and T = λx⃗.C_{2} B_{1} … B_{m} be two rigid terms of the same type that are in λ-normal form. Then θ ∈ U({⟨S, T ⟩}) if and only if

1. C_{1} = C_{2}, (which implies that n = m), and

2. θ ∈ U({⟨λx⃗.A_{i}, λx⃗.B_{i}⟩ | 1 ≤ i ≤ n}).

This lemma suggests that we can determine whether no unifiers exist for a disagreement set D or that we can reduce the problem to finding unifiers for the arguments of each pair in D. By a simple process of α-conversion, we can arrange for the two terms in each disagreement pair to have identical binders (which may be empty). We can now construct a function called simplify, illustrated in Figure 7, which takes a disagreement set and performs the above computation.

1. simplify(∅) = ∅

2. simplify({⟨S, T ⟩}) =

if S is flexible then return {⟨S, T ⟩}.

if T is flexible then return {⟨T , S⟩}.

otherwise

let S = λx⃗.C_{1} A_{1} … A_{n} and

T = λx⃗.C_{2} B_{1} … B_{m} be in λ-normal form.

if C_{1} ≠ C_{2} then return Fail.

otherwise return simplify({⟨λx⃗.A_{i}, λx⃗.B_{i}⟩ | 1 ≤ i ≤ n}).

3. simplify({⟨S_{i}, T_{i}⟩ | 1 ≤ i ≤ s}) =

if simplify({⟨S_{i}, T_{i}⟩}) = Fail for some i then return Fail.

otherwise return ⋃_{i=1}^{s} simplify({⟨S_{i}, T_{i}⟩}).

Figure 7: The function simplify.

The function simplify therefore transforms a given disagreement set into either the failure symbol Fail or a disagreement set consisting solely of “flexible-flexible” or “flexiblerigid” disagreement pairs. As illustrated in the following lemma—whose proof may be found in Huet [Hue75]—we can be confident that the unifiers of the initial disagreement set are the same as those for the reduced disagreement set.

Lemma 2 For a disagreement set D, U(D) = U(simplify(D)).

The first stage in computing the unifiers for a disagreement set D thus involves evaluating simplify(D). If the result is Fail then no unifiers exist for D. Alternatively, if the result is an empty set or a set consisting only of flexible-flexible pairs then at least one unifier can be found easily for D, namely the trivial unifier λx⃗.true [NM95]. More work needs to be performed, however, if the new set contains any flexible-rigid pairs. In this case, we must consider substitutions which attempt to make the heads of the two terms identical. Let us now present the function match which undertakes such a task.

Let S = λx⃗.F A_{1} … A_{n} be a flexible term and T = λx⃗.C B_{1} … B_{m} be a rigid term where both terms have the same type and are in λ-normal form. Additionally, let the type of F be α_{1} → ⋯ → α_{n} → β where n ≥ 0 and β is an atomic type, and, for 1 ≤ i ≤ n, let w_{i} be a variable of type α_{i}. Then, for fresh variables H_{k}, k ≥ 0, of appropriate types, the function match—taking a disagreement pair to a disagreement set—may be defined as shown in Figure 8.

The role of match is to suggest a set of substitutions which form “partial” unifiers and thus bring the search for a “complete” unifier closer to a solution. The following lemma, due to Huet [Hue75], states that match achieves this goal.

1. match(⟨S, T ⟩) = imitate(⟨S, T ⟩) ∪ ( ⋃_{i=1}^{n} project_{i}(⟨S, T ⟩)).

2. imitate(⟨S, T ⟩) =

if C is a variable which appears in x⃗ then return ∅.

otherwise

return {⟨F , λw_{1} … w_{n}.C (H_{1} w_{1} … w_{n}) … (H_{m} w_{1} … w_{n})⟩}.

3. project_{i}(⟨S, T ⟩) =

if α_{i} ≠ β_{1} → ⋯ → β_{s} → β for s ≥ 0 then return ∅.

otherwise

return {⟨F , λw_{1} … w_{n}.w_{i} (H_{1} w_{1} … w_{n}) … (H_{s} w_{1} … w_{n})⟩}.

Figure 8: The function match.

Lemma 3 Let S be a flexible term and T be a rigid term where both terms have the same type and are in λ-normal form. If there is a substitution θ ∈ U({⟨S, T ⟩}) then there exists a substitution φ ∈ match(⟨S, T ⟩) and a “smaller” substitution θ′ such that θ = θ′ · φ.

We now have established the necessary machinery required to describe a unification algorithm based on the iterative use of functions simplify and match. We introduce the notion of a P-derivation—pronounced “program derivation”—as a higher-order generalisation of SLD-resolution, the computational model used in first-order logic languages. P-derivations are used to determine the success of a goal query against a program.

5.4.2 P-derivations

First of all, let us create the triple ⟨G, D, θ⟩ where G is a set of goal formulas, D is a disagreement set, and θ is a set of substitutions. We then say that a triple ⟨G_{2}, D_{2}, θ_{2}⟩ is a P-derivation of a triple ⟨G_{1}, D_{1}, θ_{1}⟩ with respect to program P if and only if D_{1} ≠ Fail and one of the following three situations holds:

1. Goal reduction step. θ_{2} = ∅, D_{2} = D_{1}, and there is a goal formula G ∈ G_{1} such that either:

G = G_{1} ∧ G_{2} ⇒ G_{2} = (G_{1} − {G}) ∪ {G_{1}, G_{2}};
G = G_{1} ∨ G_{2} ⇒ G_{2} = (G_{1} − {G}) ∪ {G_{i}}, for any 1 ≤ i ≤ 2; or
G = ∃x.P ⇒ G_{2} = (G_{1} − {G}) ∪ {[y/x]P} where y is a fresh variable.

2. Backchaining step. Let G ∈ G_{1} be a positive rigid atomic formula, and let D ∈ P be a definite clause of the form ∀x⃗.A ← G′. Then θ_{2} = ∅, G_{2} = (G_{1} − {G}) ∪ {G′}, and D_{2} = simplify(D_{1} ∪ {⟨G, A⟩}).

3. Unification step. Let ⟨S, T ⟩ ∈ D_{1} be a flexible-rigid pair. Then either:

match(⟨S, T ⟩) = ∅ ⇒ D_{2} = Fail, or
φ ∈ match(⟨S, T ⟩) ⇒ θ_{2} = φ, G_{2} = G_{1} · φ, and D_{2} = simplify(D_{1} · φ).

For a given goal set G, we call a sequence ⟨G_{i}, D_{i}, θ_{i}⟩_{1≤i≤n} a P-derivation sequence if G_{1} = G, D_{1} = ∅, θ_{1} = ∅, and, for all 1 < k < n, ⟨G_{k+1}, D_{k+1}, θ_{k+1}⟩ is a P-derivation of ⟨G_{k}, D_{k}, θ_{k}⟩. Using this notation, we say that a P-derivation sequence terminates if either:

1. G_{n} consists solely of flexible-rigid pairs (or is empty) and D_{n} consists solely of flexible-flexible pairs (or is empty), or

2. D_{n} = Fail.

In case 1, we say that the P-derivation sequence terminates successfully and we compute the answer substitution as the composition θ_{n} · . . . · θ_{1} of substitutions.

5.4.3 Some examples

Let us now step through several examples to highlight the computational strategy presented in the previous section. Consider finding a unifier for the disagreement set D_{1} = {⟨F 1, 1⟩, ⟨F 2, 2⟩} where F : nat → nat (assuming that nat is the type of natural numbers). A unification step may be applied using either of the flexible-rigid terms in D_{1}. If we choose the first term, the unification step produces the set

match(⟨F 1, 1⟩) = {⟨F , λw.1⟩, ⟨F , λw.w⟩},

of possible substitutions. The first of these substitutions is given by the function imitate and the second by project. We may arbitrarily select either of these substitutions to apply in the remainder of the unification step. Suppose we choose the first substitution, namely φ = ⟨F , λw.1⟩. Then we generate the new disagreement set D′_{1} by

D′_{1} = D_{1} · φ = {⟨(λw.1) 1, 1⟩, ⟨(λw.1) 2, 2⟩}.

Notice that we can apply a β-conversion to each of the disagreement pairs in D′_{1} resulting in

D′_{1} = {⟨1, 1⟩, ⟨1, 2⟩}.

To complete the unification step we must call the function simplify(D1^{′}). Clearly, this results in Fail since the rigid-rigid pair ⟨1, 2⟩ does not unify. Therefore, we are forced to backtrack and choose the alternative substitution φ = ⟨F , λw.w⟩. This time, we obtain the disagreement set

D′_{1} = D_{1} · φ = {⟨(λw.w) 1, 1⟩, ⟨(λw.w) 2, 2⟩},

and, by β-converting each pair, we get

D′_{1} = {⟨1, 1⟩, ⟨2, 2⟩}.

We can see that the function simplify will succeed and return D′_{1} unchanged. The result of the unification step is therefore the substitution θ_{2} = ⟨F , λw.w⟩.

As a more involved example, consider the disagreement set D_{1} = {⟨F 1, 2 + 1⟩} for F : nat → nat. Since the only disagreement pair in D_{1} is flexible-rigid, the application of a unification step is appropriate at this stage. The possible substitutions for F are therefore computed by

match(⟨F 1, 2 + 1⟩) = {⟨F , λw.(H_{1} w) + (H_{2} w)⟩, ⟨F , λw.w⟩},

where the first substitution was produced by imitate and the second by project. By stepping through the definition of project, we can see exactly how the substitution ⟨F , λw.w⟩ was created: the argument to F is clearly not of functional type (it has type nat), i.e., variable w in the term λw.w is a first-order variable and, as a result, w cannot have any arguments in the body of the λ-abstraction λw.w.

Continuing with the unification step, we select the second of the substitutions, φ = ⟨F , λw.w⟩, so producing the disagreement set

D′_{1} = D_{1} · φ = {⟨(λw.w) 1, 2 + 1⟩},

and by a β-conversion, we end up with

D′_{1} = {⟨1, 2 + 1⟩}.

The obligatory application of simplify(D′_{1}) results in Fail since 1 and 2 + 1 do not unify. Therefore, we try the first substitution φ = ⟨F , λw.(H_{1} w) + (H_{2} w)⟩ and obtain the disagreement set

D′_{1} = D_{1} · φ = {⟨(λw.(H_{1} w) + (H_{2} w)) 1, 2 + 1⟩},

which β-converts to

D′_{1} = {⟨(H_{1} 1) + (H_{2} 1), 2 + 1⟩}.

As ⟨(H_{1} 1) + (H_{2} 1), 2 + 1⟩ is a rigid-rigid disagreement pair, we compute that

D_{2} = simplify(D1^{′}) = {⟨H_{1} 1, 2⟩, ⟨H_{2} 1, 1⟩},

and that

θ_{2} = φ = ⟨F , λw.(H_{1} w) + (H_{2} w)⟩.

Therefore, simplify reduces the problem of finding unifiers for the two function terms in set D′_{1} to that of finding unifiers for their arguments. We can repetitiously perform a unification step on either of the disagreement pairs contained in D_{2}. Suppose we choose the first pair, then we get:

match(⟨H_{1} 1, 2⟩) = {⟨H_{1}, λx.2⟩, ⟨H_{1}, λx.x⟩}.

The second substitution ⟨H_{1}, λx.x⟩ for the higher-order variable H_{1} is inappropriate since applying this substitution to D_{2} gives

{⟨H_{1} 1, 2⟩, ⟨H_{2} 1, 1⟩}
= {apply substitution ⟨H_{1}, λx.x⟩}
{⟨(λx.x) 1, 2⟩, ⟨H_{2} 1, 1⟩}
= {β-conversion}
{⟨1, 2⟩, ⟨H_{2} 1, 1⟩}
= {application of simplify}
Fail.

Therefore, we have little alternative but to choose the first of the two substitutions for H_{1} to get

D_{3} = {⟨2, 2⟩, ⟨H_{2} 1, 1⟩},

and

θ_{3} = ⟨H_{1}, λx.2⟩.

After another unification step, we have

match(⟨H_{2} 1, 1⟩) = {⟨H_{2}, λy.1⟩, ⟨H_{2}, λy.y⟩}.

This time, there is no restriction on the choice of substitution for variable H_{2} and we can arbitrarily select either. Suppose we choose the second substitution for H_{2}, then we end up with

{⟨2, 2⟩, ⟨H_{2} 1, 1⟩}
= {substitution of ⟨H_{2}, λy.y⟩}}
{⟨2, 2⟩, ⟨(λy.y) 1, 1⟩}
= {β-conversion}
{⟨2, 2⟩, ⟨1, 1⟩}
= {application of simplify}
∅.,

and

θ_{4} = ⟨H_{2}, λy.y⟩.

We can then construct the answer substitution θ from the composition θ_{4} · θ_{3} · θ_{2} · ∅ of each substitution chosen at each step in the derivation process:

⟨H_{2}, λy.y⟩ · ⟨H_{1}, λx.2⟩ · ⟨F , λw.(H_{1} w) + (H_{2} w)⟩

= {substitution}
⟨H_{2}, λy.y⟩ · ⟨F , λw.((λx.2) w) + (H_{2} w)⟩
= {substitution}
⟨F , λw.((λx.2) w) + ((λy.y) w)⟩
= {two β-conversions}
⟨F , λw.2 + w⟩

unifying the original disagreement set D_{1}.

5.5 Programming Relations in λProlog

The higher-order logic language λProlog, developed by Nadathur and Miller [NM88], naturally supports higher-order programming features in a manner consistent with its underlying logical foundation. In what follows, we examine how to implement both Ruby [Jon90] primitives and some basic operations of the relational calculus [BdM95] in λProlog [LHRB94]. The syntax of λProlog is introduced informally as the section progresses.

5.5.1 Implementing Ruby primitives

We can define Ruby’s tuple data value in λProlog via the declaration

kind tuple type → type → type.
type :  A → B → (tuple A B).

The ‘kind’ operator creates a new type which is simply a type constructor of arity one less than the number of occurrences of the keyword ‘type’ in the declaration. In the case above, the type constructor tuple is declared taking two arguments to this new type. Function and predicate symbols are introduced via a ‘type’ declaration. The infix function symbol ‘:’ declared above takes two arbitrary types, A and B, and returns a value of type tuple A B.

Notice that λProlog is polymorphically typed and is curried in the same sense as in many functional programming languages, like Haskell, except that type signatures must be given explicitly for all function and predicate symbols. Type variables in λProlog are denoted by identifiers beginning with an upper case letter. The type of propositions (or “truth values”) is the special type ‘o’ and so the type signature of a predicate in λProlog terminates with this type. A small λProlog program defining “Peano” natural numbers, given in Figure 9, demonstrates some of these syntactic points. Natural numbers are thus represented by zero, (succ zero), (succ (succ zero)), and so forth.

We make use of the built-in list type in λProlog in order to implement the primitive relations pertaining to the Ruby list data value. Lists in λProlog are declared as

kind list type → type.
type nil list A.
type :: A → (list A) → (list A).,

kind nat type.
type zero nat.
type succ nat → nat.
type add (tuple nat nat) → nat → o.

add (M : zero) M .

add (M : succ N ) (succ Y ) ← add (M : N ) Y .

Figure 9: The implementation of Peano natural numbers in λProlog.

where nil denotes the empty list and ‘::’ denotes ‘cons’. The λProlog predicate for list concatenation is append and the basic Ruby relations can now be implemented as shown in Figure 10.

We represent the Ruby primitives of parallel composition and converse by the respective predicates

type par (A → B → o) → (C → D → o) → (tuple A C ) → (tuple B D) → o.
type conv (A → B → o) → B → A → o.
par R S (A : C ) (B : D) ← R A B, S C D.
conv R B A ← R A B.

Several syntactic points are illustrated in this example. We can see from the type declarations of par and conv that they are both higher-order predicates taking other predicates as arguments. Predicates in λProlog may be defined as “infix” and are also curried facilitating substantial notational convenience. For instance, (R par (conv S)) denotes a valid predicate in itself and can be passed as an argument to other higher-order predicates. Therefore, we can construct goals from predicates which take arbitrarily complex relations as arguments.

The conspicuous absence of the definition of sequential composition is deliberate for a technical reason which we now spend a moment to resolve. The implementation of Ruby we present here unfortunately depends critically on the use of an extra-logical predicate flex which determines whether or not a logical variable is instantiated. The reason for using this predicate—a higher-order analogy to the predicate var found in Prolog [CM87]—is to overcome a standard problem encountered in most logic programming languages, as explained in Section 4.3.

This problem particularly affects an implementation of Ruby in λProlog since we desire the ability to run queries “in reverse,” i.e., solving for logical variables in either the range or domain positions of a relation. By doing so, we satisfy the requirement that each relation in Ruby has a well defined converse. However, the fundamental Ruby primitive of sequential composition is directly affected by this problem. To see why, consider a naïve, infix implementation of sequential composition in λProlog:

type comp′ (A → B → o) → (B → C → o) → A → C → o.

type id  A → A → o.
type swap (tuple A B) → (tuple B A) → o.
type outl (tuple A B) → A → o.
type outr (tuple A B) → B → o.
type fork A → (tuple A A) → o.
type lsh (tuple (tuple A B) C ) → (tuple A (tuple B C )) → o.
type rsh (tuple A (tuple B C )) → (tuple (tuple A B) C ) → o.
type app (tuple (list A) (list A)) → (list A) → o.
type apl (tuple A (list A)) → (list A) → o.
type apr (tuple (list A) A) → (list A) → o.
type wrap A → (list A) → o.
type null A → (list B) → o.

id A A. swap (A : B) (B : A). outl (A : B) A. outr (A : B) B. fork A (A : A). lsh ((A : B) : C ) (A : (B : C )). rsh (A : (B : C )) ((A : B) : C ).

apl (A : AS) BS ← append (A :: nil) AS BS.
apr (AS : A) BS ← append AS (A :: nil) BS.
app (A : B) C ← append A B C .

wrap A (A :: nil). null A nil.

Figure 10: The implementation of the most primitive Ruby relations in λProlog.

type comp  (A → B → o) → (B → C → o) → A → C → o.
kind anonymous  type.
type untype  A → anonymous.
type uninstantiated A → o.
type flexible  anonymous → o.
comp R S A C ← uninstantiated A,!, sigma B\ (S B C , R A B).
comp R S A C ← sigma B\ (R A B, S B C ).
uninstantiated A ← flexible (untype A).
flexible (untype A)  ← flex A,!.
flexible (untype (A : B)) ← flexible (untype A), flexible (untype B).
flexible (untype (A :: nil)) ← flexible (untype A).
flexible (untype (A :: AS)) ← flexible (untype A), flexible (untype AS).

Figure 11: The implementation of sequential composition comp in λProlog.

comp′ R S A C ← sigma B\ (R A B, S B C ).

The λProlog primitive ‘sigma’ denotes existential quantification and the operator ‘\’ denotes infix λ-abstraction, providing a way to create predicates. Then the query

?− add comp′ (conv add) A (succ zero : succ zero).,

decomposes into the expression

?− sigma B\ (add A B, add (succ zero : succ zero) B).,

which is exactly the problematic situation we wish to avoid.

The solution is straightforward although admittedly less declarative than one might prefer. In the definition of sequential composition, we check whether the domain parameter is uninstantiated. If it is, we resolve the clauses in the composition in the reverse order to avoid slipping into an infinite computation. This results in a revised implementation of composition, given in Figure 11. The appearance of the cut ‘!’ in the first clause of comp simply avoids the second clause being attempted should the first one fail. Another point to note is that some type obscuring takes place simply to overcome the fact that a Ruby value comprises of either a number, or a tuple or list of numbers. An alternative method for tackling this difficulty would be to attach an explicit type constructor to each Ruby value to differentiate between them.

Now that we have implemented comp, we can easily implement the other Ruby higherorder functions, as illustrated in Figure 12. An attractive aspect of using λProlog to implement Ruby is the ease with which Ruby operators translate into λProlog syntax;

type map (A → B → o) → (list A) → (list B) → o.
type beside ((tuple A B) → (tuple C D) → o) →

((tuple D E) → (tuple F G) → o) →

(tuple A (tuple B E)) → (tuple (tuple C F ) G) → o.

type below ((tuple A B) → (tuple C D) → o) →

((tuple E F ) → (tuple B H ) → o) →

(tuple (tuple A E) F ) → (tuple C (tuple D H )) → o.

type row ((tuple A B) → (tuple C A) → o) →

(tuple A (list B)) → (tuple (list C ) A) → o.

type col  ((tuple A B) → (tuple B C ) → o) →

(tuple (list A) B) → (tuple B (list C )) → o.

type rdl  ((tuple A B) → A → o) → ((tuple A (list B))) → A → o.
type rdr  ((tuple A B) → B → o) → ((tuple (list A) B)) → B → o.
map R A B ← (conv apl) comp (par R (map R)) comp apl A B.
map R A B ← (conv null) comp null A B.
beside R S A B ← rsh comp (fst R) comp lsh comp (snd S) comp rsh A B.
below R S A B ← conv ((conv R) beside (conv S)) A B.
row R A B ← (snd (conv apl)) comp (R beside (row R)) comp (fst apl) A B.
row R A B ← (snd (conv wrap)) comp R comp (fst wrap) A B.
col R A B ← conv (row (conv R)) A B.
rdl R A B ← (row (R comp (conv outr))) comp outr A B.
rdr R A B ← (col (R comp (conv outl))) comp outl A B.

Figure 12: The implementation of Ruby higher-order functions in λProlog. cmp

cmp cmp

cmp cmp cmp

cmp cmp cmp cmp

Figure 13: A possible circuit corresponding to sort.

the higher-order functions translate almost identically from their abstract Ruby definitions to their corresponding implementations in λProlog. Let us now look at a simple example of how to create new Ruby relations in λProlog.

We present a circuit which sorts an arbitrary, non-empty list of natural numbers. We noted earlier that we require the ability to solve logic variables in both the range and domain positions of a relation, so preserving the converse of each Ruby relation. However, the arithmetic primitives of λProlog are unable to support such a flexible computational requirement. As a consequence, we utilise the alternative definition of “Peano” natural numbers introduced earlier in the section.

Two alternative methods for describing the sorting circuit have been given in the past, one by Sheeran and Jones [SJ87] and the other by Hutton [Hut92]. We implement the former presentation in this section. The sorting circuit is illustrated in Figure 13. Each node cmp is a comparison operation—taking tuples to sorted tuples—and we can see from the figure that some kind of reduction is being performed with a column of comparisons. In fact, the reduction is the converse of a reduce right, rdr^{∘}. In Ruby notation, we can define the sorting circuit sort as

sort : list nat → list nat
sort ≡ wrap^{∘} ; wrap
∨ rdr^{∘} (apr^{∘} ; col cmp)^{∘} ; snd wrap^{∘} ; apr.

The translation of this expression into λProlog is shown in Figure 14 including a suitable definition of cmp. We can then query

?− sort (succ succ zero :: zero :: succ succ succ zero :: succ zero :: nil) B.,

type leq nat → nat → o.
type min (tuple nat nat) → nat → o.
type max (tuple nat nat) → nat → o.
type cmp (tuple nat nat) → (tuple nat nat) → o.
type sort (list nat) → (list nat) → o.

leq zero M .

leq (succ M ) (succ N ) ← leq M N .
min (M : N ) M ← leq M N .
min (M : N ) N ← leq N M .
max (M : N ) M ← leq N M .
max (M : N ) N ← leq M N .
cmp A B ← fork comp (min par max) A B.
sort A B ← (conv (rdr (conv ((conv apr) comp (col cmp))))) comp

(snd (conv wrap)) comp apr A B.

sort A B ← (conv wrap) comp wrap A B.

Figure 14: The implementation of sort in λProlog.

type union (A → B → o) → (A → B → o) → A → B → o.
type fold  (tuple B ((tuple A B) → B → o)) → (list A) → B → o.
type lambda (A → B → o) → A → (list B) → o.
union R S A B ← R A B.
union R S A B ← S A B.

fold (C : R) nil C .

fold (C : R) (A :: AS) Y ← sigma B\ (R (A : B) Y , fold (C : R) AS B).
lambda R A BS ← setof B\ (R A B) BS.

Figure 15: The implementation of some more relational operators in λProlog.

to obtain the result B = (zero :: succ zero :: succ succ zero :: succ succ succ zero :: nil). We encounter a more interesting example by solving the converse of sort. The query

?− conv sort (zero :: succ zero :: succ succ zero :: succ succ succ zero :: nil) B.,

computes every permutation of the given list, corresponding to all the lists which, when sorted, result in the given list. The value of the Ruby implementation presented here is not one of circuit synthesis [LP95, Hut92] but rather of the effective demonstration that a relational calculus can be programmed in λProlog.

5.5.2 Implementing more expressive relational operations

The relational operators of Section 2.4 are unable to be expressed as clean, primitive predicates in λProlog. The implementation of the function Λ, for instance, makes use of a built-in λProlog predicate setof : (A → o) → (list A) → o—returning a list of all solutions to its first argument—which is extra-logical, i.e., setof does not have a well-defined logical meaning (since its implementation is non-primitive). However, setof allows us to mimic the behaviour of the function Λ by collecting all solutions to a relation. The fold operator over cons-lists translates simply from its definition, given in Section 2.2, to its λProlog implementation. The above two relations are implemented by the predicates lambda and fold respectively, as shown in Figure 15.

As an example of using these operators, consider the interleave relation, defined in Section 2.2, whose implementation in λProlog is given in Figure 16. We can query

?− interleave ([1, 2, 3] : [4, 5, 6]) YS.,

which produces a list containing all lists formed by interleaving [1, 2, 3] and [4, 5, 6].

The division operator ‘\’ cannot be implemented in λProlog. We would like to express division as the predicate

under R S C A ← pi B\ (R A B ⇒ S C B).,

type interleave (tuple (list A) (list A)) → (list (list A)) → o.
type tease  (list A) → (tuple (list A) (list A)) → o.
type apl  (tuple A (tuple (list A) (list A))) → (tuple (list A) (list A)) → o.
type apr  (tuple A (tuple (list A) (list A))) → (tuple (list A) (list A)) → o.
interleave XS YSS ← lambda (conv tease) XS YSS.
tease (XS : YS) ZS ← fold ((nil : nil) : union apl apr) (XS : YS) ZS.

apl (A : (XS : YS)) ((A :: XS) : YS).

apr (A : (XS : YS)) (XS : (A :: YS)).

Figure 16: The implementation of interleave in λProlog.

where pi represents universal quantification. However, pi is implemented such that the variable B cannot be bound to any variable appearing outside the scope of the universal quantification pi, like the parameters C and A. Our inability to represent division hinders our the implementation of other relational operators as primitives.

6 Depth-First Iterative Deepening

The incompleteness of the unbounded depth-first search strategy employed in logic programming languages hampers a clean, declarative implementation of a relational calculus in such languages. Depth-first search is incomplete because it can plummet into an infinite search path before a proof to a query is discovered. In the implementation of Ruby presented in Section 5.5, we rectified this problem by artificially altering the flow of control in the depth-first search via an extra-logical feature of λProlog.

An alternative way to tackle this problem—without using extra-logical predicates—is to adopt a complete search strategy. A first step towards eradicating the incompleteness of depth-first search is to limit the depth to which the algorithm may investigate, resulting in bounded depth-first search [Kor85]. This depth bound indicates the maximum number of resolution steps that can be performed when trying to prove a goal. Such a strategy exhaustively searches a finite portion of a possibly infinite search space. The problem with a bounded search, however, is immediately clear: at what depth should we stop searching? If the chosen bound is too small then some solutions may be missed. On the other hand, if the bound is too large then we run the risk of performing much unnecessary and expensive computation.

One way to overcome this problem is to search with an increasing depth bound. Firstly, we depth-first search for all solutions to depth one, say. Then we increase the depth bound and search to depth two, and so forth. This search strategy, called depth-first iterative deepening [Kor85], emulates breadth-first search except that previous nodes are not stored; rather, we commence the search again from the beginning every time the depth bound is increased. This might suggest that depth-first iterative deepening is a terribly inefficient method of search. However, considering that the search space increases exponentially from level to level, it becomes apparent that the work involved in reiterating previous searches is less significant when compared to the overall size of the search space. In general, search strategies are compared by considering trade offs in terms of space, time, and the length of solution paths. Of all the exhaustive (or “brute force”) search strategies, depth-first iterative deepening fairs the best on these three criteria, as discussed by Korf [Kor85].

In the next section, we illustrate how to implement depth-first iterative deepening search in λProlog and also point out some of the problems associated with it.

6.1 Implementing Depth-First Iterative Deepening

Extending a Horn clause program to incorporate depth-first iterative deepening transpires to be a simple, mechanical operation as demonstrated by O’Keefe [O’K90]. For each predicate defined in the λProlog program, we systematically add two new parameters: the first being the number of levels (the “depth bound”) we are able to search to and the second being the remaining number of levels until the depth bound is reached after resolution of this predicate. In addition, we also append several trivial clauses to the body of each predicate simply checking that the depth bound has not been exceeded by entering this predicate and recording the changes in level as we resolve the body of the

type add (tuple nat nat) → nat → int → int → o.
type comp (A → B → o) → (B → C → o) → A → C → int → int → o.
type conv (A → B → o) → B → A → int → int → o.
add (M : zero) M D_{in} D_{out} ←

D_{in} > 0, D_{out} is D_{in} − 1.

add (M : succ N ) (succ Y ) D_{in} D_{out} ←

D_{in} > 0, D_{1} is D_{in} − 1, add (M : N ) Y D_{1} D_{out}.

comp R S A C D_{in} D_{out} ←

D_{in} > 0, D_{1} is D_{in} − 1, R A B D_{1} D_{2}, S B C D_{2} D_{out}.

conv R B A D_{in} D_{out} ←

D_{in} > 0, D_{1} is D_{in} − 1, R A B D_{1} D_{out}.

Figure 17: Extending a program to incorporate depth-first iterative deepening in λProlog.

predicate. Explicitly, we translate the predicate

\begin{matrix}p t_{1} … t_{m} & ← \\ G_{1}, …, G_{n}., \end{matrix}

for m, n ≥ 0, into the corresponding predicate

p t_{1} … t_{m} D_{in} D_{out} ←

D_{in} > 0, D_{1} is D_{in} − 1, G_{1} D_{1} D_{2},

⋮ G_{n} D_{n} D_{out}.

which is prepared for execution under depth-first iterative deepening. As an example, we can extend the program of Figure 9 and the relational expressions comp and conv of Section 5.5 to incorporate depth-first iterative deepening as illustrated in Figure 17.

In λProlog, we embody depth-first iterative deepening in the meta-level, higher-order predicate dfid—shown in Figure 18—taking a goal to be solved as its argument. Notice

type dfid (int → int → o) → o.
type dfid′ (int → int → o) → int → int → o.
dfid Goal ← dfid′ Goal 1 1.
dfid′ Goal D Inc ←

Goal D Remaining, Remaining < Inc.

dfid′ Goal D Inc ←

D′ is D + Inc, dfid′ Goal D′ Inc.

Figure 18: Implementing depth-first iterative deepening in λProlog.

from the type signature of dfid that we use currying to avoid specifying the intial depth bound and the increment at the top level. For example, we would query

?− dfid (add (X : Y ) (succ (succ zero))).,

assuming the definition of natural numbers given in Figure 17.

The procedure comprising the heart of depth-first iterative deepening search is dfid′ whose first clause attempts to solve the goal. Since depth-first iterative deepening traverses the search space from the beginning on consecutive searches, the algorithm will successively rediscover those solutions on levels less than the current depth bound. In order to avoid reporting these solutions more than once, we use the value of Remaining, i.e., the number of levels remaining until the depth bound is reached. If this value is less than the number of levels we incremented the depth bound by then we could not possibly have found this solution on a previous iteration and so we report this as a solution. The second clause of dfid′ increments the depth bound and recursively tries to find other proofs for the goal.

6.2 Evaluating Depth-First Iterative Deepening

From the discussions of the previous sections, we can see that depth-first iterative deepening is guaranteed to find all finite proofs for an arbitrary goal query. Our initial interest in depth-first iterative deepening was motivated by the desire to eliminate the use of extralogical features in the λProlog implementation of Ruby. Therefore, we need to examine how this search strategy performs when evaluating relational Ruby expressions.

Recall from Section 5.5 that the query

?− add comp (conv add) (X : Y ) (succ (succ zero)).,  (11)

results in an infinite computation under standard depth-first search. Depth-first iterative deepening, however, does find all solutions to this query but, unfortunately, introduces a new problem of its own: quite simply, depth-first iterative deepening never gives up increasing the depth bound and, hence, does not terminate after finding the last solution.

Therefore, we must determine a method for stopping depth-first iterative deepening once the final proof to a goal query has been discovered. Both O’Keefe [O’K90] and Stickel [Sti88] propose such a method based on estimating the number of resolutions— levels in the search space—required to solve a particular goal. Specifically, when a goal fails as a result of the depth bound being exceeded, the depth bound is simply incremented by the number of clauses remaining to be resolved in the goal (assuming that solving each clause requires at least one resolution step). Stickel suggests that this method is admissible (or correct) since the number of resolutions remaining is never overestimated. Presumably, though, this method only holds for a special, limited class of queries, i.e., those queries which cannot have a proof at level greater than n if they do not have a proof at level n. However, determining a stopping criterion for an arbitrary goal clause must be undecidable since determining the satisfiability of such a clause—whether a clause actually has a solution—is generally not possible, as explained by Lloyd [Llo87].

Even despite this theoretical result, extending the estimator algorithm from a firstto a higher-order setting is complicated by the fact that both O’Keefe and Stickel make essential use of extra-logical features in their respective implementations which are not supported by λProlog. However, we can evaluate the performance of the estimator algorithm by translating the λProlog query, numbered (11) above, into its equivalent Prolog query,

?− add(X , Y , Z ), add(X , Y , succ(succ(zero)).  (12)

Unfortunately, executing query (12) in Prolog using depth-first iterative deepening still results in non-termination suggesting that the stopping criterion is inadequate to support a satisfactory implementation of relations.

7 Categorical Relational Programming

In the previous sections, we saw that existing programming languages are not entirely appropriate for implementing a relational calculus. Furthermore, we saw that both functional logic and higher-order logic programming languages possess complicated computational models hindering our ability to reason effectively about their programs. These factors suggest that an alternative computational strategy be employed for a relational programming language.

A number of suitable mathematical frameworks exist in which we can conceivably evaluate relational expressions. For instance, the category theory of relations, or allegories [FŠč90], provides several alternative methods for computing relational expressions. Broome and Lipton [BL95] propose a computational model based on rewriting relational expressions directly using a set of relational axioms selected from those which define an allegory. This line of work, though, is still under development and it remains to be seen if it is an effective way of computing relational expressions. Another approach, and the one we introduce in the remainder of the section, depends on expressing relations categorically, as tabulations.

Each relation in certain allegories can be factored (tabulated) by two functions composed solely from a small set of categorical combinators. The fundamental relational connectives of union, converse, composition, and intersection are simply functions taking relations to relations and, critically, we are able to interpret these operations categorically in terms of the tabulations of the relations each operator takes as arguments. A relational expression can then be evaluated by first replacing all primitive relations by their corresponding tabulations and then computing the new tabulations formed from the relational connectives. A relational computation, in summary, progresses by constructing new tabulations hierarchically from more primitive ones.

The final tabulation returned as the solution to a computation may, however, consist of a complicated composition of combinators in a quite unreadable form. Therefore, a printing procedure, which simplifies a tabulation by reducing both its components, becomes an integral part of the evaluation mechanism. In what follows, we formalise the connection between logic programming terms and categorical combinators, and introduce the necessary category theory to explain the computational model.

7.1 Terms and Categorical Combinators

Logic and relational programming, though regularly perceived as equivalent programming paradigms, exhibit distinctive stylistic differences in their respective programs: logic programs make extensive use of logical variables to accumulate information and to connect various parts of a program whereas relational programs are built hierarchically from compositions of relations and are variable free. Admittedly, however, logic and relational programming do share similar powers of expression. Indeed, a fundamental link between these paradigms exists which may be presented in category theory. Asperti and Martini [AM89] have shown how to view a logic program categorically and, more recently, Broome and Lipton [BL95] have considered how to transform a logic program into a relational expression which can then be manipulated providing an evaluation process for logic programs. In this section, we look at the relationship between logic and relational programming by illustrating how we can represent logic programming terms as categorical combinators. Such combinator expressions form the components of tabulations.

We begin by defining a logic programming term as

Term ::= x
| f (t_{1}, …, t_{n}).

The term x is a variable denoted by a capital letter, like X . The term f (t_{1}, …, t_{n}) is called a compound term where f is any function symbol and t_{1}, …, t_{n}, for n ≥ 0, are themselves terms. We call a function constant when n = 0 and write it as c rather than c( ). Some example terms, then, are f (X , h(Y )), f (X , Y , Z ), and g(h(c), X ).

The full set of categorical combinators we will use in the remainder of this section is given by the grammar

Poly ::= id : A → A | Poly ; Poly : A → C
| ! : A → 1 | ¡ : 0 → A | α : FA → A
| ⟨Poly, Poly⟩ : A → B × C | outl : A × B → A | outr : A × B → A
| [Poly, Poly] : A + B → C | inl : A → A + B | inr : B → A + B.

The language Poly is called polynomial since it builds arrows from constants, products, and coproducts. We pronounce the arrow ⟨ , ⟩ as “split” and the arrow [ , ] as “join” and each satisfy the usual type restrictions. The letters A, B, and C range over objects of the category and 1 and 0 are the distinguished terminal and initial objects, respectively. The composition p_{1};p_{2} : A → C of two polynomial arrows is defined in the case where p_{1} : A → B and p_{2} : B → C . The polynomial α : FA → A represents initial algebras allowing us to introduce datatypes, as explained in detail by Bird and de Moor [BdM95]. For example, we can define the initial algebra Nat of natural numbers by [zero, succ] : FNat → Nat where the functor F is defined (on types) as FA = 1 + A. For natural numbers, zero : 1 → Nat is the constant representing 0 and succ : Nat → Nat represents the function that increments a natural number by one.

One of the main benefits of representing logic programming terms categorically stems from our ability to replace variables by projections [AM89]. By doing so, we avoid some of the problems associated with variable name clashes and complicated substitution rules although other problems still persist, in particular the “occurs check” problem [Llo87]. It is quite possible, however, that we can determine more elegant solutions to such problems using category theory than exist already. We now show how to translate between logic programming terms and polynomial arrows.

7.1.1 Converting terms to polynomial arrows

Firstly, we determine the set of variables Ω = {X_{1}, …, X_{n}}, for n ≥ 0, contained in a term. The translation function F_{Ω} : Term_{Ω} → Poly is defined by

F_{Ω}(X_{i}) = \{ \begin{matrix}outr^{i−1} ; outl, & if i ≠ n \\ outr^{i−1}, & otherwise \end{matrix}  (13)

F_{Ω}(c) = ! ; c  (14)
F_{Ω}(f (t_{1}, …, t_{m})) = ⟨⟨F_{Ω}(t_{1}), …⟩, F_{Ω}(t_{m})⟩; f .  (15)

By extending the grammar Poly to include a distinguished class of variables, say x : 1 → X such that x ranges over all variable names, we imagine that the variables from the set Ω form the split ⟨X_{1}, ⟨X_{2}, ⟨…, X_{n}⟩⟩⟩ : 1 → A where each individual variable X_{i} is uniquely accessed by the projection F_{Ω}(X_{i}). Notice that a constant c : 1 → A is composed with ‘!’ to correctly type the combinator expression. As an example translation, consider the term f (X , g(Y , h(c))) where Ω = {X , Y }. Then,

F_{Ω}(f (X , g(Y , h(c))))
= {equation (15)}
⟨F_{Ω}(X ), F_{Ω}(g(Y , h(c)))⟩; f
= {equation (13), equation (15)}
⟨outl, ⟨F_{Ω}(Y ), F_{Ω}(h(c))⟩; g⟩; f
= {equation (13), equation (15)}
⟨outl, ⟨outr, F_{Ω}(c) ; h⟩; g⟩; f
= {equation (14)}
⟨outl, ⟨outr,! ; c ; h⟩; g⟩; f .

7.1.2 Converting polynomial arrows to terms

Translating in the reverse direction—from a polynomial arrow to a logic programming term—is equally straightforward. The first step is to replace each projection in a polynomial arrow by a corresponding unique variable name. To perform this task, consider the term p′ = ⟨X_{1}, ⟨X_{2}, ⟨…, X_{n}⟩⟩⟩; p where p is the combinator expression we wish to convert to a term and ⟨X_{1}, ⟨X_{2}, ⟨…, X_{n}⟩⟩⟩ is the categorical representation of the variables contained in Ω. By considering the composition ⟨X_{1}, ⟨X_{2}, ⟨…, X_{n}⟩⟩⟩; p as application, we obtain the arrow p′ in which all projections are replaced by their corresponding variables. The translation function H_{Ω} : Poly_{Ω} → Term is defined by

H_{Ω}(X_{i}) = X_{i}  (16)
H_{Ω}(! ; c) = c  (17)
H_{Ω}(⟨⟨p_{1}, …⟩, p_{m}⟩; f ) = f (H_{Ω}(p_{1}), …, H_{Ω}(p_{m})).  (18)

Therefore, we can translate the term ⟨outl, ⟨outr,! ; c ; h⟩; g⟩; f , where Ω = {X , Y }, by first composing it with the categorical representation of Ω:

⟨X , Y ⟩; ⟨outl, ⟨outr,! ; c ; h⟩; g⟩; f
= {split fusion and products}
⟨X , ⟨Y ,! ; c ; h⟩; g⟩; f .

Notice that projections are absent from the final expression. We continue with the translation via

H_{Ω}(⟨X , ⟨Y ,! ; c ; h⟩; g⟩; f )
= {equation (18)}
f (H_{Ω}(X ), H_{Ω}(⟨Y ,! ; c ; h⟩; g))
= {equation (16), equation (18)}
f (X , g(H_{Ω}(Y ), H_{Ω}(! ; c ; h)))
= {equation (16), equation (18)}
f (X , g(Y , h(H_{Ω}(! ; c))))
= {equation (17)}
f (X , g(Y , h(c))).

Although coproducts do not appear in the above formulation, their use in a relational language is extremely important; coproducts capture the notion of non-determinism by allowing us to return a number of disjoint solutions to a relational expression. Therefore, we can interpret a join as a logic programming term by conceptually applying the function H_{Ω} to each component of the join:

H_{Ω}([p_{1}, p_{2}]) = H_{Ω}(p_{1}) ∨ H_{Ω}(p_{2}),

where the symbol ‘∨’ is a term construct that connects two disjoint terms. This idea will become clear when we consider how to express the union of two relations in Section 7.4.

7.2 Tabulations

Let us introduce the category theory notation we will need in the rest of this section. We say that a pair of functions (f , g), where f : C → A and g : C → B, is a tabulation of a relation R : A → B if R = f^{∘} ; g. The following diagram illustrates the relationship between a relation R and its tabulation (f , g).

C

[figure: f; g]
A  \overline{R  ^{}}B

An allegory in which every arrow has a tabulation is called tabular. In particular, the allegory whose objects are sets and whose arrows are relations is tabular. It is this allegory that we are interested in.

Let us now give a few examples of how we might tabulate some relations. Any function f may be tabulated quite simply by (id, f ). The universal relation Π : A → B can be tabulated by the pair of functions (outl, outr). The following diagram shows why this is the case:

A × B
[figure: outl; outr]
A  B

The tabulation of the relation (add1 × add1^{∘}) : Nat × Nat → Nat × Nat, which takes a pair of natural numbers and adds one to the first component and subtracts one from the second, is shown below.

Nat × Nat
[figure: ⟨outr, outl ; succ⟩]

[figure]

⟨outr ; succ, outl⟩

Nat × Nat  Nat × Nat

We can tabulate primitive relations fairly easily in terms of categorical combinators. Recall that our intention is to express the standard relational operators in terms of tabulations which we can then manipulate. This method requires the existence of certain categorical universal constructions explained next.

7.3 Unification in Category Theory

Functional logic and higher-order logic programming languages use unification as the fundamental element of their computational models. Unifying two terms results in a set of substitutions for the variables of the terms so that the terms become identical after applying the substitutions to each one. Unification can be captured precisely in category theory by computing the equaliser of two arrows, an observation formalised by Goguen [Gog89] and applied by Rydeheard and Burstall [RB88]. In this setting, substitution simply becomes the composition of arrows.

As mentioned at the beginning of the section, the evaluation of a relational expression involves computing new tabulations from existing ones. This process hinges on the ability to determine equalisers of tabulation functions, i.e., polynomial arrows. We develop this method here.

7.3.1 Equalisers

When composed with two arrows of the same source and target, an equaliser, as its name suggests, simply makes the compositions equal providing a categorical analogy to unification. The definition of an equaliser is as follows:

Definition 1 Given a pair of arrows f , g : B → A, an equaliser of f and g is an arrow e : X → B such that

1. e ; f = e ; g, and

2. for all h : C → B such that h ; f = h ; g, there exists a unique arrow k : C → X such that h = k ; e.

An equaliser e of two arrows f and g is illustrated in the following diagram:

[figure: X; e; B; f; g; A]
[figure: h]
C^{k . . . . . .}

7.3.2 Pullbacks

Another useful universal construction is a pullback which generalises an equaliser to two arrows, this time from a common source to different targets. The definition of a pullback is presented next.

Definition 2 Given a pair of arrows f : B → A and g : C → A, the pullback of f and g is a pair of arrows p : D → B and q : D → C such that

1. p ; f = q ; g, and

2. for all h : X → B and k : X → C such that h ; f = k ; g, there exists a unique arrow d : X → D such that h = d ; p and k = d ; q.

The pullback square of the above definition is illustrated by the following diagram:

X

[figure: ^{....}; d; _{....}; k; h]
D \overline{q ^{}}C

[figure: B; p; f; A; g]

We will later make use of the fact that equalisers and pullbacks are equivalent in a category with all finite products and the terminal object formalised by the following lemma:

Lemma 4 The pair of arrows p : D → B and q : D → C is the pullback of the arrows f : B → A and g : C → A if and only if ⟨p, q⟩ : D → B × C is an equaliser of outl ; f and outr ; g.

The proof of this lemma is a simple diagram chase.

7.3.3 Some example equalisers

In order to evaluate relational expressions, we need to construct a calculus for computing equalisers of polynomial arrows which, unfortunately, is a non-trivial task; determining equalisers in the presence of coproducts and arbitrary recursive functions is undecidable in general.

Nevertheless, preliminary results obtained from a prototype calculus indicate that we can realistically expect to discover an algorithm for computing equalisers which performs well in most practical cases, in particular in the absence of recursion. Admittedly, the existing calculus is ad-hoc and no real theoretical results support it for the time being. Indeed, the formalisation of such a calculus remains mysteriously absent from the field of categorical logic programming and determining a mathematically sound calculus is one of the main aims of our current research.

We can expect that a resulting calculus will contain a set of rules, like the following ones, for computing equalisers. For the arrows [f , g], [h, k] : B + C → A, we can reduce the task to equalising the individual components of the join, illustrated by:

[figure: X; e; B; f; h; A; X′; e′; C; g; k; A]

The equaliser of [f , g] and [h, k] is simply e + e′ : X + X′ → B + C .

As another example, the equaliser of the arrows ⟨f , g⟩, ⟨h, k⟩ : A → B ×C is calculated by first determining the equaliser e of f and h. We can then find the equaliser e′ of e ; g and e ; k as shown below.

[figure: X′; e′; X; e; C; g; k; B]

The equaliser of the two splits is given by e′; e : X′ → C . The proof of this fact is simple and is given by Asperti and Martini [AM89].

An example of finding the unifier for two terms should help to clarify the intention of computing equalisers of polynomial arrows. Consider unifying the logic programming terms f (Z , g(X )) and f (h(Y ), g(h(Z ))). In order to translate these two terms into categorical combinators, we first notice that Ω = {X , Y , Z } (since the variables are shared between terms). The categorical representation of Ω is thus ⟨X , ⟨Y , Z ⟩⟩ and we translate the two terms via

F_{Ω}(f (Z , g(X ))) = ⟨outr ; outr, outl ; g⟩; f
F_{Ω}(f (h(Y ), g(h(Z )))) = ⟨outr ; outl ; h, outr ; outr ; h ; g⟩; f .

We can determine the unifier for them by constructing the equaliser e as follows:

X e_{}

(A × B) × C

⟨outr ; outr, outl ; g⟩; f  ^{}
⟨outr ; outl ; h, outr ; outr ; h ; g⟩; f^{}

D

(assuming the existence of a calculus for computing equalisers). In this case, e would be the arrow ⟨h ; h, ⟨id, h⟩⟩ providing the substitutions {⟨X , h(h(Y ))⟩, ⟨Z , h(Y )⟩}.

7.4 The Category Theory of Relations

In the preceding discussion, we introduced the categorical machinery necessary to express relations as tabulations and suggested a method of computing equalisers of polynomial arrows. We now tie all these concepts together to form a proposed evaluation strategy for relational expressions by showing how the the relational operations of composition, converse, intersection, and union may be interpreted in category theory. An evaluation of a relational expression proceeds by replacing primitive relations by their tabulations and computing new tabulations in a manner determined by each relational connective. This transpires to be simple and elegant method of computing relations. We now show how each relational operator can produce a new tabulation from existing ones.

7.4.1 Converse

Let R : A → B be a relation and let (f , g) be its tabulation, where f : R → A and g : R → B, as illustrated below.

R

[figure: f; g]
A  B

We can calculate the converse R^{∘} : B → A simply by “swapping” the tabulation functions around:

R

[figure: g; f]
B  A

Thus, the tabulation of R^{∘} is just (g, f ).

7.4.2 Union

Let R : A → B and S : A → B be two relations and let (f , g) and (h, k) be their respective tabulations, where f : R → A, g : R → B, h : S → A, and k : S → B. We can calculate the union R ∪ S : A → B simply as

R + S

[figure: [f , h]; [g, k]]
A  B

so the tabulation of R ∪ S is then ([f , h], [g, k]).

7.4.3 Composition

Let R : A → B and S : B → C be two relations and let (f , g) and (h, k) be their respective tabulations, where f : R → A, g : R → B, h : S → B, and k : S → C . We can calculate the composition R;S : A → C by constructing the pullback functions p : X → R and q : X → S of g and h as illustrated in the diagram below.

X

[figure: p; q]
R  S
[figure: f; g; h; k]
A  B  C

The new tabulation for R ; S is the pair (p ; f , q ; k).

7.4.4 Intersection

Let R : A → B and S : A → B be two relations and let (f , g) and (h, k) be their respective tabulations, where f : R → A, g : R → B, h : S → A, and k : S → B. We can calculate the intersection R ∩ S : A → B from

X

[figure: p; q]
A ^{_{}h}  S
[figure: ⟨h, k⟩]
A × B
[figure: ⟨f , g⟩]
[figure: R; f; g; B; k]

where p and q are the pullback functions of ⟨f , g⟩ and ⟨h, k⟩. The tabulation for the relation R ∩ S is thus (p ; f , p ; g).

8 Conclusions and Further Work

8.1 Conclusions

The endeavour to create a relational programming language is important for several main reasons. Firstly, the use of relational calculi in program derivation is progressively becoming more widespread [BdM95, ABH^{+}92, Möl92, SS88]. The development and understanding of such calculi, however, suffers from the lack of a relational language in which to execute relational expressions. A second reason for a relational language stems from the desire to integrate the two main declarative programming paradigms of functional and logic programming; a relational language combines elements of both these paradigms. Although many experimental functional logic languages have been developed [Llo95, HS93, KLMR90], the main criticism is that their operational semantics are complex and mathematically inelegant. On the other hand, adequate theory exists [BL95, FŠč90, AM89] to suggest that an elegant computational model for a relational language could be developed to redress the current, unsatisfactory situation. Indeed, it is possible that, during the development of a relational language, insights could be made into the computational strategy of purely logic programming languages.

Moreover, the need to develop a new computational strategy for a relational programming language depends on the inadequacies of evaluation models for existing programming languages rather than on purely aesthetic grounds. For instance, functional programming languages are unsuitable for clear reasons; by representing relations as list-valued functions, the fundamental relational operation of converse becomes difficult to implement since it requires a possibly infinite search space to be traversed. Generally, extending such an implementation to encompass relations that may return infinite lists complicates matters greatly since the obvious definitions of standard relational operators no longer hold.

Functional logic programming languages promise the ability to naturally capture the essential elements of a relational language. Currently, however, the implemented functional logic languages [Llo95, HS93] fall short of satisfying the required criteria for a relational language, particularly from a computational point of view. It remains unclear whether future versions of such languages will address these points.

Perhaps the most suitable languages for implementing a relational calculus are the higher-order logic programming languages, such as λProlog [NM88]. In Section 2.3, a purely relational implementation of Ruby [Jon90] was presented. However, problems were encountered due to the left to right evaluation strategy employed in λProlog, hindering a completely declarative implementation of Ruby since we artificially altered the flow of control in the λProlog program. As a consequence, correctness results for the implementation of Ruby became extremely difficult suggesting that the computational model of λProlog requires some alteration. Indeed, the evaluation problem is prevalent in most logic programming languages and is also evident in the implemented functional logic languages. Additionally, we do not really require the entire generality of λProlog’s computational model to capture a relational calculus. For example, we utilise only the syntactic convenience of currying and higher-order features when programming relations; we make no real use of the full expressiveness of higher-order unification, casting doubt on it as the most appropriate candidate for modeling relational computations.

The alternative computational strategy, proposed in Section 7, exploits the category theory of relations [FŠč90] as its underlying mathematical framework. Each relational expression is translated into a tabulation, the two composite functions of which are comprised solely from a concise set of polynomial categorical combinators. The computation hinges on our ability to express the fundamental relational operations in terms of well understood categorical concepts and on a method of computing equalisers for polynomial combinators. As the situation stands at the moment, a formal calculus to describe equalisers for polynomial arrows is missing as is an evaluation strategy for rewriting relational expressions to some final answer. The solution to both of these questions should prove intriguing and will form the basis of further work.

8.2 Program of Further Work

The project will commence with the implementation of a rudimentary functional programming language based on categorical principles. The language will be implemented by translating functional expressions to categorical combinators using the method presented in Section 7. One of the main questions at this stage is to determine the appropriate notion of reduction for the language. We will primarily develop an understanding of the new theory for the non-recursive case. We would later hope to extend the theory to encompass primitive recursion (folds).

Next, we shall develop an algorithm for computing the equaliser of two first-order functional programs expressed as categorical combinator code. Rydeheard and Burstall [RB88] have given a preliminary algorithm for performing such a task although they do not replace variables by projections. Finding a general algorithm appears to be possible, a fact supported from observations made from an unverified prototype implementation of computing equalisers for (non-recursive) polynomial arrows. Whether an efficient algorithm exists is still an open question; the problem must be NP-hard since, after all, we are essentially determining the equality of two arbitrary functional programs. Despite this, it seems reasonable to expect to find an algorithm that performs well in most practical cases. Pinpointing these limitations exactly is important for developing a concrete mathematical understanding of the algorithm. However, should it transpire that no efficient algorithm may be formulated, several other avenues would be open for exploration, for example, the rewriting strategy of Broome and Lipton [BL95], or investigating a restricted form of higher-order unification [Mil91].

In the third and final stage of the project, we aim to implement relations as spans in the enhanced functional language. That such an implementation is feasible follows from the construction of relations over a finitely complete category [FŠč90]. By this time, the novel implementation of relations will be compared to any available, alternative languages. This comparison will provide definite criterion to judge the success of the project.

If the project is successful, and the work takes less time than anticipated, the equaliser algorithm could be extended to deal with limited higher-order features. It would then also be desirable to pay additional attention to a typing discipline: the operator for computing equalisers cannot be assigned any reasonable type by a static type checker, and so a form of dynamic typing will be required.

Acknowledgements

I would like to extend my sincere thanks to Oege de Moor. I would like to thank Stephen Muggleton for suggesting depth-first iterative deepening as an alternative search strategy and also Luc de Raedt for pointing me toward several implementations of iterative deepening.

References

[ABH^{+}92] C. J. Aarts, R. C. Backhouse, P. Hoogendijk, E. Voermans, and J. C. S. P. Van der Woude. A relational theory of datatypes. Available via anonymous ftp

from ftp.win.tue.nl in directory pub/math.prog.construction, Septem-

ber 1992.

[AM89] A. Asperti and S. Martini. Projections instead of variables: A category theoretic interpretation of logic programs. In G. Levi and M. Martelli, editors, Proceedings of the Sixth International Conference on Logic Programming, pages 337–352. MIT Press, 1989.

[BdM95] R. S. Bird and O. de Moor. The Algebra of Programming. Prentice Hall International, 1995.

[Bir87] R. S. Bird. An introduction to the theory of lists. In M. Broy, editor, Logic of Programming and Calculi of Discrete Design, volume 36 of NATO ASI Series F, pages 3–42. Springer–Verlag, 1987.

[BL86] M. Bellia and G. Levi. The relation between logic and functional languages: a survey. Journal of Logic Programming, 3(3):317–236, 1986.

[BL95] P. Broome and J. Lipton. Combinatory logic programming: Computing in relation calculi. Department of Mathematics, Wesleyan University, CT 06459, USA, 1995.

[Chu40] A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.

[CM87] W. Clocksin and C. Mellish. Programming in Prolog. Springer-Verlag, third edition, 1987.

[FŠč90] P. J. Freyd and A. Ščedrov. Categories, Allegories, volume 39 of Mathematical Library. North–Holland, 1990.

[Gog88] J. A. Goguen. Higher order functions considered unnecessary for higher order programming. Technical report SRI-CSL-88, SRI International, 333 Ravenswood Ave., Menlo Park CA 94025, 1988.

[Gog89] J. A. Goguen. What is unification? In H. Aït-Kaci and M. Nivat, editors, Resolution of Equations in Algebraic Structures, volume 1, chapter 6. Academic Press, 1989.

[Han94] M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19(20):583–628, 1994.

[HS93] M. Hanus and A. Schwab. Alf User’s Manual. Max-Planck-Institut für Informatik, Saarbrücken, Germany, 1993.

[Hue73] G. Huet. The undecidability of unification in third-order logic. Information and Control, 22:257–267, 1973.

[Hue75] G. Huet. A unification algorithm for typed λ-calculus. Theoretical Computer Science, 1(1):27–57, 1975.

[Hut92] G. Hutton. Between Functions and Relations in Calculating Programs. Research report, Department of Computer Science, Glasgow University, 1992.

[Jon90] G. Jones. Designing circuits by calculation. Technical Report PRG–TR– 10–90, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, England, 1990.

[JS90] G. Jones and M. Sheeran. Circuit design in Ruby. In J. Staunstrup, editor, Formal Methods for VLSI Design, pages 13–70. Elsevier Science Publications, 1990.

[JS91a] G. Jones and M. Sheeran. Collecting butterflies. Technical Monograph PRG-91, University of Oxford, Programming Research Group, 1991.

[JS91b] G. Jones and M. Sheeran. Relations and refinement in circuit design. In J. Woodcock and C. Morgan, editors, Third Refinement Workshop, 1990. Springer Workshops in Computing, 1991.

[KLMR90] H. Kuchen, R. Loogen, J. J. Moreno-Navarro, and M. Rodriguez-Artalejo. Graph-based implementation of a functional logic language. In N. Jones, editor, Proceedings of the Third European Symposium on Programming, Copenhagen, volume 432 of Lecture Notes in Computer Science, pages 271–290. Springer–Verlag, 1990.

[Kor85] R. E. Korf. Depth-first iterative deepening: An optimal admissible tree search. Artificial Intelligence, 27(1):97–109, 1985.

[LB94] J. Lipton and P. Broome. Combinatory logic programming. In P. van Hentenryck, editor, Proceedings of the Eleventh International Logic Programming Symposium. MIT Press, 1994.

[LHRB94] S. Le Huitouze, O. Ridoux, and P. Brisset. Prolog/Mali reference manual.

Available via anonymous ftp from ftp://ftp.irisa.fr/local/lande/pm,

1994.

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

[Llo95] J. W. Lloyd. Declarative programming in Escher. Technical Report CSTR-95-013, Department of Computer Science, University of Bristol, June 1995.

[LP95] W. Luk and C. Pitcher. Simulation Facilities in Rebecca. Imperial College of Science, Technology, and Medicine, London, U.K., 1995.

[Mil91] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497– 536, 1991.

[Möl92] B. Möller. Derivation of graph and pointer algorithms. In B. Möller, H. Partsch, and S. Schuman, editors, Formal Program Development, Proceedings of the IFIP TC2/WG2.1 State of the Art Seminar. Springer, 1992.

[NM88] G. Nadathur and D. Miller. An overview of λProlog. In R. Kowalski and K. A. Bowen, editors, Fifth International Logic Programming Conference, pages 810–827, Seattle, U.S.A., 1988. MIT Press.

[NM90] G. Nadathur and D. Miller. Higher-order horn clauses. Journal of the A.C.M., 37(4):777–814, 1990.

[NM95] G. Nadathur and D. Miller. Higher-order logic programming. To appear in Journal of Artificial Intelligence and Logic Programming, 1995.

[O’K90] R. A. O’Keefe. The Craft of Prolog. MIT Press, 1990.

[Pre94] C. Prehofer. Higher-order narrowing. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, pages 507–516. IEEE Computer Society Press, 1994.

[Qia94] Z. Qian. Higher-order equational logic programming. In Proceedings of the 21st ACM Symposium on Principles of Programming Languages, pages 254– 267, Portland, U.S.A., 1994. ACM Press.

[RB88] D. E. Rydeheard and R. M. Burstall. Computational Category Theory. Prentice–Hall, 1988.

[Red87] U. Reddy. Functional logic languages part I. In Proceedings of a Workshop on Graph Reduction, pages 401–425. Lecture Notes in Computer Science 279, Springer-Verlag, 1987.

[SJ87] M. Sheeran and G. Jones. Relations + higher-order functions = hardware descriptions. In W. E. Proebster and H. Reiner, editors, Proceedings of the IEEE Comp Euro 87: VLSI and Computers, pages 303–306, Hamburg, 1987.

[SS88] G. Schmidt and T. Ströhlein. Relationen und Grafen. Springer-Verlag, 1988.

[Sti88] M. E. Stickel. A Prolog technology theorem prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.

[War82] D. Warren. Higher-order extensions to Prolog: Are they needed? Machine Intelligence, 10:441–454, 1982.