PROGRAM SEPARATION AS A BASIS FOR DEFINITIONAL HIGHER ORDER PROGRAMMING

GÖRAN FALKMAN

Abstract. We describe a program separation scheme based on a notion of form and content of an algorithm. We show that this type of program separation is one way of making algorithms an explicit part of declarative programming. We also show how this type of program separation can be used as a basis for definitional higher order programming.

1. Introduction

The basis for all modern declarative programming languages like ML, Haskell, and Prolog is that the programmer should be more concerned with what the program should do and less with how the program should accomplish some task.

The actual algorithms are often rather implicit in such languages since they are hidden under layers of very high-level notions like pattern-matching, unification, and backtracking. So if you want to study algorithms in this context there must be a way of making algorithms a more explicit part of declarative programming without losing to much of the declarative reading of the programs.

Just as higher order functions and meta-programming have been subjects to intensive studies in the functional programming and logic programming community respectively, we are in the area of definitional programming interested in the notions of higher order definitions and definitional higher order programming.

In this paper we describe a program separation scheme based on a notion of form and content of an algorithm. We show that this type of program separation is one way of making algorithms an explicit part of declarative programming. We also show how this type of program separation can be used as a basis for definitional higher order programming.

Key words and phrases. Programming methodology, definitional programming, program separation.

This work was supported by the Swedish Research Council for Engineering Sciences (TFR) and the Swedish National Board for Industrial and Technical Development (NUTEK).

It is part of the work done within the ESPRIT working group GENTZEN

The work presented here is based on some earlier work on program separation [5].

As an introductory example, consider the recursive definition of addition:

P \{ \begin{matrix}plus(0, m) & = & m, \\ plus(s(n), m) & = & s(plus(n, m)). \end{matrix}

The intended algorithm associated with this definition is given implicitly in proving that plus(n, m) = n + m with respect to P. By induction: If n = 0, then the definiens of plus(n, m), P(plus(n, m)), is m and thus in this case plus(n, m) = n + m. So assume plus(n, m) = n + m with respect to P. Now P(plus(s(n), m)) = s(plus(n, m)), so by the induction hypothesis plus(s(n), m) = s(n) + m. The algorithm may be formulated as follows:

(1) if n = 0, then take the definiens of plus(n, m) in P, P(plus(n, m)), as the result of the computation of plus(n, m),

(2) if n = s(k), then the result of the computation of plus(n, m) is given by computing plus(k, m) and then applying s to the result.

In this algorithm we really only use primitive operations on definitions; looking up the definiens of an expression and checking whether a given expression is defined or not. So we may reformulate the algorithm in the following manner:

P lus(x) = \begin{cases}P_{1}(x) & if P_{1}(x) ∩ Dom(P_{1}) = ∅, \\ P_{2}(P lus(P_{1}(x))) & if P_{1}(x) ∩ Dom(P_{1}) ≠ ∅. \end{cases}

where P_{1} and P_{2} are the following definitions:

P_{1} \{ \begin{matrix}plus(0, m) & = & m, \\ plus(s(n), m) & = & plus(n, m). \end{matrix}

P_{2} { n = s(n)

P_{1} and P_{2} is the canonical separation of P in order to find definitions such that addition is locally definable, i.e., to isolate the local operations needed to compute additions on the basis of P. P lus then describes the global structure of the algorithm.

It is natural to think of this type of program separation as a separation of form and content. P lus gives the recursive form of the algorithm and P_{1} and P_{2} give the particular content needed to compute addition.

The rest of this paper is organized as follows. In Section 2 we give a short introduction to the target language. In Section 3 we introduce a notion of form and content of an algorithm by studying a couple of examples.

2. Programming with definitions

The target language of this paper is based on an existing definitional programming language called GCLA^{1} [1, 2, 3, 4, 7].

Compared to GCLA we use an idealized syntax and, what is more important, we have extended the language by allowing multiple object-level definitions and more general guards and provisos. We use the same operational semantics as in GCLA.

2.1. Basic building blocks. The basic building blocks of the language are variables, constants, terms, atoms, and conditions.

2.1.1. Variables. Variables are denoted by strings with a capital initial letter, e.g., “X”, “Xs”, “A long variable” etc.

2.1.2. Constants. Constants are denoted by strings beginning with a lowercase letter, e.g., “x”, “aConstant” etc.

2.1.3. Terms. Terms are built up using variables and constants:

(i) All variables are terms, (ii) All constants are terms, (iii) If f is a functor and T_{1}, …, T_{n} are terms, then f(T_{1}, …, T_{n}) is a term.

2.1.4. Atoms. Atoms are terms which are not variables:

(i) All constants are atoms, (ii) If f is a functor and T_{1}, …, T_{n} are terms, then f(T_{1}, …, T_{n}) is an atom.

2.1.5. Conditions. Conditions are built up using, ⊥, ⊤, and terms: (i) ⊥ is condition. (Falsity), (ii) ⊤ is a condition. (Truth), (iii) All terms are conditions, (iv) If C_{1} and C_{2} are conditions, then C_{1} → C_{2} is a condition,

(v) If C_{1} and C_{2} are conditions, then C_{1} ; C_{2} is a condition, (vi) If C_{1} and C_{2} are conditions, then C_{1} , C_{2} is a condition.

2.2. Definitions and programs. Definitions are built up by definitional clauses and using definitions we form programs.

2.2.1. Definitional clauses. If a is an atom and C is a condition, then a = C is a definitional clause.

A is referred to as the head of the clause and C is referred to as the body of the clause.

We may also have guarded definitional clauses. If a is an atom, C is a condition, and G_{1}, …, G_{n} are guards, i.e., simple syntactical equality and inequality constraints on variables like “X = Y ”, “f(Y) ≠ f(g(Z))”, “W ⩾ 1” etc., then a#{G_{1} ∧ ⋯ ∧ G_{n}} = C is a guarded definitional clause.

1Is to be pronounced “Gisela”.

2.2.2. Definitions. A definition D is an ordered set of (guarded) definitional clauses:

D { a = A. ; b = B. ; c = C. ; d = D. ; ⋮

Definitions will be denoted by D_{1}, D_{2}, D_{3}, …

2.2.3. Programs. A program P, is a set of definitions, P = {D_{1}, …, D_{n}} for n > 1.

2.3. The meaning of a program. A program P is a set of definitions. In the definitions we define atoms in terms of certain conditions, but these conditions are not defined in the definitions themselves. Instead we select one of the definitions in P to interpret all the conditions in the other definitions. This definition will be called the rule definition (or the meta-level definition) and it will be denoted by R. The definitions in P \ {R} are referred to as the objectlevel definitions (or simply the definitions). We continue to denote object-level definitions by D_{1}, D_{2}, D_{3}, …

The difference between the object-level definitions and the rule definition is that in the latter we have access to some primitive operations on definitions which are used in the communication between the rule definition and the objectlevel definitions.

The purpose of R is to give meaning to the conditions that are used in the object-level definitions. To give this meaning we define inference rules that interpret all the different object-level conditions. We also define search strategies that guide the search among the inference rules.

When defining inference rules and search strategies we use the conditions defined in Section 2.1.5. Rather than having a “meta-meta-level definition” interpreting these conditions the meaning of the conditions used in R is given by a sequent calculus, DOLD, which is the same calculus that gives the operational semantics of GCLA [7].

Thus a program P consists of R and at least one object-level definition, and an interpretation of P is obtained only by putting the object-level definitions in the context of R.

2.3.1. Inference rules. An inference rule (or simply a rule) interprets one of the object-level conditions. The general form of an inference rule is:

Rule(P T_{1}, …, P T_{n}) = P_{1}, …, P_{k},

(P T_{1} → Seq_{1}), …, (P T_{n} → Seq_{n}) → Seq. where

• P T_{1}, …, P T_{n} are proof terms, i.e., partially instantiated functional expressions representing the proofs of the premises, Seq_{i},

• P_{1}, …, P_{k} are provisos, i.e., side conditions on the applicability of the rule. k may be equal to 0,

• Seq and Seq_{1}, …, Seq_{n} are sequents on the form Γ ⊢ C where Γ is a finite set of conditions and C is a condition. Intuitively Γ ⊢ C could be read as: “C follows from Γ.”

One way to read this is: “If P_{1}, …, P_{k} hold and P T_{1} proves Seq_{1}, …, and P T_{n} proves Seq_{n}, then Rule(P T_{1}, …, P T_{n}) proves Seq.”

2.3.2. Search strategies. A search strategy (or simply a strategy) guides the search among the inference rules. A strategy has the following general form:

\begin{aligned}Strategy & = & (P_{1} → Seq_{1}), …, (P_{n} → Seq_{n}). \\ Strategy & = & P T_{1}, …, P T_{m}. \end{aligned}

where • P T_{1}, …, P T_{m} are proof terms,

• P_{1}, …, P_{n}, for n ⩾ 0, are provisos,

• Seq_{1}, …, Seq_{n}, for n ⩾ 0, are sequents. You can read a strategy as: “If P_{1} holds and some P T_{i}, 1 ⩽ i ⩽ m, proves

Seq_{1}, then Strategy proves Seq_{1}, …, or if P_{n} holds and some P T_{i}, 1 ⩽ i ⩽ m, proves Seq_{n}, then Strategy proves Seq_{n}.”

2.3.3. Provisos. A proviso is a condition on the applicability of a rule or a strategy. Intuitively you can think of a proviso as a black box performing some operation that has to succeed in order for the rule or strategy to succeed. Some provisos may have side-effects like adding constraints to variables or generating substitutions.

Some of the provisos are used in the communication between R and the object-level definitions. These provisos are built up using a set of primitive operations on definitions which are entirely justified by the interpretation of the object-level definitions as definitions.

The most important of these primitive operations are:

• D(a) which gives the definiens of the term a in the definition D. In short, D(a) is the maximal set of all bodies of clauses in D whose heads are unifiable with each other and with a, i.e., D(a) = {A | a = A ∈ D}. There can be more than one definiens for a term a. The reader is referred to [7] for a formal definition of D(a) and to [2] for details on the computational aspects of D(a),

• Dom(D) which gives the domain of a definition D, i.e., Dom(D) = {a | ∃A(a = A ∈ D)},

• unify(A, B) which is used to unify the object-level terms A and B.

Using the operations above we can for example construct a proviso for testing whether something is in the domain of a certain definition, i.e., “a ∈ Dom(D)”.

2.4. Queries. If Seq is a sequent on the form Γ ⊢ C and S is a (meta-level) condition then S ⊩ Seq. is a query.

We may interpret a query as asking for an object-level substitution σ such that Sϕ proves Γσ ⊢ Cσ for some meta-level substitution ϕ.

3. Program separation

3.1. A notion of form and content. In this section we are going to introduce a notion of form and content of an algorithm. We will do this by studying an example. This will lead us to a definition of an abstract recursive form of a class of very simple recursive algorithms.

3.1.1. A motivating example. As an example we study the canonical definition for finding the last element of a list.

Example 3.1.1. Consider the following recursive definition for finding the last element of a list:

L \{ \begin{matrix}last((x: : nil)) & = & x, \\ last((x: : xs)) & = & last(xs) if xs ≠ nil. \end{matrix}

where nil denotes the empty list and : : is the cons operator.

The intended algorithm associated with this definition can be described as follows:

(1) if l = (x: : nil), then take the definiens of last(l) in L, L(last(l)), as the result of the computation of last(l),

(2) if l = (x: : xs), where xs ≠ nil, then the result of the computation of last(l) is given by computing last(xs).

Now, what we want to do is to separate, so to speak, the (recursive) form, or the global structure, of the algorithm from the particular content needed to compute last.

To find the particular content needed to compute last we try to separate L into definitions such that the operation of finding the last element of list is locally definable, i.e., we try to isolate the local operations needed to compute last on the basis of L.

Intuitively locally defined means that all operations needed to compute the result from an argument are present in the definitions but global information, like which local operation to be performed and when, are not [6].

In the case of last, it turns out that we do not need to separate L any further; whenever we reach something on the form last((x: : nil)) in the computation of last, the next thing to do is to return x, and whenever we find something on the form last((x: : xs)) the next step is to compute last(xs). But this is precisely what L says, so last is already locally defined in L.

To extract the recursive form of the algorithm we study the computation of last((1 : :(2 : :(3 : : nil)))). We see that all we have to do to compute last((1 : :(2 : :(3 : : nil)))) is to look up the definiens of last((1 : :(2 : :(3 : : nil)))) in L and recursively compute L(last((1 : :(2 : :(3 : : nil))))), i.e., last((2 : :(3 : : nil))). The recursion stops when we find an expression that is not defined in L, i.e., an element.

So in the computation of last((1 : :(2 : :(3 : : nil)))) we really only use primitive operations on definitions; looking up the definiens of an expression and checking whether a given expression is defined or not.

We may therefore reformulate the algorithm in the following manner:

Last(x) = \begin{cases}L(x) & if L(x) ⊈ Dom(L), \\ Last(L(x)) & if L(x) ⊆ Dom(L). \end{cases}  (1)

We may read (1) as: “If L(x), the definiens of x in L, is not defined in L (the base case), then take L(x) as the result of the computation of Last(x). Else if L(x) is defined in L (the recursive case), then the result of the computation of Last(x) is given by recursively computing Last(L(x)).”

It is natural to think of this type of separation as a separation of form and content. We say that (1) gives the (recursive) form of the algorithm whereas L gives the particular content needed to compute last.

The natural way to implement a separated algorithm, as the one above for computing last, is to define the content as object-level definitions and to define the form by strategies and rules in the rule definition.

In the case of last, the implementation of L is straightforward:

D_{1} \{ \begin{matrix}last([X]) & = & X. \\ last([X|Xs])#\{Xs ≠ []\} & = & last(Xs). \end{matrix}

R consists of a rule with two clauses corresponding to the two cases of (1):

R \{ \begin{matrix}f(1) & = & (D_{1}(X) ⊈ Dom(D_{1})), \\ & & unify(D_{1}(X), F) → (X ⊢ F). \\ f(2) & = & (D_{1}(X) ⊆ Dom(D_{1})), \\ & & (f( ) → (D_{1}(X) ⊢ F)) → (X ⊢ F). \end{matrix}  (2)

A typical query would then be:

f( ) ⊩ last([1, 2, 3, 4, 5]) ⊢ X.

which has the solution X = 5.

3.1.2. An abstract recursive form. In the definition of (1) in Example 3.1.1, we did not use any information about the particular definition at hand. Thus it should be possible to describe the recursive form of the algorithm for finding the last element of a list without referring to any specific definition.

We get the following generalization of (1):

F (x) = \begin{cases}D(x) & if D(x) ⊈ Dom(D), \\ F (D(x)) & if D(x) ⊆ Dom(D). \end{cases}  (3)

where D is some definition.

In contrast to (1), (3) does not describe the recursive form of a specific algorithm but the abstract recursive form of a class of algorithms.

Further examples of algorithms belonging to this class are the canonical definitions of enumerating the members of a list, enumerating the members of a binary tree, deciding whether an element is a member of a list or not, generating suffixes of a list, returning the element with index i from a list, and others.

Exactly what constitutes this class remains an open question.

We also generalize (2) in the same way:

R \{ \begin{matrix}f(1, D) & = & (D(X) ⊈ Dom(D)), \\ & & unify(D(X), F) → (X ⊢ F). \\ f(2, D) & = & (D(X) ⊆ Dom(D)), \\ & & (f( , D) → (D(X) ⊢ F)) \\ & & → (X ⊢ F). \end{matrix}  (4)

The rule f is now parameterized with a definition and since f itself is a definition, this is a kind of definitional higher order programming.

To find the last element in the list [1, 2, 3, 4, 5] we would now pose the query:

f( , D_{1}) ⊩ last([1, 2, 3, 4, 5]) ⊢ X.

where D_{1} is the same definition as in Example 3.1.1.

3.2. Splitting and collecting. In many algorithms, a splitting and collecting part can be discerned. In the splitting part the computation is split up into several sub-computations and in the collecting part the results from these subcomputations are collected together to form the final result.

In some of these algorithms, the result of the collecting part is the result of the whole computation while in others some additional computing is needed in order to get the final result.

In this section we are going to study the abstract recursive forms of very simple recursive algorithms which can be described in terms of a splitting and collecting part.

As we will see these forms are natural extensions of the abstract recursive form given by (3) in Section 3.1.2.

3.2.1. Algorithms that build structures. Algorithms that build some kind of a data structure are very common. As an example of such an algorithm we study the canonical algorithm for appending two lists.

Example 3.2.1. Consider the following recursive definition for appending two lists:

A \{ \begin{matrix}append(nil, ys) & = & ys, \\ append((x: : xs), ys) & = & (x: : append(xs, ys)). \end{matrix}

The algorithm normally associated with this definition can be described as follows:

(1) if xs = nil, then take the definiens of append(xs, ys) in A as the result of the computation of append(xs, ys),

(2) if xs = (z: : zs), then the result of the computation of append(xs, ys) is given by computing append(zs, ys) and then applying : : to z and the result.

The algorithm described above is really implicit in A since there is nothing in A that indicates that we must first look inside (x: : append(xs, ys)) to compute append(xs, ys) and then apply : : to x and the result. What we like to do is to make the algorithm a more explicit part of A.

We do this by applying the program separation scheme outlined in Section 3.1, i.e., we try to separate the recursive form of the algorithm from the particular content needed to compute append.

One way to find the particular content needed to compute append is to separate A into the following definitions:

A_{1} \{ \begin{matrix}append(nil, ys) & = & ys, \\ append((x: : xs), ys) & = & x, \\ append((x: : xs), ys) & = & append(xs, ys). \end{matrix}

A_{2} \{ \begin{matrix}x & = & (x: : xs) if x ≠ nil ∧ x ≠ (y: : ys), \\ xs & = & (x: : xs) if xs = nil ∨ xs = (y: : ys). \end{matrix}

The intuition behind A_{1} is that whenever we reach something on the form append(nil, ys) in the computation of append then we return ys and whenever we find something on the form append((x: : xs), ys) the computation is split up into two sub-computations: x and append(xs, ys).

Similarly, the intuition behind A_{2} is that whenever we reach something that is not a list, i.e., an element, then we construct a list from that element and some list xs and whenever we find something that is a list then we construct a new list from that list and some element x. A_{2} can be seen as the reverse of the inductive definition of lists of a given type.

To find the recursive form of the algorithm we notice that to compute for example append((1 : :(2 : : nil)), (3 : : nil)) all we have to do is to look up the definiens of append((1 : :(2 : : nil)), (3 : : nil)) in A_{1} and continue with the subcomputations 1 and append((2 : : nil), (3 : : nil)). Now we should put 1 in front of a list, namely the list we get by appending (3 : : nil) to (2 : : nil), and we can do that by simply looking up the definiens of 1 in A_{2}. When the recursive computation of append((2 : : nil), (3 : : nil)) eventually returns, we should put an element, i.e., 1, in front of the resulting list and we can do that by simply looking up the definiens of the resulting list in A_{2}. The recursion stops when we find something that is not defined in A_{1}, i.e., an element.

So in the computation of append((1 : :(2 : : nil)), (3 : : nil)) we really only use primitive operations on definitions and we may therefore formulate the algorithm as follows:

Append(x) = \begin{cases}A_{1}(x) & if A_{1}(x) ∩ Dom(A_{1}) = ∅, \\ A_{2}(Append(A_{1}(x))) & if A_{1}(x) ∩ Dom(A_{1}) ≠ ∅. \end{cases}  (5)

We say that (5) gives the recursive form of the algorithm whereas A_{1} and A_{2} together give the particular content needed to compute append.

A_{1} and A_{2} are implemented by two object-level definitions:

D_{3} \{ \begin{matrix}append([], Y s) & = & Y s. \\ append([X|Xs], Y s) & = & X. \\ append([X|Xs], Y s) & = & append(Xs, Y s). \end{matrix}

D_{4} \{ \begin{matrix}X#\{X ≠ [] ∧ X ≠ [Y |Y s]\} & = & [X|Xs]. \\ Xs#\{Xs = [] ∨ Xs = [Y |Y s]\} & = & [X|Xs]. \end{matrix}

The form (5) is implemented by the following rule definition:

R \{ \begin{matrix}f(1) & = & (D_{3}(X) ∩ Dom(D_{3}) = ∅), \\ & & unify(D_{3}(X), F) → (X ⊢ F). \\ f(2) & = & (D_{3}(X) ∩ Dom(D_{3}) ≠ ∅), \\ & & (\{A_{1}, …, A_{n}\} = D_{3}(X)), \\ & & (g( ) → (A_{1} ⊢ F)), …, (g( ) → (A_{n} ⊢ F)) → (X ⊢ F). \\ g(1) & = & (X ∉ Dom(D_{3})), \\ & & unify(D_{4}(X), F) → (X ⊢ F). \\ g(2) & = & (X ∈ Dom(D_{3})), \\ & & (f( ) → (X ⊢ F X)), \\ & & unify(D_{4}(F X), F) → (X ⊢ F). \end{matrix} (6)

The first clause of the rule f corresponds to the base case. If the definiens of an expression consists of more than one member we evaluate all the members to the same value. This is to ensure that the two lists created from the element and the recursive call respectively are equal. This is taken care of in the second clause of f. Thus, it is in this rule that the collecting is performed.

The two clauses of the rule g correspond to the second case in (5).

To concatenate the lists [1, 2] and [3, 4] we pose the query:

f( ) ⊩ append([1, 2], [3, 4]) ⊢ X.

which has the solution X = [1, 2, 3, 4].

What happens in the algorithm given by (5) above is that we use D_{3} to present values and recursive calls and then use D_{4} to build a structure based on the number of recursive calls.

3.2.2. Computing in the collecting part. So far we have only considered examples where the collecting part consists of building a structure on basis of a given datatype. In this section we consider a simple example where we actually compute in the collecting part.

Example 3.2.2. Consider the following (naive) recursive definition for reversing a list:

R \{ \begin{matrix}reverse(nil) & = & nil, \\ reverse((x: : xs)) & = & append(reverse(xs), (x: : nil)). \end{matrix}

where append is the operation of appending two lists.

The intended algorithm associated with this definition can be described as follows:

(1) if xs = nil, then take the definiens of reverse(xs) in R, R(reverse(xs)), as the result of the computation of reverse(xs),

(2) if xs = (y: : ys), then the result of the computation of reverse(xs) is given by computing reverse(ys) and then appending (x: : nil) to the result.

In order to make the above algorithm a more explicit part of R we try to separate R into definitions such that reverse is locally definable. One way to do this is to separate R into the following definitions:

R_{1} \{ \begin{matrix}reverse(nil) & = & nil, \\ reverse((x: : xs)) & = & x, \\ reverse((x: : xs)) & = & reverse(xs). \end{matrix}

R_{2} \{ \begin{matrix}x & = & append(xs, (x: : nil)) & if x ≠ nil ∧ x ≠ (y: : ys), \\ xs & = & append(xs, ys) & if xs = nil ∨ xs = (y: : ys). \end{matrix}

We can understand R_{1} as: “If we reach something on the form reverse(nil) in the computation of reverse then we return nil and if we find something on the form reverse((x: : xs)) the computation is split up into two computations: x and reverse(xs).”

Similarly, we can understand R_{2} as: “If we reach something that is not a list, i.e., an element, then we construct an append structure from some list xs and the list consisting of that element, and if we find something that is a list then we construct an append structure from that list and another list ys.”

It is easy to see that the recursive form of this algorithm must be very similar to (5); in both cases we use the two results from the recursive step to build a data structure. The important difference is that in the case of reversing a list the data structure is intermediate—it is not the final result of the computation— we need to do some additional computing on the structure, i.e., evaluating the append structure to a list.

We get the following recursive form of the algorithm:

Rev(x) = \begin{cases}R_{1}(x) & if R_{1}(x) ∩ Dom(R_{1}) = ∅, \\ Append(R_{2}(Rev(R_{1}(x)))) & if R_{1}(x) ∩ Dom(R_{1}) ≠ ∅. \end{cases} (7)

where Append is the algorithm for appending two lists.

Perhaps to gain some additional intuition of what this program separation is all about, one may think of the content of the algorithm as the part of the algorithm that defines on which objects the next step of the algorithm should act upon, and the form of the algorithm as the part that defines what exactly is the next step of the algorithm.

If we translate this algorithm into a program, R_{1} and R_{2} are implemented by the following two object-level definitions:

D_{5} \{ \begin{matrix}reverse([]) & = & []. \\ reverse([X|Xs]) & = & X. \\ reverse([X|Xs]) & = & reverse(Xs). \end{matrix}

D_{6} \{ \begin{matrix}X#\{X ≠ [] ∧ X ≠ [Y |Y s]\} & = & append(Xs, [X]). \\ Xs#\{Xs = [] ∨ Xs = [Y |Y s]\} & = & append(Xs, Y s). \end{matrix}

The form (7) is implemented by the following rule definition:

R \{ \begin{matrix}f(1) & = & (D_{5}(X) ∩ Dom(D_{5}) = ∅), \\ & & unify(D_{5}(X), F) → (X ⊢ F). \\ f(2) & = & (D_{5}(X) ∩ Dom(D_{5}) ≠ ∅), \\ & & (\{A_{1}, …, A_{n}\} = D_{5}(X)), \\ & & (g( ) → (A_{1} ⊢ F X)), …, (g( ) → (A_{n} ⊢ F X)), \\ & & (append → (F X ⊢ F)) → (X ⊢ F). \\ g(1) & = & (X ∉ Dom(D_{5})), \\ & & unify(D_{6}(X), F) → (X ⊢ F). \\ g(2) & = & (X ∈ Dom(D_{5})), \\ & & (f( ) → (X ⊢ F X)), \\ & & unify(D_{6}(F X), F) → (X ⊢ F). \end{matrix}  (8)

where append is some strategy or rule defined elsewhere for appending two lists, e.g., the rule f in (6).

This rule definition is essentially the same as (6) but with the important difference that we use an external strategy (or rule) append in the second clause of f for evaluating the intermediate append structure built by g to a list.

If we would like to reverse the list [1, 2, 3, 4, 5] we can pose a query like:

f( ) ⊩ reverse([1, 2, 3, 4, 5]) ⊢ X.

which has the solution X = [5, 4, 3, 2, 1].

3.2.3. Abstract recursive forms. In the definitions of (5) and (7) in Example 3.2.1 and Example 3.2.2 respectively, we did not use any information about the particular definitions at hand. So it should be possible to describe the recursive form of the algorithms for computing append and reverse without referring to any specific definition.

Consider the following generalization of (5):

F (x) = \begin{cases}D_{1}(x) & if D_{1}(x) ∩ Dom(D_{1}) = ∅, \\ D_{2}(F (D_{1}(x))) & if D_{1}(x) ∩ Dom(D_{1}) ≠ ∅. \end{cases}  (9)

where D_{1} and D_{2} are some definitions.

Just like (3) in Section 3.1.2, (9) describes the abstract recursive form of a class of algorithms. Further examples of algorithms belonging to this class are the canonical definitions of finding the maximum and minimum of two natural numbers, computing the length of a list, substituting one element for another in a list, duplicating all the members in a list etc.

We also generalize the rule definition in Example 3.2.1 in the same way:

R \{ \begin{matrix}f(1, D_{1}, D_{2}) & = & (D_{1}(X) ∩ Dom(D_{1}) = ∅), \\ & & unify(D_{1}(X), F) → (X ⊢ F). \\ f(2, D_{1}, D_{2}) & = & (D_{1}(X) ∩ Dom(D_{1}) ≠ ∅), \\ & & (\{A_{1}, …, A_{n}\} = D_{1}(X)), \\ & & (g( , D_{1}, D_{2}) → (A_{1} ⊢ F)), \\ & & …, \\ & & (g( , D_{1}, D_{2}) → (A_{n} ⊢ F)) \\ & & → (X ⊢ F). \\ g(1, D_{1}, D_{2}) & = & (X ∉ Dom(D_{1})), \\ & & unify(D_{2}(X), F) → (X ⊢ F). \\ g(2, D_{1}, D_{2}) & = & (X ∈ Dom(D_{1})), \\ & & (f( , D_{1}, D_{2}) → (X ⊢ F X)), \\ & & unify(D_{2}(F X), F) → (X ⊢ F). \end{matrix}  (10)

The rules f and g are now a kind of higher order definitions since they are parameterized with two definitions D_{1} and D_{2}.

To concatenate the two lists [1, 2] and [3, 4] we would now pose the query:

f( , D_{3}, D_{4}) ⊩ append([1, 2], [3, 4]) ⊢ X.

where D_{3} and D_{4} are the same definitions as in Example 3.2.1.

Similarly we get the following generalization of (7):

F (x) = \begin{cases}D_{1}(x) & if D_{1}(x) ∩ Dom(D_{1}) = ∅, \\ G(D_{2}(F (D_{1}(x)))) & if D_{1}(x) ∩ Dom(D_{1}) ≠ ∅. \end{cases}  (11)

where D_{1} and D_{2} are some definitions and G is some function defined elsewhere.

The form (11) describes the abstract recursive form of a class of algorithms. Further examples of algorithms belonging to this class are the canonical definitions of flattening a list, computing the factorial of a natural number, computing the fibonacci-numbers, computing the sum and product of all the members in a list of natural numbers, listing a binary tree in pre-, in-, and post-order checking if a binary tree is full etc.

We also generalize the rule definition in Example 3.2.2 in the same way:

R \{ \begin{matrix}f(1, D_{1}, D_{2}, P T) & = & (D_{1}(X) ∩ Dom(D_{1}) = ∅), \\ & & unify(D_{1}(X), F) \\ & & → (X ⊢ F). \\ f(2, D_{1}, D_{2}, P T) & = & (D_{1}(X) ∩ Dom(D_{1}) ≠ ∅), \\ & & (\{A_{1}, …, A_{n}\} = D_{1}(X)), \\ & & (g( , D_{1}, D_{2}, P T) → (A_{1} ⊢ F X)), \\ & & …, \\ & & (g( , D_{1}, D_{2}, P T) → (A_{n} ⊢ F X)), \\ & & (P T → (F X ⊢ F)) \\ & & → (X ⊢ F). \\ g(1, D_{1}, D_{2}, P T) & = & (X ∉ Dom(D_{1})), \\ & & unify(D_{2}(X), F) \\ & & → (X ⊢ F). \\ g(2, D_{1}, D_{2}, P T) & = & (X ∈ Dom(D_{1})), \\ & & (f( , D_{1}, D_{2}, P T) → (X ⊢ F X)), \\ & & unify(D_{2}(F X), F) \\ & & → (X ⊢ F). \end{matrix}  (12)

Since the definitions f and g are parameterized with two definitions, D_{1} and D_{2}, this is yet another example of how this type of program separation can be used as a basis for definitional higher order programming.

To reverse the list [1, 2, 3, 4, 5] we pose the query:

f( , D_{5}, D_{6}, append) ⊩ reverse([1, 2, 3, 4, 5]) ⊢ X.

where D_{5} and D_{6} are the same definitions as in Example 3.2.2 and append is some strategy or rule defined elsewhere for appending two lists, e.g., the rule f in (6).

References

1. M. Aronsson, GCLA user’s manual, Research Report T91:21A, SICS, 1991.

2. , GCLA, the design, use, and implementation of a program development system, Ph.D. thesis, Department of Computer and Systems Sciences, University of Stockholm, 1993.

3. M. Aronsson, L-H. Eriksson, A. Gäredal, L. Hallnäs, and P. Olin, The programming language GCLA—a definitional approach to logic programming, New Generation Computing 7 (1990), no. 4, 381–404.

4. M. Aronsson, P. Kreuger, L. Hallnäs, and L-H. Eriksson, A survey of GCLA—a definitional approach to logic programming, Extensions of Logic Programming, Proceedings of the 1st International Workshop held at the SNS, Universität Tübingen, 1989 (P. Shroeder-Heister, ed.), Springer Lecture Notes in Artificial Intelligence, vol. 475, Springer-Verlag, 1990.

5. G. Falkman, L. Hallnäs, and O. Torgersson, Program separation in GCLA, Proceedings of the Post-Conference Workshop on Proof-Theoretical Extensions of Logic Programming, Santa Margherita Ligure, Italy, 18 June 1994 (A. Momigliano and M. Ornaghi, eds.), June 1994, pp. 31–37.

6. L. Hallnäs, WM94: program separation in GCLA, Proceedings of La Wintermöte ’94, Lundsbrunn, January 18–20, January 1994, pp. 93–94.

7. P. Kreuger, GCLA II, a definitional approach to control, Extensions of Logic Programming, Proceedings of the 2nd International Workshop held at SICS, Sweden, 1991 (L-H. Eriksson, L. Hallnäs, and P. Shroeder-Heister, eds.), Springer Lecture Notes in Artificial Intelligence, vol. 596, Springer-Verlag, 1992, pp. 239–297.

Department of Computing Science, Chalmers University of Technology, S-412 96 Göteborg, Sweden

E-mail address: falkman@cs.chalmers.se