MAX-PLANCK-INSTITUT FÜR

INFORMATIK

An Abstract Program Generation Logic

David A. Plaisted

MPI–I–94–232 July 1994

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Authors’ Addresses

David Plaisted Max-Planck-Institut für Informatik Im Stadtwald D-66123 Saarbrücken Germany

plaisted@mpi-sb.mpg.de

or

Department of Computer Science CB# 3175, 352 Sitterson Hall University of North Carolina at Chapel Hill Chapel Hill, North Carolina 27599-3175 USA

plaisted@cs.unc.edu

Acknowledgements

The comments of David Basin were very helpful in motivating the section on goal-directed program generation and the section on generating programs in specific languages (such as term-rewriting programs). This work was done while the author was on sabbatical and leave of absence at the Max Planck Institute in Saarbrücken, Germany. This work was partially supported by UNC Chapel Hill and by the National Science Foundation under grant number CCR-9108904.

Abstract

We present a system for representing programs as proofs, which combines features of classical and constructive logic. We present the syntax, semantics, and inference rules of the system, and establish soundness and consistency. The system is based on an unspecified underlying logic possessing certain properties. We show how proofs in this system can be systematically converted to programs in a class of abstract logic programming languages including term-rewriting systems and Horn clause logic programs. A number of examples of such logic programming languages and underlying logics are given, as well as some proofs that can be expressed in this system and the corresponding programs.

1 Introduction

We present a programming (meta-)logic P L which is an enrichment of an underlying logic L. This logic, like others, represents programs as proofs, and programs satisfying a certain specification can be extracted from a proof. If the proof is correct, the extracted program is guaranteed to be correct with respect to the specification. Our emphasis is not on automatically constructing programs using a theorem prover, but on representing them in as abstract a manner as possible to facilitate their reuse in different settings. This seems to be of practical importance and also more feasible than automatic program derivation, given the current state of automated reasoning. As hypotheses correspond to subroutines, a proof from a lemma corresponds to an abstract data type that can be instantiated later to obtain a concrete program. However, the system can also be used for (presumably interactive) program generation, and we develop this possibility too. The heart of the system is a systematic method for reasoning about recursion, composition, and fixpoints in an unspecified logic. Although fairly simple, it still may be useful in bringing out and clarifying the connections between different systems, and may be useful for applications. Also, this simplicity has pedagogical advantages. Furthermore, because of the fundamental nature of recursion, composition, and fixpoints, the logic can be considered as another logic of computation. An enriched model of computation (with interleaving or fairness, for example) would require an extension to the inference rules.

The main problem we are trying to deal with is the reuse of programs. Why is it that we have to write the same programs over and over again for different applications, whether a sorting program or a unification program or whatever? The answer may be in part that the algorithms are not represented in an abstract enough manner, and that inessential details obscure the essentials of the algorithm. One goal of the present system is to find an abstract representation for algorithms that will permit them to be used in a variety of settings, without having to be recoded each time. For this purpose, some general methods of combining and instantiating general algorithms for specific applications are mentioned. We note that the techniques presented for this combination of algorithms permit the use of classical logic as opposed to some kind of constructive logic as the main deductive mechanism; this means that the deduction used is often simpler than that in a constructive logic (or, in any case, different).

The logic P L is distinguished from others by its separation between the classical and computational aspects of the logic, and also by its independence from the underlying logic. The extended logic P L introduces new program-construction variables into the underlying logic L and some constructive inference rules for these variables. However, no requirements of constructiveness are imposed on the underlying logic. Furthermore, it only imposes weak demands on the structure of the underlying logic; essentially, first-order logic with a sort structure can be used for many applications. The logic P L does not specify a particular syntax for the programming language. In addition, the logic permits considerable freedom in the underlying computational mechanism, whether deterministic or nondeterministic, functional or relational, terminating or non-terminating and so on. Thus the system is to a large degree independent of the syntax and semantics of the programming language and also from the underlying logic L. In this way we obtain a program generation logic with a high degree of abstractness. This flexibility makes it easy to tailor the logic for specific applications. This also allows for the possibility of translations between different such logics, and we discuss this possibility.

The general idea of the system is to prove statements of the form (∃P)A(P) where P is a program and A is a property it should satisfy. However, we are interested in constructing modules from which programs can be constructed; thus the statement is rather (∃F)A(F) where F is a “program constructing function,” that is, a function mapping from programs to programs. Given programs that implement certain desired operations, F returns a program that satisfies the top-level specification. Thus we might have a statement of the form (∃F)(∀P_{1} … P_{n})(A_{1}(P_{1}) ∧ … ∧ A_{n}(P_{n}) ⊃ A(F (P_{1} … P_{n})) where A_{i} are the specifications of the subprograms P_{i} and A is the specification of F (P_{1}, …, P_{n}). Given procedures P_{i} satisfying the specifications A_{i}, F returns a program F (P_{1}, …, P_{n}) satisfying the specification A. Also, F is required to be constructible. However, in the place of the formula A_{1}(P_{1}) ∧ … ∧ A_{n}(P_{n}) ⊃ A(F (P_{1} … P_{n})) we allow an arbitrary formula B(P_{1}, …, P_{n}, F (P_{1}, …, P_{n})) mentioning P_{1}, …, P_{n}, and F. We can approximately express this as (∀P_{1} … P_{n})(∃P)B(P_{1}, …, P_{n}, P), which is similar in form to the specifications used by other program generation systems. The quantifier (∃P) is required to be constructive, in a sense made precise by the semantics. However, the difference is that P_{1} … P_{n} and P are considered as programs, not inputs and outputs to a program. Though not much different formally from considering P_{1}, …, P_{n} and P as inputs and outputs to a program, this difference in point of view has a number of significant consequences. For example, reasoning at the level of programs in this way makes the generation of recursions and fixpoints very natural. We represent this formula (∀P_{1} … P_{n})(∃P)B(P_{1}, …, P_{n}, P) using the syntax [P_{1} … P_{n} → P]B(P_{1}, …, P_{n}, P) where P_{1}, …, P_{n} and P are variables representing programs and [P_{1} … P_{n} → P] is a new kind of quantifier. The semantics of this requires that P be constructible from P_{1} … P_{n}, in a sense made precise by the logic. This syntax allows us to generate programs without explicitly mentioning F, and permits a significant expressive power within a first-order-like system.

The rules of inference of the system consist of several kinds: 1. Those that influence F; these correspond to compositions of programs, recursions, and fixpoint operations, and these are required to be constructive in a certain sense. 2. Those that only influence the specification A, but do not affect F; these need not be constructive. 3. Those that permit an interaction between F and the underlying logic; these for example permit one of the P_{i} or P to be replaced by an existentially or universally quantified variable in the underlying logic, or permit a quantified variable in the underlying logic to be replaced by a program variable P_{i} or P. In this way we obtain a combination of constructive and classical operations, and the constructive operations have a simple semantic justification in terms of the operations on F to which they correspond.

The organization of this paper is as follows. First we present the syntax and semantics of the logic, give a set of inference rules for it, and argue for their soundness. Next we present two general proof transformations analogous to the deduction theorem in the propositional calculus. Then we show how proofs in the system may be translated into programs, and also give some mappings between proofs formalized with respect to different underlying logics. We give a number of derived inference rules which facilitate program construction in this system. We discuss the use of derived inference rules for obtaining more efficient programs, and also for facilitating goal-directed program generation. We present a general method for translating proofs in this system into logic programming languages satisfying certain general properties; this includes Horn-clause logic programming and term-rewriting systems as special cases. We illustrate the application of the method to several different underlying logics, too. We show how the system can reason about termination and nontermination, and present some specific algorithms and give their derivations. Finally we comment about higher-order properties of the system and some possible extensions to higher-order reasoning.

We now make some comments about other approaches to program generation. The constructive type theory approaches of [24], Nuprl [5], or the calculus of constructions [12] identify the proof that a term has a type with the proof that a term satisfies a specification. From such a proof, a term (program) in the typed or untyped lambda calculus satisfying the specification can be extracted. Such systems involve constructive higher-order logic and typically synthesize programs from constructive proofs of formula of the form (∀x)[P (x) ⊃ (∃y)R(x, y)], where P is the input assertion and R is the input-output relation. This approach is based on the Curry-Howard isomorphism [20] and the propositions-as-types principle; the latter identifies logical propositions with types whose inhabitants are proofs of the proposition. This approach leads to the synthesis of total functions, although there are some ways to extend this to partial functions. A number of implementations of this idea have been done, including Nuprl [11], Oyster and CLAM [8], and Coq [14].

In [27], a computational interpretation of classical natural deduction is discussed, in which lambda terms may be extracted from proofs; this investigation is continued in [28]. For other papers dealing with computational interpretations of classical logic see [19], [15], [25], and [26]. These systems typically supply a computational interpretation to all classical proofs; in contrast, our system uses classical logic for the part of the proof that does not affect the computation at all.

As for logics dealing with fixed points, we can mention the logic for computable functions of Milner [17]. In [10] a system is given whereby high-level specifications involving least and greatest fixpoints can automatically be transformed into efficient programs. Extensions of Nuprl and the Calculus of Constructions to fixpoints and possibly to nonterminating computations are given, respectively, in [31] and [2].

An early approach to program synthesis is that of [18], who used a resolution theorem prover to derive programs satisfying a specification. It is also possible to synthesize a program by applying a set of transformation rules to a specification. One example of early work in this direction is the deductive synthesis approach of [6]. Another early idea was that of [16], whereby the information contained in a proof can be used to specialize a program to a smaller class of inputs. The TABLOG system of Manna and Waldinger [23] also permits a program to be derived from a specification of the desired input-output behavior. This system is largely firstorder (and classical) but with induction rules and rules for specialized theories built in; it uses non-clausal theorem proving in order to facilitate the induction proofs. The Isabelle system [29] permits metalogics to be formalized; it uses a fragment of higher-order intuitionistic logic with higher-order metavariables to formalize the rules of various logics. The Isabelle system can be used to formalize a number of program generation systems [21, 3, 4]. It might also be possible to formalize the present system in Isabelle. In addition to these, there are many other program generation systems which are also based on the idea of proofs as programs or extracting programs from proofs.

2 Syntax

We now return to a discussion of our logic P L and the underlying logic L. The underlying logic is assumed to be some extension of sorted first-order logic. The syntax of the programming logic P L is the syntax of the underlying logic, enriched with individual variables called program variables. Some of the sorts of the underlying logic are specified as program sorts. Program variables can be of one of the program sorts. These program variables may be individual variables, function or predicate variables, or possibly variables of the lambda calculus, depending on the logic. These variables are intended to represent programs. We use upper case letters (X, Y) for sequences of program variables or individual program variables and lower case (x, y) for variables of the underlying logic. We use lower case letters f, g, h for functions in the underlying logic, letters A, B, C for formulas in the underlying logic, and s, t, u for terms. We note that there is no requirement about which arguments of programs are inputs and which are outputs, or even if they have inputs or outputs; if some convention about inputs and outputs is followed, then the recursion rule and the functional composition rules need to be consistent with this convention.

If X and Y are sequences of program variables, we call [X → Y] a program constructor quantifier. We allow formulas of the form [X → Y]A where A is a formula of the underlying logic and X, Y are (possibly empty) sequences of program variables and A does not contain any occurrences of the quantifier [ … → …]. We can regard A (without occurrences of →) as [→]A. We require X and Y to be disjoint in the quantifier [X → Y].

By (∀X)A we mean a sequence of universal quantifications, and similarly for (∃X)A.

3 Semantics

We assume that the underlying logic L is interpreted with respect to a nonempty collection of structures, each having a possibly infinite collection of sorts and a corresponding list D_{1} … D_{n} … of domains and specifying interpretations of the nonlogical symbols as predicates and functions on these domains. Recall that some of the sorts are specified as program sorts. The domains corresponding to the program sorts are called program domains. We require that the program domains be non-empty. We extend these structures for the underlying logic to structures for our programming logic P L. This is done by extending the structures to also specify a domain P C of program construction functions. We sometimes refer to P C as a sort, and it may have subsorts. We require that the program construction functions have specified arities, that is, the sorts (program domains) of the arguments and result are specified. The program construction functions F map elements X_{1} … X_{n} in specified program domains to an element F (X_{1} … X_{n}) in some specified program domain. Also, we require the following:

1. The projection functions p_{i} defined by p_{i}(X_{1} … X_{n}) = X_{i} are program construction functions.

2. The composition of program construction functions is a program construction function. That is, if F_{i}(X_{1} … X_{m}) are in PC and G is in P C then G(F_{1}(X_{1} … X_{m}), …, F_{n}(X_{1} … X_{m})) is in P C (if the sorts are consistent). (This is to some extent a consequence of property 3, as shown below.) Also, this composition should be constructible.

3. The program construction functions have fixpoints that are also program construction functions. That is, let F_{1}(X, Y) … F_{n}(X, Y) be a tuple of program constructing functions, where X and Y are lists of program variables and X has n elements. Suppose that the sorts of F_{i}(X, Y) and X_{i} are the same, for 1 ≤ i ≤ n. Then there is tuple G_{1} … G_{n} of program constructing functions such that for all Y, F_{i}(G_{1}(Y), … G_{n}(Y), Y) = G_{i}(Y), for 1 ≤ i ≤ n. We can write this as F (G(Y), Y) = G(Y), allowing F and G to refer to tuples of program construction functions. We don’t require G to be a least fixpoint here, just some fixpoint. Also, we require that some such fixpoint G be constructible from F_{1} … F_{n}.

For example, we might have F_{1}(X_{1}, X_{2}, Y) and F_{2}(X_{1}, X_{2}, Y) in P C. Then the fixpoint property would require that there exist functions G_{1}(Y) and G_{2}(Y) in P C such that F_{1}(G_{1}(Y), G_{2}(Y), Y) = G_{1}(Y) and F_{2}(G_{1}(Y), G_{2}(Y), Y) = G_{2}(Y).

Writing F and G for pairs of functions, we have F (G(Y), Y) = G(Y). We can obtain composition from the fixpoint property as follows: Let H_{1} and H_{2} be arbitrary unary elements of PC, and let F (X, Y, Z) be (H_{1}(X), H_{2}(Y)). (Formally, F_{1}(X, Y, Z) = H_{1}(X) and F_{2}(X, Y, Z) = H_{2}(Y); tuples are not really needed here. However, we do need to be able to compose with projection functions to express F_{1} and F_{2}.) Then F has a fixpoint G, that is, F (X, G(X)) = G(X). Letting G(X) be (G_{1}(X), G_{2}(X)), we obtain that F (X, G_{1}(X), G_{2}(X)) = (G_{1}(X), G_{2}(X)) = (H_{1}(X), H_{2}(G_{1}(X))) so G_{1}(X) = H_{1}(X) and G_{2}(X) = H_{2}(G_{1}(X)) = H_{2}(H_{1}(X)). Thus G(X) = (H_{1}(X), H_{2}(H_{1}(X))) and we can compute the composition H_{2} ∗ H_{1} of H_{2} and H_{1}. Similar techniques yield fully general compositions; for this it suffices to take H_{1} and F_{1} as sequences of m functions and X as a sequence of n program variables and H_{2} of arity m. Thus G_{1} is a sequence of m functions, F and G are sequences of m + 1 functions, H_{2} ∗ H_{1}(X) is H_{2}(H_{11}(X), …, H_{1m}(X)), and we can compute a general composition.

We use F, G, H for program constructing functions and also later on for program variables. We call a structure satisfying the above three properties, a programming structure. In order to show soundness of the logic, it is necessary that the formulas of P L be interpreted relative to a set of structures in which the above properties hold. We note that for recursive functions, fixpoints as in 3 exist by the recursion theorem. The requirement of constructibility is difficult to test or even understand in a general context as above. We will make this more concrete in our discussion of the generation of programs in specific languages.

We interpret a formula [X → Y]A[X, Y] where |X| = m and |Y | = n as follows: There exists in P C a tuple of n program construction functions F_{1} … F_{n} with m arguments such that for all X in the respective program domains, A[X, F_{1}(X), …, F_{n}(X)]. We can express this as the following formula in P L, where we add variables F_{i} of sort P C (or its subsorts): (∃F_{1} … F_{n} ∈ P C)(∀X)A[X, F_{1}(X), … F_{n}(X)]. However, we note that this formula does not fully express the semantics. Not only do we require that the F_{i} exist, but the proof of this must be constructive. Thus we have a mixture of classical and constructive logic, with the constructive part restricted to the program constructing functions. Note also that we do not prove constructively the existence of outputs to a program. Nor do we prove constructively the existence of a program. Rather, we prove constructively the existence of the program constructing functions F_{i}. The reason is that we want to develop a set of building blocks that can frequently be reused and combined to form desired programs. The program constructing functions are such building blocks, because they map programs to programs, and by specifying their (program) arguments they can be instantiated to obtain particular programs having specified properties.

Our system can be applied to domains in which least fixpoints may not exist, or may be difficult to express, or for which the proper concept of a least fixpoint may be obscure. However, domains in which fixpoints and least fixpoints exist typically may be expressed as complete partial orders. That is, there is a partial ordering <_{d} defined on each sort of program construction function and an element ⊥ such that ⊥ ≤_{d} x for all x. Also, if x_{1}, x_{2}, x_{3}, … is a sequence with x_{1} ≤_{d} x_{2} ≤_{d} x_{3} … then the least upper bound ⨆_{i} x_{i} exists. A function f is monotone if x ≤_{d} y implies f(x) ≤_{d} f(y) and continuous if for all monotone sequences x_{1}, x_{2}, x_{3}, … we have that f(⨆_{i} x_{i}) = ⨆_{i} f(x_{i}). It turns out that computable functions typically correspond to continuous functions on a domain, and so we can take P C to be the set of continuous functions in the appropriate domains. All continuous functions are monotone, and the composition of continuous functions is continuous. We can extend the ordering to functions by f ≤_{d} g if for all x, f(x) ≤_{d} g(x). A value x is a fixed point of f if f(x) = x. It is known that continuous functions f have the least fixed point ⨆_{i} f^{i}(⊥). For functions f(x_{1}, …, x_{n}) with more than one argument, we say they are continous if f(⨆_{i} x_{1i}, …, ⨆_{i} x_{ni}) = ⨆_{i} f(x_{1i}, …, x_{ni}). In this case, we can take fixpoints with respect to one of the arguments. For example, to find a least y such that f(x, y) = y (or more precisely, a least function g(x) such that for all x, f(x, g(x)) = g(x)), we can take g(x) = ⨆_{i}(λy.f(x, y))^{i}(⊥). Such a function g will also be continuous. This can be generalized to more than one function and more than one argument. A domain is called flat if x <_{d} y implies x = ⊥. A function f is said to be strict if f( …, ⊥, …) = ⊥. The intuition is that if x <_{d} y then x is “less defined” than y; ⊥ is the totally undefined element, in the sense that nothing is known about its value. It is customary therefore to let ⊥ represent a nonterminating computation that returns no information.

It may be that the original semantics is not given in terms of programming structures. For example, programs may be interpreted as character strings and an evaluation function may be used to extract their behavior. In this case, the fixpoint property will not directly hold, since typically the fixpoint property applies to the semantics of a program and not to its syntax. However, we can change the semantics so that the meaning (interpretation) of a program is its behavior. That is, if a program P appears only in the context f_{eval}(P, x_{1}, …, x_{n}) where f_{eval} is some kind of evaluation function, then P can be interpreted as the function from x_{1} … x_{n} to f_{eval}(P, x_{1} … x_{n}). In this modified semantics, the fixpoint property may hold.

4 Inference Rules

As usual, we can rename bound variables subject to capture. Also, duplicates in X and Y can be eliminated, and variables in X and Y can be permuted. The functional composition rules and the least fixpoint rules may be included or omitted, depending on the underlying logic.

\frac{[X, U → Y, Z]A[X, U, Y, Z]}{[X → Y, Z]A[X, Y, Y, Z]} (Recursion rule)

where U and Y have the same sort.

For functional programming:

(Functional composition rule 1)

[F_{1} … F_{m} → G](∀z_{1} … z_{n})G(z_{1} …, z_{n}) = T (F_{1}, …, F_{m}, z_{1}, …, z_{n})

assuming that the program variables F_{i} and G are of functional type, where T is a well-formed term involving only the variables z_{i} and applications of function variables F_{i} to appropriate numbers and sorts of arguments.

(Functional composition rule 2)

[P, F_{1} … F_{m} → Q](∀z_{1} … z_{n})(Q(z_{1} … z_{n}) ≡ P (F_{1}(z_{1} … z_{n}), …, F_{n}(z_{1} … z_{n})))

Here P is a program variable that is a predicate in the underlying logic and the F_{i} are function variables.

(Least fixpoint rule, where assumed)

\frac{[X, U → Y, Z]A[X, U, Y, Z] (∀XU)(∃!Y)(∃Z)A[X, U, Y, Z]}{[X → Y, Z](A[X, Y, Y, Z] ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)}

Here ∃! means “There exists unique” and <_{d} is a domain ordering.

(Underlying logic rule)

\frac{[X → Y]A}{[X → Y]B} if ⊢ (∀X, Y)(A ⊃ B) in the underlying logic L

We note that this derivation in the underlying logic need not be constructive.

\frac{[X, Y →]A}{[Y →](∀X)A} (Left elimination rule)

\frac{[X → Y, Z]A}{[X → Y](∃Z)A} (Right elimination rule)

This rule can be used to eliminate excess output variables.

\frac{[X → Y](∀Z)A}{[Z, X → Y]A} (Left introduction rule; Z, Y must be disjoint)

This rule can be used to add excess input variables.

\frac{[X → Y](∀Z)A}{[X → Y, Z]A} (Right introduction rule; Z, X must be disjoint)

This rule is valid since at least one Z is computable. This rule can be used to add excess output variables.

\frac{[X → Y]A [X → Z]B}{[X → Y, Z](A ∧ B)} (Conjunction rule; if no captures and Y, Z are disjoint)

We illustrate recursion as follows: Suppose X and Y have the same type. Then the formula [X → Y, Z]A[X, Y, Z] represents a method of obtaining programs Y and Z from X. We then have the following derivation:

1. [X → Y, Z] A[X, Y, Z] (given)
2. [→ Y, Z]  A[Y, Y, Z] (1, recursion rule)

The conclusion represents a program that has the input X and the output Y the same. We can think of this as replacing the input programs X by a recursive call to the program-constructing operation implicit in 1. We will illustrate this below with a derivation of the (recursive) factorial function using an application of the recursion rule.

We also have a stronger version of the fixpoint rule which only guarantees the existence of a least fixpoint for input programs X and U such that Y is unique, in the formula A[X, U, Y, Z]:

\frac{[X, U → Y, Z]A[X, U, Y, Z]}{[X → Y, Z](A[X, Y, Y, Z] ∧ (∀Y′)((∀W)(∃Z′)A[X, Y′, W, Z′] ≡ (W = Y′)) ⊃ (Y ≤_{d} Y′))}

4.1 Derived Rules

We give some example proofs in this system.

1. [X, W → Y]  A[X, W, Y]
2. [X, W → Y]  (∀ Z)A[X, W, Y] where Z does not appear in A

(by the underlying logic rule)

3. [X, W → Y, Z] A[X, W, Y]  (right introduction)

(Z disjoint with W and X)

4. [W → Y, Z]  A[Z, W, Y]  (recursion rule)
5. [W → Y, X]  A[X, W, Y]  (renaming rule) (X, W disjoint)

The intuition is that in 5, X are specific programs and Y are programs obtained from them using the mapping of 1. Thus we get the derived inference rule

\frac{[X, W → Y]A}{[W → X, Y]A} (W, X disjoint)

Here is a proof of another derived rule:

1. [X, W → Y]  A(X, Y)
2. [X, W → Y]  (∀Z)A(X, Y) (underlying logic rule)

where the sorts of X an Z are the same

3. [X, W → Y, Z] A(X, Y)  (right introduction rule)

(Z disjoint from X and W)

4. [W → Y, Z] A(Z, Y) (recursion rule on X and Z)
5. [W → Y]  (∃Z)A(Z, Y) (right elimination)
6. [W → Y]  (∃X)A(X, Y) (renaming)

Thus we obtain the rule

\frac{[X, W → Y]A(X, Y)}{[W → Y](∃X)A(X, Y)}

which allows input variables to be replaced by existentially quantified variables. We now show how unnecessary input variables can be eliminated:

1. [X, Y → Z] A[X, Z]  where Y do not appear in A
2. [X → Y]  (∃W)A[X, Z] (using the above derived rule)
3. [X → Y]  A[X, Z]  (underlying logic rule)

Thus we have the derived inference rule

\frac{[X, Y → Z]A[X, Z]}{[X → Y]A[X, Z]}

where Y do not appear in A. We show how separate program forming operations can be combined “in parallel”. Assume (W,Y), (Z,X), and (Y,Z) are disjoint.

1. [X → Y]  A[X, Y]  given
2. [W → Z]  B[W, Z]  given
3. [X → Y]  (∀W)A[X, Y]  (1, underlying logic rule)
4. [W → Z]  (∀X)B[W, Z]  (2, underlying logic rule)
5. [X, W → Y]  A[X, Y]  (3, left introduction rule)

(Y,W disjoint)

6, [X, W → Z] B[W, Z] (4, left introduction rule)

(Z,X disjoint)

7. [X, W → Y, Z] (A[X, Y] ∧ B[W, Z]) (5,6, conjunction rule)

(Y,Z disjoint)

Thus we obtain the following inference rule:

\frac{[X → Y]A [W → Z]B}{[X, W → Y, Z](A ∧ B)} (if no captures and Y, Z are disjoint and W, Y and Z, X are disjoint)

We call this the combination rule. We now illustrate a kind of program composition.

1. [X → Y]  A[X, Y]  (given)
2. [Y → Z]  B[Y, Z]  (given) (note that Y,Z are disjoint)
3. [V → Z]  B[V, Z]  (renaming, 2) (so that V,Z disjoint)
4. [X, V → Y, Z] A[X, Y] ∧ B[V, Z]  (combination rule)

(Y,Z and X,Z and V,Y disjoint)

5. [X → Y, Z] A[X, Y] ∧ B[Y, Z] (recursion rule)
6. [X → Z]  (∃Y)A[X, Y] ∧ B[Y, Z] (right elimination rule)

In this way we derive the following rule:

\frac{[X → Y]A [Y → Z]B}{[X → Z](∃Y)A ∧ B} (assuming X, Z disjoint)

We call this the program composition rule. We would like to have the following more general rule too:

\frac{[X → Y]A [Y, W → Z]B}{[X, W → Z](∃Y)A ∧ B} (assuming X, Z and W, Y disjoint)

For this purpose we modify the above proof as follows:

1. [X → Y]  A[X, Y]  (given)
2. [Y, W → Z]  B[Y, W, Z]  (given)

(note that Y, Z and W, Z are disjoint)

3. [V, W → Z] B[V, W, Z] (renaming, 2)

(so that V, Z are disjoint)

4. [X, V, W → Y, Z] A[X, Y] ∧ B[V, W, Z]  (combination rule)

(Y, Z and X, Z and V, Y and W, Y disjoint)

5. [X, W → Y, Z] A[X, Y] ∧ B[Y, W, Z] (recursion rule)
6. [X, W → Z]  (∃Y)A[X, Y] ∧ B[Y, W, Z] (right elimination rule)

We now derive a kind of converse of the conjunction rule:

1. [X → Y, Z] (A ∧ B)  (assumed)
2. [X → Y]  (∃Z)(A ∧ B) (right elimination)
3. [X → Y]  A ∧ (∃Z)B  (underlying logic rule, assuming Z does not occur in A)
4. [X → Y]  A  (underlying logic rule)

Thus we obtain the following derived rule:

\frac{[X → Y, Z](A ∧ B)}{[X → Y]A} (assuming Z does not occur in A)

This permits us to separate out individual program constructing functions. The following rule (identifying inputs) is sometimes convenient. Assuming the identity is computable (which follows from the first functional composition rule), we have

1. [X → Y]  (Y = X)
2. [X → Z]  (Z = X)
3. [X → Y, Z] (Y = X ∧ Z = X)  (1,2, conjunction rule)
4. [Y, Z → W] A(Y, Z, W)  (assumption)
5. [X → W]  (∃Y, Z)(Y = X ∧ Z = X ∧ A(Y, Z, W)) (3,4, composition rule)
6. [X → W]  A(X, X, W)  (5, underlying logic rule)

Thus we derive the rule

\frac{[Y, Z → W]A(Y, Z, W)}{[X → W]A(X, X, W)}

which permits us to make two input variables equal. We now derive another version of the functional composition rule:

\frac{[→ H](H_{1} = k_{1} ∧ … ∧ H_{n} = k_{n})}{[F → G](∀z_{1} … z_{n})G(z_{1}, …, z_{n}) = T (F, k, z_{1}, …, z_{n})}

assuming that the program variables F and G are of functional type, where T is a well-formed term involving only the variables z_{i} and applications of function variables F_{i} and k_{j} to appropriate numbers and sorts of arguments, where F is (F_{1} … F_{m}) and H is (H_{1} … H_{n}) and k is (k_{1} … k_{n}). We call this the functional composition rule with individual functions. The intention is that the k_{i} are known individual function symbols in the underlying logic and they are also known to be computable. Then we are allowed to use these function symbols in the functional composition rule. The proof is as follows, letting Z abbreviate z_{1} … z_{n} and H = k abbreviate H_{1} = k_{1} ∧ … ∧ H_{n} = k_{n}:

1. [F, H → G] (∀z)G(z) = T (F, H, z)  (first functional composition rule)
2. [→ H] (H = k) (assumption)
3. [F → G]  (∃H)(H = k ∧ (∀z)G(z) = T (F, H, z)) (program composition rule,1,2)
4. [F → G]  (∀z)G(z) = T (F, k, z)  (3, underlying logic rule)

We now show how the functional composition rule can be extended to allow recursion, with abbreviations as above and G a sequence of program variables and T a sequence of terms:

\frac{[→ H](H = k)}{[F → G](∀z)G(z) = T (F, k, G, z)}

where T is a sequence of well-formed terms involving the function symbols appearing in the sequences F,k, and G. Since G is defined in terms of itself, we have a recursive definition. We call this the recursive functional composition rule. The proof is as follows:

1. [→ H]  (H = k)  (assumed)
2. [F → H]  (∀F′)(H = k)  (underlying logic rule)
3. [F, F′ → H] (H = k)  (left introduction rule)
4. [F, F′ → G] (∀z)G(z) = T (F, F′, k, z) (3, a sequence of applications of

the functional composition rule with individual functions)

5. [F → G]  (∀z)G(z) = T (F, G, k, z) (4, recursion rule)

This rule permits a number of functions to be defined in terms of one another using mutual recursion and known computable individual functions. This rule is fairly powerful and permits many functions to be derived in one step. We later comment on how this can be controlled.

Note that from these rules we can derive the following:

[X → Y]true

\frac{(∀X, Y)A}{[X → Y]A}

\frac{(∀X)A}{[→ X]A}

\frac{[X → Y]A}{(∀X)(∃Y)A}

5 Soundness of the Logic

Using this semantics we can show that the rules of inference are sound (and constructive in the functions F_{i}). For this we have to consider the following rules:

renaming rule  left elimination rule
permuting rule  right elimination rule
eliminating duplicates  introduction rule
recursion rule  right introduction rule
functional composition rules conjunction rule
underlying logic rule  least fixpoint rule

We call (∃F_{1} … F_{n} ∈ P C)(∀X)A[X, F_{1}(X), …, F_{n}(X)] the semantic formula for [X → Y]A. We abbreviate this formula as [(F_{1} … F_{n}) : X → Y]A[X, Y]. We often use F as an abbreviation for a list (F_{1} … F_{n}) of program constructing functions; then we have [F : X → Y]A[X, Y] as an abbreviation for this formula. We can also write it as (∃F)(∀X)A[X, F [X]]. Yet another representation is (∀X, Y)(F [X] = Y ⊃ A[X, Y]). We now show that the rules are sound. As for the renaming rule, since we can rename X in the formula (∀X)A[X, F_{1}(X), …, F_{n}(X)], we can also rename X in [X → Y]A. We can rename Y since the variables Y do not explicitly appear in the semantic formula. Duplicates in X can be eliminated since (∀X)(∀X)B is equivalent to (∀X)B. The X variables can be permuted since universal quantifiers can be permuted, and because the projection functions (and compositions) are computable. The Y variables can be permuted since the existential quantifiers for F_{1} … F_{n} can be permuted. Duplicates in the Y variables can be eliminated since duplicate existential quantifiers can be eliminated. None of these rules introduce new F_{i}, so constructibility of the F_{i} is preserved. Some of these rules permute the F_{i} or their arguments but these transformations are all constructible.

The recursion rule is justified by the fact that the program construction functions have constructible fixpoints, property 3 above. In particular, assume [X, U → Y, Z]A[X, U, Y, Z]. The corresponding semantic formula is (∃F, G ∈ P C)(∀X, U) A[X, U, F (X, U), G(X, U)]. Let F and G refer to particular elements of PC, so we have now (∀X, U) A[X, U, F (X, U), G(X, U)]. Let H(X) be a fixpoint of F, that is, F (X, H(X)) = H(X). Instantiating the semantic formula, we obtain (∀X) A[X, H(X), F (X, H(X)), G(X, H(X))]. Since F (X, H(X)) = H(X), we have (∀X) A[X, H(X), H(X), G(X, H(X))]. Since functions in P C have constructible fixpoints, H(X) is also in P C. Also, since compositions of elements of P C are in P C, we have that the function G′(X) = G(X, H(X)) is also in P C. Therefore we obtain the formula (∀X)A[X, H(X), H(X), G′(X)], and from it (∃H, G′ ∈ P C)(∀X)A[X, H(X), H(X), G′(X)], which is the semantic formula for [X → Y, Z] A[X, Y, Y, Z].

We now consider the functional composition rule. In a functional setting, we typically choose the program domains to include all (well-sorted) compositions of elements of the program domains, justifying the functional composition rules. The second rule interfaces functions and predicates. Also, such compositions are constructible. However, these rules need not be sound for all programming logics P L. The underlying logic rule is sound since if (∀X, Y) (A[X, Y] ⊃ B[X, Y]) in the underlying logic then (∀X) A[X, F_{1}(X), …, F_{n}(X)] implies (∀X) B[X, F_{1}(X), …, F_{n}(X)], hence (∃F_{1} … F_{n} ∈ P C)(∀X) A[X, F_{1}(X), …, F_{n}(X)] implies (∃F_{1} … F_{n} ∈ P C)(∀X) B[X, F_{1}(X), …, F_{n}(X)], so [X → Y]A implies [X → Y]B. This does not change the F_{i}, so we preserve constructibility of the F_{i}.

The left elimination rule is sound since the semantic formula for [X, Y →]A is (∀X, Y)A. The right elimination rule is sound since some of the expressions F_{i}(X) can be replaced by existentially quantified variables in the semantic formula.

The left introduction rule is sound by properties of universal quantifiers in the underlying logic. We are giving the semantic functions extra arguments, which is allowed because projections are computable and composition is computable. The right introduction rule is sound since there is at least one computable program constructing function of each sort and we can choose this to be the F_{i} corresponding to Z. These rules all transform the F_{i} in constructible ways, often not at all.

We consider the conjunction rule:

\frac{[X → Y]A [X → Z]B}{[X → Y, Z](A ∧ B)} (Conjunction rule; if no captures and Y, Z are disjoint)

This rule is valid because existential quantification (for the F_{i}) can be pushed inside conjunction when the existentially quantified variables only appear in one conjunct. That is, (∃F)(∀X)A[X, F [X]] ∧ (∃G)(∀X)B[X, G[X]] is equivalent to (∃F, G)((∀X)A[X, F [X]]∧(∀X)B[X, G[X]]), or, to (∃F, G) (∀X) (A[X, F [X]] ∧B[X, G[X]]), which is [(F, G) : X → Y, Z](A[Y] ∧ B[Z]). This rule combines two sets of program construction functions, an operation which is constructible.

We now consider the least fixpoint rule:

\frac{[X, U → Y, Z]A[X, U, Y, Z] (∀XU)(∃!Y)(∃Z)A[X, U, Y, Z]}{[X → Y, Z](A[X, Y, Y, Z] ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)}

Here (∃!Y) means “there exists a unique Y.” For this rule, ≤_{d} must be a domain ordering satisfying appropriate conditions, that is, least fixpoints of continuous functions exist and are constructible. These are assumptions that are often satisfied in practice. Also, we need to assume that all constructible program constructing functions are continuous. From the hypothesis [X, U → Y, Z]A[X, U, Y, Z] we have that there are tuples F and G of program contructing functions such that (∀XU)A[X, U, F [X, U], G[X, U]]. We then know that for each X there is a least Y such that F [X, Y] = Y. We assume that least fixpoints are constructable, so let H be an element of P C such that F [X, H[X]] = H[X] and such that H[X] is a minimal such element. Thus we have (∀X) A[X, H[X], F [X, H[X]], G[X, H[X]]], that is, (∀X) A[X, H[X], H[X], G[X, H[X]]]. Thus we have [X → Y, Z]A[X, Y, Y, Z], reasoning as in the recursion rule. Now, if (∃Z′)A[X, Y′, Y′, Z′], then from A[X, Y′, F [X, Y′], G[X, Y′]] we know that Y′ is F [X, Y′], since we are given the hypothesis (∀XU)(∃!Y) (∃Z)A[X, U, Y, Z]. Since Y′ is F [X, Y′], Y′ is a fixpoint of F. Letting Y be the least fixpoint H[X] of F, we have that A[X, Y, Y, Z] and Y ≤_{d} Y′. This is what is needed. The proof for the stronger version of the fixpoint rule is similar, except that we only can conclude Y ≤_{d} Y′ when the uniqueness assumption holds. We note that domains permit us to express nontermination using “bottom” (⊥, or undefined) if desired. Thus we can reason about termination and nontermination within this formalism. Also, it is not necessary that all programs terminate; we can represent nonterminating programs.

5.1 Consistency

We note that if we interpret the formula [X → Y]A as (∀X)(∃Y)A, then all inference rules are sound in the underlying logic except possibly the recursion rule and the functional composition rules. Therefore, if the underlying logic is sound, any proof not using the recursion rule or the functional composition rules is sound. For the full logic, we note that consistency is not a trivial matter. Consider the formula [X → Y](Y = X + 1). If we apply the recursion rule we obtain [→ Y](Y = Y + 1). Applying right elimination we get (∃Y)(Y = Y + 1). Using the underlying logic rule we obtain 0 = 1. However, we want to have addition by 1 computable since the logic is supposed to capture computability. Therefore we must take care to ensure consistency in some other way. For this, we need to have domains in which least fixpoints exist. This means that the integers would be extended with a “bottom” element ⊥ and we then have ⊥ = ⊥ + 1 removing the inconsistency. So we can only say Y − Y = 0 if Y ≠ ⊥, which is annoying but manageable, and this prevents the above derivation of 0 = 1. Note that such considerations only apply to values produced by computations; in the underlying logic, if we know that Y is an integer then we can use the identity Y − Y = 0. This introduction of fixpoints causes other problems. For example, in the underlying logic, we would like to have the rule (∀x)(P (x) ∨ ¬P (x)). This implies P (⊥) ∨ ¬P (⊥). However, computable functions are typically taken to be monotone. This means that if P is computable, then P (⊥) ⊃ (∀x)P (x). This would imply that if P and ¬P are computable and nontrivial, we cannot have (∀x)(P (x) ∨ ¬P (x)). It would be highly unpleasant to give up the rule (∀x)(P (x) ∨ ¬P (x)). We could develop special rules for “⊥”; for example, we could replace (∀x)A by (∀x)((x ≠ ⊥) ⊃ A) everywhere. But the domain structures can be more complicated than this, and so such an approach is not in general sufficient. Our approach is to say that computability is explicitly treated by the logic P L, and that the underlying logic need not be concerned with it. Therefore, if P is computable, ¬P may be uncomputable, but we can still use it and have the axiom (∀x)(P (x) ∨ ¬P (x)). Therefore we may have P (x) for some x and not P (⊥); this implies that ¬P is not monotone, and therefore not computable. Later we will give a general method for “coercing” values of computed predicates to Booleans, so that the underlying logic need not deal with “bottom” as a value of a predicate.

If we interpret the formula [X → Y]A as the semantic formula (∃F_{1} … F_{n} ∈ P C)(∀X)A[X, F_{1}(X), …, F_{n}(X)] then again all rules of inference are sound in the underlying logic except the functional composition rules and the recursion rule. However, if we assume that the underlying logic has at least one programming structure (that is, satisfying the above three properties about program constructing functions), then all rules of inference are sound including the recursion rule. If the functional composition rules are used, then corresponding properties of the program domains and the sort P C must be assumed for the underlying logic. In this way we can translate any proof involving formulae of P C into a proof in the underlying logic. In order to derive both a formula W and its negation, W must not have a program constructor quantifier, since none of the formulas have negations outside of the program constructor quantifier [X → Y]. Therefore W must be a formula in the underlying logic. However, these P L derivations of W and its negation can be translated into derivations in the underlying logic using the semantic formulas in place of the formulas of P L. This would imply that the underlying logic were inconsistent. However, we assumed that the underlying logic had at least one structure satisfying the specified properties, that is, at least one model M. Also, all rules of inference, translated in this way, are sound. Thus M would have to satisfy both W and its negation, which is not possible. We note again, however, that this translation of formulas into the corresponding semantic formulas does not fully capture the semantics of the logic, since the program constructing functions must be derived constructively.

6 General Deduction Theorems

Some kind of general deduction theorems can give us more flexibility in the way rules are written. These also may make some proofs easier to write (and derive). We derive such rules here syntactically and semantically. For this we use ⊢_{P L} to indicate derivability in the logic P L.

6.1 First deduction principle

D_{1}. If we can show

\frac{[→ Y_{1}]A_{1} Γ}{[X → Y]A}

(that is, Γ, [→ Y_{1}]A_{1} ⊢_{P L} [X → Y]A) then it follows that

\frac{Γ}{[Y_{1}, X → Y](A_{1} ⊃ A)}

(that is, Γ ⊢_{P L} [Y_{1}, X → Y](A_{1} ⊃ A)) assuming that Y_{1} and Y are disjoint. We can give a (semantic) validity argument as follows. We express Γ in more detail as follows:

\frac{[→ Y_{1}]A_{1}(Y_{1}) [X_{2} → Y_{2}]A_{2}(X_{2}, Y_{2}) … [X_{n} → Y_{n}]A_{n}(X_{n}, Y_{n})}{[X → Y]A(X, Y)}

We show that

\frac{[X_{2} → Y_{2}]A_{2}(X_{2}, Y_{2}) … [X_{n} → Y_{n}]A_{n}(X_{n}, Y_{n})}{[Y_{1}, X → Y]A_{1}(Y_{1}) ⊃ A(X, Y)}

We do this as follows. From the hypotheses we have F_{i} such that A_{1}(F_{1}) and (∀X_{i})A_{i}(X_{i}, F_{i}(X_{i})), i > 1. Then G(F_{1} … F_{n}) is such that (∀X)A(X, G(X)). Thus (∀X)A(X, G(F_{1} … F_{n})(X)). We can write this as (∀X)A(X, G(F_{2} … F_{n}) (F_{1}, X)). Then we have that ∧_{i}(∀X_{i})A_{i}(X_{i}, F (X_{i})) ⊃ ((∀X, Y_{1})A_{1}(Y_{1}) ⊃ A(X, G(F_{2} … F_{n}) (Y_{1}, X))). This corresponds to the inference rule

\frac{[X_{2} → Y_{2}]A_{2}(X_{2}, Y_{2}) … [X_{n} → Y_{n}]A_{n}(X_{n}, Y_{n})}{[Y_{1}, X → Y]A_{1}(Y_{1}) ⊃ A(X, Y)}

And of course if we have Y_{1} in the conclusion, it can be moved back as a hypothesis using the composition rule, so we can go from the lower form of the inference rule to the upper form.

6.2 Second deduction principle

D_{2}. If

\frac{[W → Y_{1}]A_{1} Γ}{[Z → Y]A}

then

\frac{[X, W → Y_{1}]C(X) ⊃ A_{1} Γ}{[X, Z → Y]C(X) ⊃ A}

Note that A_{1} only mentions Y_{1}, not X. This can be shown valid by a simple syntactic argument. Suppose we have the upper inference rule. Suppose also that we have [X, W → Y_{1}]C(X) ⊃ A_{1} and Γ. Now, we want to show that [X, Z → Y]C(X) ⊃ A can be derived. By the first deduction principle, it suffices to show that from [→ X]C(X) we can derive [Z → Y]A. From [→ X]C(X) and [X, W → Y_{1}]C(X) ⊃ A_{1} we can derive [W → Y_{1}]A_{1} by the composition rule. Then by the upper inference rule we can derive [Z → Y]A. This is all that is required. We now show that the lower rule (for all C) implies the upper one. For this, it suffices to let C(X) be “true.” Then the X variables in the hypothesis and conclusion become superfluous, and can be eliminated, leading to the upper rule.

6.3 Syntactic proofs

We now give syntactic proofs of the first deduction principle. We rewrite this principle in the following way (D′_{1}):

If

\frac{[→ X]A(X) Γ}{[Y → Z]B(Y, Z)}

then

Γ ⊢_{P L} [X, Y → Z]A(X) ⊃ B(Y, Z)

assuming that X and Z are disjoint. This needs to be shown for each of the inference rules of P L. Then we show D′_{2}: if there is an inference rule of the form

\frac{[X → Y]A(X, Y) Γ}{[U → V]B(U, V)}

then we have

Γ, [W, X → Y]C(W) ⊃ A(X, Y) ⊢_{P L} [W, U → V]C(W) ⊃ B(U, V)

where W and Y and W and V are disjoint. Together these suffice to prove the first (hence both) deduction principles, by induction on proof size. We note that renamings of variables in the conclusion are not significant and are permitted when necessary. We start with D′_{1}. We consider the renaming variables rule. The only case of concern to us is the following:

\frac{[→ X]A(X)}{[→ Y]A(Y)}

We need to show that [X → Y]A(X) ⊃ A(Y) (when X and Y are disjoint). This follows because the identity is computable (from the first functional composition rule).

Now we consider the rule that permits us to permute variables:

\frac{[→ X]A(X)}{[→ Y]A(X)}

where Y is a permutation of X. We need to show that [X → Y]A(X) ⊃ A(X). This is not allowed, since X and Y have common variables and this is not permitted. So let Y′ and X′ be consistent renamings of Y and X (since the names of the variables is not significant). Then we want to show that [X → Y′]A(X) ⊃ A(X′). By the permutation of variables rule, it suffices to show [X → X′]A(X) ⊃ A(X′). This follows from [X → X′](X′ = X); by the underlying logic rule we obtain [X → X′](X′ = X) ∧ A(X) ⊃ A(X). By the underlying logic rule again we obtain [X → X′]A(X) ⊃ A(X′).

The recursion rule and least fixpoint rules are not relevant because the hypothesis is not of the right form. The functional composition rules are not applicable because they have no hypothesis. Consider the underlying logic rule; in the form of concern to us it is

\frac{[→ X]A(X)}{[→ X]B(X)}

where A(X) ⊢ B(X) in the underlying logic. To separate the variables, we make this

\frac{[→ X]A(X)}{[→ Y]B(Y)}

and desire to show that [X → Y]A(X) ⊃ B(Y). This follows again from the rule [X → Y](Y = X) by the underlying logic rule (assuming equality replacement is allowable there). The remaining rules are handled by similar arguments.

We now go back and show D′_{2} for each inference rule. Suppose we have

\frac{[X → Y]A(X, Y) Γ}{[U → V]B(U, V)}

and the conclusion is obtained by renaming variables; then Γ is empty and the rule is of the form

\frac{[X → Y]A(X, Y)}{[U → V]A(U, V)}

We want to show that [Z, X → Y]C(Z) ⊃ A(X, Y) ⊢_{P L} [Z, U → V]C(Z) ⊃ A(U, V). But this is obtained directly by renaming variables. The permuting variables rule is equally direct.

Consider the recursion rule:

\frac{[X, U → Y, Z]A(X, U, Y, Z)}{[X → Y, Z]A(X, Y, Y, Z)}

From this general schema we also immediately have

\frac{[W, X, U → Y, Z]C(W) ⊃ A(X, U, Y, Z)}{[W, X → Y, Z]C(W) ⊃ A(X, Y, Y, Z)}

as required. The functional composition rules are not relevant. The least fixpoint rule is as follows:

\frac{[X, U → Y, Z]A[X, U, Y, Z] (∀XU)(∃!Y)(∃Z)A[X, U, Y, Z]}{[X → Y, Z](A[X, Y, Y, Z] ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)}

We want to show the following:

\frac{[W, X, U → Y, Z]C(W) ⊃ A[X, U, Y, Z] (∀XU)(∃!Y)(∃Z)A[X, U, Y, Z]}{[W, X → Y, Z]C(W) ⊃ (A[X, Y, Y, Z] ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)}

Now, from the least fixpoint rule, substituting C(W) ⊃ A[X, U, Y, Z] everywhere for A[X, U, Y, Z] we obtain

\frac{[W, X, U → Y, Z]C(W) ⊃ A[X, U, Y, Z] (∀W XU)(∃!Y)(∃Z)(C(W) ⊃ A[X, U, Y, Z])}{[W, X → Y, Z]((C(W) ⊃ A[X, Y, Y, Z]) ∧ (∀Y′)((∃Z′)(C(W) ⊃ A[X, Y′, Y′, Z′])) ⊃ Y ≤_{d} Y′)}

We have the following proof:

1. [W, X, U → Y, Z] C(W) ⊃ A[X, U, Y, Z]

(assumption)

2.  (∀XU)(∃!Y)(∃Z)A[X, U, Y, Z]

(assumption)

3.  (∀W XU)(∃!Y)(∃Z)(C(W) ⊃ A[X, U, Y, Z])

(derivation in underlying logic)

4. [W, X → Y, Z]  ((C(W) ⊃ A[X, Y, Y, Z]) ∧ (∀Y′)((∃Z′)(C(W) ⊃ A[X, Y′, Y′, Z′]))

⊃ Y ≤_{d} Y′)

(least fixpoint rule)

5. [W, X → Y, Z]  ((C(W) ⊃ A[X, Y, Y, Z]) ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)

(underlying logic rule)

6. [W, X → Y, Z]  (C(W) ⊃ (A[X, Y, Y, Z]) ∧ (∀Y′)((∃Z′)A[X, Y′, Y′, Z′]) ⊃ Y ≤_{d} Y′)

(underlying logic rule)

The underlying logic rule and all the remaining rules are fairly straightforward.

6.4 Applications to program generation

We give one application of the above deduction rules to program generation. Suppose we have done a derivation of the following form:

\frac{[→ Y_{1}]A_{1}(c) … [→ Y_{n}]A_{n}(c)}{[X → Y]A(c)}

where c is an uninterpreted constant symbol. This derivation essentially shows how a program satisfying A can be derived from programs satisfying A_{i}. This form of proof is convenient because it often corresponds to the calling structure of the procedures used. However, we may need to change this proof to a different form to prove that the specification A is always satisfied. By repeated application of the first deduction principle, we obtain

[Y_{1} … Y_{n}X → Y](∧_{i}A_{i}(c) ⊃ A(c))

Since c is arbitrary, we can introduce a universal quantifier:

[Y_{1} … Y_{n}X → Y](∀x)(∧_{i}A_{i}(x) ⊃ A(x))

Now it may be possible to apply the recursion rule to make some of the Y_{i} identical to Y and then use mathematical induction to show (∀x)A(x). For this the variable X may be essential, since it can be used to record the argument on which a program is called. Such inductions typically make use of the fact that recursive calls use values of the parameters that are smaller in some well-founded ordering.

7 Extracting Program Constructing Functions from Proofs

We now show in a systematic way how to extract a program constructing function from a proof. Actually, a proof may be regarded as a constructive mapping from program constructing functions in the hypotheses, to a program-constructing function in the conclusion. For each rule, we give a description of this mapping and show that it is constructive. To indicate the mapping, we use the quantifier [F : X → Y]A[X, Y] which is interpreted as before as (∀X)A[X, F [X]]. Here F is considered as a tuple of program-constructing functions. This construction also gives a more formal presentation of some of the reasoning in the proof of soundness of the logic.

Again we consider the following rules:

renaming rule  left elimination rule
permuting rule  right elimination rule
eliminating duplicates  introduction rule
recursion rule  right introduction rule
functional composition rules conjunction rule
underlying logic rule  least fixpoint rule

For this discussion, we consider (F, G) to be a tuple of program constructing functions such that (F, G)[X] is the concatenation of F [X] and G[X].

Corresponding to the renaming rule we have the rule

\frac{[F : X → Y]A[X, Y]}{[F : U → V]A[U, V]}

which is constructive since the F in the conclusion is obtained constructively (by the identity transformation) from the F in the hypothesis.

For the permutation rule we have

\frac{[F : X → Y]A[X, Y]}{[F′ : U → V]A[U, V]}

where U and V are permutations of X and Y and where F’ is defined so that A[X, F [X]] is a variant of A[U, F′[U]]. This is done by defining F′ as F with the arguments permuted and the elements of F permuted as necessary. This is still a constructive transformation, and is allowable since projections and composition are computable.

The rule eliminating duplicates does not change F since only the first occurrence of a variable in X or Y matters.

For the recursion rule we have

\frac{[(F_{1}, F_{2}) : X, U → Y, Z]A[X, U, Y, Z]}{[(G, F_{2}) : X → Y, Z]A[X, Y, Y, Z]}

where F_{1}[X, U] and F_{2}[X, U] correspond to Y and Z, respectively and where F_{1}[X, G[X]] = G[X]. Thus G is a fixpoint of F_{1}. Since we assume the fixpoint operator is constructive, this transformation from (F_{1}, F_{2}) to (G, F_{2}) is constructive.

The functional composition rules, where applicable, introduce a new program construction operation which is the composition of functional programs or the composition of functions and a predicate. This is assumed to be a constructive operation.

The underlying logic rule does not change F, and so the transformation is constructive.

For the left elimination rule, there are no program construction operations, and so the transformation is constructive. The hypothesis is of the form [X, Y →]A, which means that F is empty.

We can express the right elimination rule in this way:

\frac{[(F, G) : X → Y, Z]A}{[F : X → Y](∃Z)A}

This eliminates part of the given (F, G) tuple, and is therefore constructive. The left introduction rule can be expressed as follows:

\frac{[F : X → Y](∀Z)A}{[G : Z, X → Y]A}

where G[Z, X] is F [X]. This is allowed because projection and composition are computable, and is constructive.

The right introduction rule is expressed as follows:

\frac{[F : X → Y](∀Z)A}{[(F, G) : X → Y, Z]A}

where G[X] is defined to be a fixed tuple Z of programs; this is allowable since we assume that there is at least one program of each sort, which is known constructively.

For the conjunction rule we have

\frac{[F : X → Y]A [G : X → Z]B}{[(F, G) : X → Y, Z](A ∧ B)}

For the least fixpoint rule (when assumed) we have that the least fixpoint is constructible, so there is a constructible mapping giving the least fixpoint of a program generating function.

By repeatedly applying the above transformations we can obtain a program transforming function from a proof, if program transforming functions for the hypotheses are applied. Also, this can be done constructively. This provides a proof of the soundness of the logic as well as a way of extracting a program transforming function.

7.1 Specific programming languages

We generalize the construction of programs from proofs to permit the generation of programs in specific programming languages. This also permits us to give a more concrete description of the constructibility requirement on the logic. To do this, for each inference rule

\frac{[X_{1} → Y_{1}]A_{1} … [X_{n} → Y_{n}]A_{n}}{[X → Y]A}

we have to find a term t(F_{1}, … F_{n}) in the underlying logic such that the rule

\frac{[F_{1} : X_{1} → Y_{1}]A_{1} … [F_{n} : X_{n} → Y_{n}]A_{n}}{[t(F_{1} … F_{n}) : X → Y]A}

is sound in the underlying logic, that is,

[F_{1} : X_{1} → Y_{1}]A_{1} ∧ … ∧ [F_{n} : X_{n} → Y_{n}]A_{n} logically imply [t(F_{1} … F_{n}) : X → Y]A. Also, these terms t must be constructible in two senses: They must have a computable operational semantics, and they must be constructible, that is, the terms in the conclusion of each inference rule must be constructible from the terms in the hypotheses. For this purpose, we might have some term like fix(X, F (X, Y)) for the recursion rule to represent a tuple G such that F (G(Y), Y) = G(Y), and in this case, fix would have to be computable to produce the programs in the conclusion of the rule from programs in the hypotheses. Similarly, compositions and other operations used to construct programs in the inference rules must be computable. Furthermore, the programs so constructed must have a computable operational semantics. Using such rules repeatedly, we build up expressions representing program generating functions; these can be converted to programs when values for the unknown subprograms (or unknown program generating functions) are supplied. This transformation can be made more efficient by making use of derived rules of inference adapted to efficient constructions in the programming language. For example, certain recursions can be more efficiently translated into an iterative loop than a general recursion. Such recursions can be expressed in a derived rule of inference that captures the idea of a recursion that involves a counter (or whatever). By fashioning the proof so that such derived rules are used, one can obtain more efficient programs. This idea is also explored in a different program generation context by [1].

We illustrate the use of a derived rule for iteration to enable the generation of more efficient programs. Consider the following proof, where the underlying logic includes arithmetic and conditionals are computable:

1. [→ S]  P (S, 0)

(assumed)

2. [→ X]  (∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1))

(assumed)

3. [S, X, Y → Z] (∀n)(Z(n) = if n = 0 then S else X(Y (n − 1)))

(derived functional composition rule, using the computability of some functions)

4. [S, X → Y]  (∀n)(Y (n) = if n = 0 then S else X(Y (n − 1)))

(3, recursion rule, renaming)

5. [→ Y]  (∃X, S)P (S, 0) ∧ (∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1))

∧(Y (n) = if n = 0 then S else X(Y (n − 1))) (1,2,4,composition rule)

6. [→ Y]  (∀n)(n ≥ 0 ⊃ P (Y (n), n))

(5, underlying logic rule)

In this way we obtain the following derived rule of inference:

\frac{[→ S]P (S, 0) [→ X](∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1))}{[→ Y](∀n)(n ≥ 0 ⊃ P (Y (n), n))} (It_{1})

The computed program would involve recursion, by the recursion rule in step 4. However, this computation can be done more efficiently by an iteration in many languages; the program Y (n) can be expressed something like this:

w := S; for i = 1 step 1 until n do W := X(w) od;

Therefore, by explicitly including this construction in the above derived inference rule, one could obtain a more efficient program. This would be a general optimization technique available when the underlying logic satisfied suitable additional assumptions. There are numerous opportunities for this kind of optimization, making use of special constructs in the target programming language.

7.2 Extracting concrete programs

In order to obtain an actual program, one has to have a proof in which none of the hypotheses assert the existence of program transforming functions. Also, the conclusion must be of the form [→ Y]A. Then the above constructions yield a program satisfying the specification A. However, we imagine that the system would often be used in a more abstract way, to reason about program constructing functions with generic assumptions. That is, if we can derive a formula A from formulae A_{1} … A_{n}, possibly asserting the existence of program constructing functions, and we can derive A_{1} from formulae B_{1} … B_{m}, possibly also asserting the existence of program constructing functions, then we can derive A from B_{1} … B_{m}A_{2} … A_{n}. This involves putting together program constructing functions while still not constructing a concrete program. The ability to reason at this abstract level should increase the reusability and applicability of the proofs in this system. We note that in practice we will have a derivation of A′ from A_{1} … A_{n} and will need to show that A′ implies A; this involves a kind of fitting together of programs. To do this, we may have to apply some kind of a proof homomorphism to the sub-proof, as explained below, to make the terminology consistent. We may also have to do some reasoning in the underlying logic. For example, A may be [X → Y]C and A′ may be [X → Y]C′. Then using the underlying logic rule it suffices to show that ⊢ (∀X, Y)(C′ ⊃ C). This amounts to showing that a given program satisfies a specification. Assuming that the underlying logic is classical, this step involves purely classical reasoning. We anticipate that a library of programs would be expressed in P L and derived with human assistance; then these programs could be combined for specific applications. This combining step would therefore be largely restricted to classical logic. We can regard the proof of A from A_{1} … A_{n} as a parameterized program constructing function; when the program constructing functions for A_{1} … A_{n} are supplied, we obtain a program constructing function A. This is somewhat like having generic programs for sorting, manipulating lists, and so on. Now, when we derive A_{1} from B_{1} … B_{m}, we are to an extent instantiating the generic program constructing function for A_{1}, introducing in the process a number of other generic program constructing functions on which it depends. Note that this is done in a way that guarantees correctness; we can only instantiate the program constructing function for B_{1} in a way that satisfies the specification B_{1}. Note the similarity of this approach to the use of abstract data structures.

7.3 Proof homomorphisms

It is possible to combine proofs in another way. For example, the choice of names for the functions and predicates in the logic is often arbitrary. One would like to be able to combine proofs using different naming conventions. Thus, one would like to translate a proof using one naming convention into a proof using another naming convention. Then the proofs could be combined. In general we can imagine a proof homomorphism H as a function mapping formulae in one underlying logic L_{1} to another underlying logic L_{2}. We define h([X → Y]A) to be [X → Y]h(A) and therefore obtain a mapping between the programming logics P L_{1} and P L_{2} based on L_{1} and L_{2}, respectively. Recall that ⊢_{P L} indicates derivability in the logic P L, and similarly for logics P L_{1} and P L_{2}. We say a mapping H is a proof homomorphism from P L_{1} to P L_{2} if it is a mapping from P L_{1} to P L_{2} and the following property is satisfied:

If A_{1} … A_{n} ⊢_{P L} 1A then h(A_{1}) … h(A_{n}) ⊢_{P L_{2}} h(A).

We have the following easy result:

Proposition 7.1 The mapping H is a proof homomorphism if the following conditions are satisfied:

1. All axioms of L_{1} must map onto theorems of L_{2}.

2. If

\frac{A_{1} … A_{n}}{A}

is an inference rule in L_{1}, then in L_{2} we must have h(A_{1}), …, h(A_{n}) ⊢ h(A).

Proof. By induction on the size of proofs.

□

In addition to simple mappings that involve changes in the names of functions and predicates, we have more interesting ones. For example, we can change X < Y to X > Y everywhere in many cases; using this mapping we can map a program to sort in increasing order, to a program to sort in decreasing order. Also, one might (for example) encode the integers as lambda calculus terms. Then, one could construct a proof homomorphism mapping results about the integers onto results about lambda calculus expressions. The use of such homomorphisms permits one to combine programs written with respect to different underlying logics.

In general, one can conveniently write general proofs that mention objects in the underlying logic (such as trees, terms, numbers, et cetera). When generating programs in some specific language, it may be necessary to find a more concrete representation of these objects; for example, we may need to represent trees or terms as lists in LISP. We can use a proof homomorphism for this purpose. Note that the original proof, mentioning abstract objects such as trees, is in this way more abstract than a proof in any concrete language, which must represent these objects in some way. This is one advantage of our representation of programs as proofs, over representing them in some specific language.

Another application of proof homomorphisms is to state variables. We may map an abstract proof onto one that corresponds to a program with an internal state; this may permit a more efficient use of data structures, for example. This could be formalized by adding an extra output to each function; this extra output would be the state resulting from computing the function. Our notion of proof homomorphisms is general enough to permit such a mapping that adds (or deletes) state information to (from) a program. Since our logic does not treat outputs of programs in any special way, such a mapping is possible. This also permits the combination of programs in different formalisms; we might have one program customized to list structures, and another that works on the level of abstract objects such as trees. We can combine them by first mapping the latter program onto a program in which trees are represented as lists. We might also be able to have a proof homomorphism mapping recursive constructions onto an explicit stack implementing recursion on a traditional von Neumann style architecture.

Used in this way, the programming logic P L has many of the advantages of algebraic specification methodologies [9] and other such algebraic specification methods: modularity, abstractness, reusability, and the guarantee of correctness with respect to a specification. However, this is obtained without a commitment to the initial algebra approach. Later we will also mention problems which rule out the direct use of the initial algebra approach in our method.

These proof homomorphisms also permit an abstract algorithm (a proof) to be realized in various programming languages. For this, we extend proof homomorphisms to statements of the form [t : X → Y]A by h([t : X → Y]A) = [h(t) : X → Y]h(A). Thus the proof homomorphism can also map the terms t representing program generation functions. In this way we can obtain programs in different languages. We can verify the correctness of such proof homomorphisms in the same way as given above, but with attention paid to the h(t) terms.

8 Abstract Logic Programming

We present an abstract approach that permits proofs to be converted into logic programs satisfying the specifications. This will include both term-rewriting systems, Horn-clause style logic programming, and functional programs as special cases. Then we give methods for showing that specific systems fit into the general framework. This framework automatically guarantees that the logic programs are constructible from a proof in P L. We write a logic program L[X; Y] to indicate that X are input program variables and Y are output program variables. A logic program in this sense is just a formula of a special form in the underlying logic. It is intended that some special proof system will be used to derive input-output relations from logic programs. For example, term-rewriting can be used to derive equational consequences, or Prolog-style reasoning can be used to derive consequences of Horn clauses. Thus if X is a program variable, to compute X(x_{1} … x_{n}) using L, we could derive a statement of the form X(x_{1} … x_{n}) = y from L. Or, in the Prolog approach, we could derive R_{X}(x_{1}, …, x_{n}, y) for some suitable relation R_{X}.

Definition 8.1 We say that a computable function F satisfies a formula [X → Y]A[X, Y] if (∀X)A(X, F (X)). In this case we write F ⊧ [X → Y]A[X, Y]. We also say F satisfies A[X, Y], and write F ⊧ A[X; Y].

Definition 8.2 We say that a logical expression L[X; Y] implements a formula [X → Y]A[X, Y] if there is a computable function F that satisfies [X → Y]L[X, Y] and if (∀XY)L[X, Y] ⊃ A[X, Y] is valid in the underlying logic. We require that all the input variables X that occur in L must also occur in A, and all the output variables that occur in A must also occur in L. However, there may be input variables in A that do not appear in L, and there may be extra output variables in L that do not appear in A. Note that A[X, Y] implements the formula [X → Y]A[X, Y] if this latter formula is derivable in P L.

Definition 8.3 A computable mapping G : L_{1} … L_{n} → L from logic programs to logic programs realizes an inference rule

\frac{[X_{1} → Y_{1}]A_{1} … [X_{n} → Y_{n}]A_{n}}{[X → Y]A}

if for all L_{1} … L_{n} implementing the hypotheses, G(L_{1} … L_{n}) implements the conclusion. Note that this allows customized realizations for derived inference rules. A computable mapping realizes a proof in the same way.

Theorem 8.4 If we have a proof in P L in which all inference rules are realized, then from logic programs implementing the hypotheses we can effectively obtain a logic program implementing the conclusion. That is, we can realize the whole proof.

Proof. By a simple induction on proof size.

□

Corollary 8.5 If we realize all the original inference rules in the system P L, then we can realize all proofs in P L.

8.1 Abstract logic programming languages

We now consider abstract logic programming languages and their ability to realize proofs.

Definition 8.6 A logic programming language is a set of formulas of the underlying logic, in which free program variables are specified as input and output variables.

Definition 8.7 We say that a logic programming language LL is P L-adequate if

1. Input and output variables can be renamed (subject to capture) (note that we need a subject to capture condition also for P L).

2. If L[X, U; Y, Z] is a logic program then so is L[X; Y, Y, Z] (or a logic program M[X; Y, Z] such that M[X; Y, Z] ⊃ L[X; Y, Y, Z] and such that for some constructible function h : P C → P C, for all functions F and G in P C, if (F, G) ⊧ L then (H(F), G) ⊧ M). That is, the input variables U have been replaced by output variables Y.

3. If A and B are logic programs with disjoint sets of output variables, then A∧B is a logic program.

4. If t[F] is a term involving functional program variables F, then there is a logic program L[G; F] such that L[G; F] ⊧_{UL} (∀x)G(x) = t[F](x). Also, this logic program is constructible from the formula (∀x)G(x) = t[F](x). Here x can be a sequence of variables, F is a sequence of program variables, and G is a single program variable.

5. For all program sorts, there is a logic program L(; Y) with one output variable Y and no input variables, implying Y = a for some computable a of the appropriate sort.

8.2 Annotating proofs with abstract logic programs

We now annotate the inference rules of P L to show how they can be realized by logic programs in a P L-adequate language LL. We call the resulting system P L_{prog}. Recall that in section 7.1 we used the notation [F : X → Y]A[X, Y] to indicate A[X, F (X)], where F is in P C. Here we use the notation [L : X → Y]A[X, Y] to indicate that L is a logic program implementing A. This is not the same, since a logic program L could be satisfied by more than one function F. Now, it is possible for L to have output variables not explicitly mentioned in Y. First we consider the renaming rule, in which U and V are renamings of X and Y:

\frac{[L[X; Y] : X → Y]A[X, Y]}{[L[U; V] : U → V]A[U, V]}

Next we consider the rule eliminating duplicates; here U and V are X and Y, respectively, with duplicates removed:

\frac{[L[X; Y] : X → Y]A[X, Y]}{[L[X; Y] : U → V]A[U, V]}

Next we consider the permutation rule; here U and V are permutations of X and Y, respectively:

\frac{[L[X; Y] : X → Y]A[X, Y]}{[L[X; Y] : U → V]A[U, V]}

\frac{[L[X, U; Y, Z] : X, U → Y, Z]A[X, U, Y, Z]}{[L[X; Y, Y, Z] : X → Y, Z]A[X, Y, Y, Z]} (Recursion rule)

where U and Y have the same sort.

\frac{[L[X, U; Y, Z] : X, U → Y, Z]A[X, U, Y, Z]}{[M[X; Y, Z] : X → Y, Z]A[X, Y, Y, Z]} (Recursion rule)

(alternate version, where appropriate)

For functional programming:

(Functional composition rule 1)

[L[F, G] : F_{1} … F_{m} → G](∀z_{1} … z_{n})G(z_{1} …, z_{n}) = T (F_{1}, …, F_{m}, z_{1}, …, z_{n})

where L[F, G] is a logic program such that L[F, G] ⊧_{UL} (∀z_{1} … z_{n})G(z_{1} …, z_{n}) = T (F_{1}, …, F_{m}, z_{1}, …, z_{n}). (This must exist by point 4 in the definition of P Ladequate.)

(Underlying logic rule)

\frac{[L : X → Y]A}{[L : X → Y]B} if ⊢ (∀X, Y)(A ⊃ B) in the underlying logic L

.

\frac{[L : X, Y →]A}{[true : Y →](∀X)A} (Left elimination rule)

\frac{[L : X → Y, Z]A}{[L : X → Y](∃Z)A} (Right elimination rule)

\frac{[L : X → Y](∀Z)A}{[L : Z, X → Y]A} (Left introduction rule; Z, Y must be disjoint)

\frac{[L[X; Y] : X → Y](∀Z)A}{[L[X; Y] ∧ L′[; Z] : X → Y, Z]A} (Right introduction rule; Z, X must be disjoint)

Here L′[; Z] is a conjunction of L′[; Z_{i}] for Z_{i} in Z, whose existence is required by point 5 in the definition of P L-adequate.

\frac{[L_{1} : X → Y]A [L_{2} : X → Z]B}{[L_{1} ∧ L_{2} : X → Y, Z](A ∧ B)} (Conjunction rule; if no captures and Y, Z are disjoint)

Theorem 8.8 If LL is P L-adequate then all proofs in P L can be realized by logic programs.

Proof. We show that the above annotated inference rules in P L_{prog} are all realized by the indicated logic programs. We first note that the transformations to the required logic programs in the conclusions are all computable. It remains to show that if the indicated logic programs implement the hypotheses, then the indicated logic program in the conclusion implements the conclusion. This is mostly quite straightforward. For example, for the recursion rule, we note that if (∀XUY Z)(L[X, U; Y, Z] ⊃ A[X, U, Y, Z]) then (∀XY Z)(L[X; Y, Y, Z] ⊃ A[X, Y, Y, Z]). The alternate version of the recursion rule is similar, since M[X; Y, Z] ⊃ L[X; Y, Y, Z]. For now we ignore the second functional composition rule, assuming that a predicate is regarded as a Boolean function. Or else we can extend 4. to predicates too. We ignore the least fixpoint rule for the time being. The underlying logic rule requires no change in the logic program. Perhaps it would be appropriate to give this argument in more detail. Suppose we derive [X → Y]B from [X → Y]A in P L. Let L be a logic program implementing [X → Y]A. Then we know that there is a computable function satisfying [X → Y]L. Also, (∀XY)(L ⊃ A). Since A ⊢ B in the underlying logic, (∀XY)(L ⊃ B) also. Therefore L implements B.

We now consider the left elimination rule. Suppose that [X, Y →]A[X, Y] and we have a logic program L implementing this rule. Then there is a computable function F such that (∀X, Y)A[X, Y, F (X, Y)], but since A has no output variables, we have (∀XY)A[X, Y]. Therefore we can take L to be just true, without any input or output variables, and L implements [X, Y →]A[X, Y]. It is easy to see that L also implements [Y →](∀X)A. The right elimination rule is handled as follows: Suppose L[X; Y, Z] implements [X → Y, Z]A. Then (∀XY Z)(L[X; Y, Z] ⊃ A). Therefore (∀XY W)(L[X; Y, W] ⊃ (∃Z)A). This is all that is required; we are allowed to have the extra W output variables in L. The left introduction rule is no problem; A receives new input variables that do not appear in L. The conjunction rule is dealt with by noting that the conjunction of two logic programs is a logic program, and that the output variables of the hypotheses are distinct. The right introduction rule introduces new output variables in A. For this, we need to introduce new output variables in L. By point 5, we can find a logic program with a new output variable. By point 3, we can take the conjunction of this logic program with another, adding a new output variable. By repeating this process, an arbitrary number of new output variables can be added. This is enough for the right introduction rule, since the hypothesis must be true for all Z.

□

What is slightly surprising about this theorem is that no quantifiers are required. Although the inference rules of P L may add or remove universal and existential quantifiers, these can be simulated by logic programs without any quantifiers at the outer level.

8.3 Observable behavior of logic programs

We now consider the computational aspect of logic programming languages. We assume that there is an interface language IL associated with LL and a (sound) inference operation ⊢_{LL} for deriving IL assertions from LL programs. For example, for term-rewriting systems, the assertions in IL might be of the form F (s_{1} … s_{n}) = t where s_{1}, …, s_{n}, and t are constructor terms and F is a defined function. Thus we evaluate F on inputs s_{1} … s_{n} and obtain the output t. Here the inference rules ⊢_{LL} could be term-rewriting. For Prolog-style Horn-clause logic programming, the IL-assertions might be of the form P (s_{1} … s_{n}) where P is a predicate and s_{1} … s_{n} are terms, indicating that the terms s_{i} satisfy P. This could be returned by a logic program as an answer to a query of the form :– P (r_{1} … r_{n}) for terms r_{i}. The inference rules here could be SLD-resolution for deriving such assertions P (s_{1} … s_{n}). The interface language corresponds to the input-output behavior of LL programs that is visible to the user. We require that the relation ⊢_{LL} be (partially) computable. That is to say, given A, one should be able to enumerate the formulas B such that A ⊢_{LL} B. This corresponds to the fact that logic programs should have a computable operational semantics.

Definition 8.9 Suppose L(X; Y) is a logic program and IL is an interface for it. Then the (IL-)interface of L is the set of B(X; Y) in IL such that L(X; Y) ⊢_{LL} B(X; Y). Here the X and Y are considered as free variables, so we really have that for any disjoint X and Y, L(X; Y) ⊢_{LL} B(X; Y). The interface of L is the observable part of L, as far as direct input-output behavior is concerned.

We now say something about the correctness of the derived logic programs. We often abbreviate L[; Y] and B(; Y) by L(Y) and B(Y).

Theorem 8.10 Suppose L[; Y] implements [→ Y]A(Y). Then there is a computable function F such that A(F) and such that if B(Y) is in the interface of L[; Y] then B(F). That is, the interface of L can be extended to a computable function satisfying the specification A.

Proof. Since L implements [→ Y]A(Y), there is a computable function F that satisfies [→ Y]L[; Y]. In this case this implies L[; F]. Since (∀Y)(L[; Y] ⊃ A(Y)), we have also A(F). Now, if B(Y) is in the interface of L(; Y), then L[; Y] ⊢_{LL} B(Y) hence L[; F] ⊢_{LL} B(F). Thus B(F) for all B in the interface, and F satisfies A.

□

In particular cases, we may be able to derive many such B, and then we know that these are correctly computed and can be extended to a computable function as stated above. It remains to say more about how much of F can be computed in general. The above theorem does not rule out the possibility that the interface of L can be empty, which for functional programs might mean that for no inputs s_{1} … s_{n} is the output t = F (s_{1} … s_{n}) computable. We will deriving conditions under which the deduction ⊢_{LL} is “complete,” in a sense. The idea is to show that there is a computable function F satisfying L such that for all B in IL, B(F) iff L(Y) ⊢_{LL} B(Y). Thus the interface of F is the intersection of the interfaces of all functions satisfying L, so F is a kind of “initial” object. This function F must also satisfy A, because L ⊃ A, and so if A(Y) ⊃ B(Y) for B in IL, we have that L(Y) ⊃ B(Y), hence B(F), so by definition of F, B is in the interface of L. Thus all B(Y) in IL for which A(Y) ⊃ B(Y), are in the interface of L, and hence visible to the user. The difficulty in general is nontermination; it is not easy to compute nonterminating elements, and the inputs or results of a computation may be nonterminating. These are considered as part of a computable function, but do not appear in the interface.

Definition 8.11 A logic programming language LL is extensible for interface IL if for all logic programs L in LL there exists a computable function F such that L(F) and such that for all B in IL, ⊧_{UL} B(F) iff L(X) ⊢_{LL} B(X).

Theorem 8.12 If LL is extensible for interface IL, L is in LL and L implements A, and (∀Y)(A(Y) ⊃ B(Y)), then B is in the interface of L.

Proof. Since LL is extensible for IL, there is a computable F such that L(F) and such that for all B in IL, B(F) iff L(X) ⊢_{LL} B(X). Since L(F) and L ⊃ A, A(F). Since (∀Y)(A(Y) ⊃ B(Y)), B(F). Therefore, by definition of F, L(X) ⊢_{LL} B(X).

□

We now want to give conditions under which L cannot derive “too much.” The preceding theorem still allows L to have an interface possibly larger than that needed for F.

Definition 8.13 Suppose L_{1} and L_{2} are logic programs in LL. Let IL be an interface language for LL. Then L_{1} and L_{2} are interface-equivalent (for IL) if for all assertions B in IL, L_{1} ⊢ B iff L_{2} ⊢ B.

Definition 8.14 A specification A(F) is complete with respect to an interface language IL iff A(F_{1}) ∧ A(F_{2}) implies that F_{1} and F_{2} are interface-equivalent for IL.

Theorem 8.15 Suppose L implements A and A is complete with respect to interface language IL. Suppose B(Y) is in the interface of L. Then (∀Y)(A(Y) ⊃ B(Y)).

Proof. We know there is a computable function F such that L(F). Since B is in the interface of L, B(F). Since L ⊃ A, A(F). Suppose A(Y); then Y is interfaceequivalent to F. Therefore B(Y) also.

□

Corollary 8.16 Suppose LL is extensible for interface IL, L is in LL, L implements A, and A is complete with respect to IL. Then B is in the interface of L iff (∀Y)(A(Y) ⊃ B(Y)).

Proof. By a combination of the two preceding theorems.

□

Completeness cannot be guaranteed since it depends on A, over which we have no control. The hardest part of the above is proving extensibility. For languages having a denotational semantics based on complete partially ordered sets and least fixpoints, extensibility is typically fairly straightforward. For such languages, the recursion rule corresponds to a least fixpoint operation, and for each logic program LL derived there will be a least computable function F satisfying LL. It follows that assertions of the form F (s_{1} … s_{n}) = t, where s_{i} and t are maximal in the domain ordering, will be true for all F satisfying LL. Maximal elements are “defined,” that is, they contain no occurrences of ⊥, typically. Furthermore, if t is “finite” (for example, not an infinite list), then such assertions can be derived by a finite computation (or derivation). Therefore, we may take the interface to be the set of such assertions F (s_{1} … s_{n}) = t where the s_{i} and t are defined and finite; this guarantees extensibility. However, for some programming formalisms, the existence of a denotational semantics is not straightforward; this includes term-rewriting systems (for whatever reason) and logic programs (because of the nondeterminism).

Another approach is to use initial algebras [9]; it is known that any set of equations has an initial algebra. One problem is that this algebra may be only partially computable; the equality may not be decidable. Another problem is that it may involve functions that do not possess fixpoints, as required by our definition of a programming structure. For example, consider the empty set of equations with the constructors 0 and s (successor). The initial algebra is the natural numbers. However, s must have a fixpoint. We usually require for constructors that s(x) = s(y) iff x = y. This implies that the fixpoint of s must be the infinite term s(s(s …)). In addition, we typically need ⊥ to represent undefined values. Thus the semantics will need to contain infinite terms with occurrences of “bottom.” In this way, the initial algebra approach becomes considerably more complicated, and not much different than the denotational semantic approach above. We still may get extensibility this way if the underlying logic is too weak to distinguish the initial algebra from computable functions, however.

8.4 Evaluation strategies and underlying logics

We may specify a number of different relations ⊢_{LL} for a given logic programming language LL, and these have implications for the underlying logic. These different relations ⊢_{LL} correspond to different methods for deriving consequences of a logic program L. These may correspond to different evaluation strategies (for example, lazy or eager evaluation), that is, different operational semantics. A strategy that permits more consequences of L to be derived, restricts the semantics more, since models of UL must satisfy all these consequences. A strategy that permits fewer consequences to be derived allows more flexibility in the choice of semantics, and sometimes permits a simpler semantics. This has a corresponding effect on the underlying logic, since it should be sound with respect to the semantics. In particular, the more models there are, the fewer inferences are sound in the underlying logic, and the more restrictive the underlying logic rule is. The fewer models there are, the more axioms and inferences can be used in the underlying logic rule. We will illustrate these interrelationships below.

8.5 Generating term-rewriting programs

We extend the inference rules to generate assertions of the form [R(X; Y) : X → Y]A[X, Y] where R(X; Y) is a term-rewriting system mentioning the variables X and Y as function symbols. For a survey of term-rewriting systems, see Dershowitz and Jouannaud [13] or [30]. To formalize the generation of such systems, we define a term-rewriting program R(X; Y) as a set (conjunction) of equations {r_{1} = s_{1} … r_{n} = s_{n}} in which the orientation of the equations matters, that is, which term is on the left and which is on the right. These equations may contain function symbols from the underlying logic as well as the variables X and Y as function symbols. These equations are viewed computationally as the term-rewriting system R_{→}(X; Y) = {r_{1} → s_{1} … r_{n} → s_{n}}. We require that these rules be orthogonal, that is, left linear and non-overlapping. We cannot in general require termination, since many reasonable programs do not correspond to terminating term-rewriting systems. However, left linearity is reasonable, since the left-hand sides correspond roughly to procedure calls, and the formal parameters of a procedure definition are typically distinct. A subset of the function symbols from the underlying logic are called constructor terms. Also, the left-hand sides r_{i} are all of the form F (u_{1} … u_{n}) where F is an output variable or a non-constructor function symbol, and the u_{i} are constructor terms. This is called the constructor discipline. The right-hand sides s_{i} may contain input variables, output variables, and arbitrary function symbols from the underlying logic. We consider LL_{tr} as the logic programming language specified in this way, that is, the set of term-rewriting programs. The inference rule is replacement of equals by equals left to right, which is computable, and the interface language is the set of equations of the form F (s_{1} … s_{n}) = t where s_{1} … s_{n} and t are constructor terms and F is a program variable or a function from the underlying logic.

Theorem 8.17 The language LL_{tr} is P L-adequate.

Proof. The points 1 and 2 are immediate. For 3, we have non-overlapping because the output variables of the hypotheses L_{1} and L_{2} are distinct. For point 4, we need to add a rule F (x) = t[F, G](x), which is allowed because F is an output program variable. For point 5, we can have the system Y = a.

□

We note that this implies, that if in a P L-proof, the assumptions are implemented by LL_{tr} programs, then we can effectively obtain an LL_{tr} program implementing the conclusion. This requires, among other things, that the term-rewriting systems implementing the assumptions be orthogonal, and then guarantees that the system implementing the conclusion will be orthogonal. These systems implementing the assumptions will often compute functions in the underlying logic (such as addition, multiplication, et cetera). At the lowest level, we can assume that the constructors and destructors are computable, and also a conditional function that tests the top-level constructor of a term. It is easily verified that these functions are in fact computable for reasonable representations of terms; however, nontermination has to be handled propery, as indicated below. Then other functions can be defined in terms of these basic functions. We also note that all derived LL_{tr} programs will have at most one rule of the form Y_{i}(u_{1} … u_{n}) = s for each output variable Y_{i}, and for such a rule, u_{1} … u_{n} will be distinct variables, assuming that the systems implementing the hypotheses also have this property. The reason is that such rules can only be introduced by the functional composition rule, and all transformations preserve this property. There may be two or more rules r_{i} = s_{i} for which all r_{i} have the same top-level symbol F from the underlying logic, however.

Theorem 8.18 For R(X; Y) in LL_{tr}, R_{→}(X; Y) is confluent. Also, parallel- outermost rewriting will compute a normal form, if one exists. Furthermore, if F is an output variable and u_{1} … u_{n} are constructor terms and t is a constructor term and the equation F (u_{1} … u_{n}) = t is a logical consequence of R(X; Y) using only equality reasoning, then t is the R-normal form of F (u_{1} … u_{n}), and t can be effectively computed from F (u_{1} … u_{n}).

Proof. R_{→}(X; Y) is confluent because it is orthogonal. For orthogonal systems, parallel-outermost rewriting computes normal forms, if they exist. For the last part, the Church-Rosser property of confluent systems guarantees that t will be the normal form of F (u_{1} … u_{n}), since t is irreducible. Also, t can be effectively computed, since parallel-outermost rewriting is effective.

□

This shows that we can derive a certain portion of the input-output relation of the function F, in fact, its entire interface. However, this is still unsatisfactory, because it is related not to the final specification of F, but rather to the logic program R, which is constructed without the user’s control or possibly even without his or her knowledge. We would rather relate the computability of F to the derived specification of F. That is, if we prove [R : X → Y]A, we would rather relate the computability of Y to the specification A instead of to R. We know that R ⊃ A; if in fact A ⊃ R also, then A and R are equivalent, and all equational consequences of R are also consequences of A. This implies that all equational consequences of R of the form F (u_{1} … u_{n}) = t as above, are also consequences of A. Most of the rules of P L_{prog} actually preserve equivalence, but some of them do not. This corresponds to the fact that the program R may give more information than the specification. Another case of interest is when all the reasoning in the proof of [R : X → Y]A is equational; then any equational consequence of A is also an equational consequence of R, and is therefore derivable from R by rewriting. However, it still may be possible to derive extra consequences from R that are not derivable from A. If the specification of A is complete, then we know that there is essentially only one computable function (or sequence of functions) satisfying A, so R and A are equivalent (with respect to the interface), and elements of the interface of R are consequences of A. However, it is possible that the underlying logic permits many interesting consequences of R to be derived by non-equality reasoning, which we may miss.

To solve this, we use the theorems about completeness and extensibility given earlier. For this we need to show how to extend the interface of a term-rewriting system to a function satisfying the equations in the system. A problem is that for some u_{1} … u_{n}, F (u_{1} … u_{n}) may have no normal form. That is, the computation of F (u_{1} … u_{n}) may not terminate. We need to find a function F′ satisfying the interface, which means that F′(u_{1} … u_{n}) has to have a value and these values need to be chosen to satisfy R. We can partially solve this by adding a ⊥ element and the equation x ≠ ⊥ ⊃ ⊥ <_{d} x. However, just representing all such F (u_{1} … u_{n}) by ⊥ won’t do, because sometimes they can behave differently in some contexts. For example, F (u_{1} … u_{n}) may compute an infinite list of integers, and it may be possible to extract the third element of this list. This infinite list program is, incidentally, an example of a nonterminating program that our formalism can handle. A program to generate such an infinite list can be implemented for example by the term-rewriting system list(n) → cons(n, list(s(n))), which could easily be generated in our system. Two different such infinite lists (say, list(0) and list(1)) may have different third elements, and thus cannot be both equal to “bottom,” even though they both fail to terminate. Another solution is just to consider terminating systems; this doesn’t suffice because many natural definitions (for example of the factorial function) correspond to non-terminating systems.

One solution is to consider restricted evaluation strategies, such as innermost rewriting ; this amounts to ensuring strictness. Let T (F, X) be the set of terms over a set F of function symbols and a set X of variables. Then we consider the flat domain T (F, X) ∪ {⊥}, and the programs are then continuous (strict) functions from this domain to itself. The program construction functions are then continuous functions from a tuple of such program domains to a program domain. Strictness of programs requires, for example, that if-then-else always evaluates all of its arguments, leading to undesired nontermination. This means also that the destructors arg_{i} no longer satisfy the equation arg_{i}(f(x_{1}, …, x_{n})) = x_{i}, since if some x_{j} is ⊥ then f(x_{1}, …, x_{n}) = ⊥; instead we can only say that f(x_{1}, …, x_{n}) ≠ ⊥ ⊃ arg_{i}(f(x_{1}, …, x_{n})) = x_{i}. Similary, the test top f(t) whether the top level function symbol of t is f no longer satisfies top f(f( …)) = true; instead we have f( …) ≠ ⊥ ⊃ top f(f( …)) = true. Also, we can now only say that f ≠ g∧g( …) ≠ ⊥ ⊃ top f(g( …)) = false. As mentioned above, this corresponds to a restriction on the derivation relation ⊢_{LL} and allows more models; we take flat domains and require all functions to be strict. This has the effect of allowing more rules in the underlying logic (for example, f( …, ⊥, …) = ⊥). This works, but results in assigning too many terms a value of “bottom” that have defined values when non-strict computation is used.

Yet another idea is to use a reduction strategy which evaluates f(u_{1} … u_{n}) carefully; only some of the arguments are chosen for evaluation (depending on f and on the results of previous evaluations), but whenever an argument is selected, it is evaluated all the way to normal form. This makes all nonterminating terms equivalent, which corresponds to a flat domain but with non-strict functions allowed. Thus the program domains would contain continuous functions from tuples of T (F, X) ∪ {⊥} to itself, and the program construction functions would contain continouus functions from tuples of program domains to a program domain. Again, this corresponds to a different derivability relation ⊢_{LL} and influences the semantics. Since the domains are flat, we can use the rule x < y ⊃ x = ⊥ in the underlying logic, for example. However, the function programs cannot be assumed to be strict. This approach permits a reasonable number of functions (including those involving conditionals) to be computed without undesirable nontermination. For this, we evaluate if-then-else in a reasonable way, with the first argument evaluated to normal form, then reducing the whole to one of the two remaining arguments. Thus we have the equations if(true, y, z) = y (even if z = ⊥) and if(false, y, z) = z (even if y = ⊥). For other functions with specialized evaluation strategy, corresponding equations can be added to the underlying logic. In addition, the domain structure is fairly simple. However, some of the flexibility of lazy evaluation is lost.

A further solution is to consider the values in a non-flat domain, and construct the values of non-terminating computations by (non-strict) least fixpoints. Maybe there are other solutions too. This solution works for term-rewriting systems of the kind we are considering; the semantics is given in terms of infinite terms containing occurrences of “bottom” and ordered so that s >_{d} t if t is obtained from s by replacing some set of subterms by ⊥. Thus f(a, b, c) >_{d} f(a, ⊥, c). For this, we can add the following equations to the underlying logic, for all constructors f:

arg_{1}(f(x_{1}, …, x_{n})) = x_{1}
arg_{2}(f(x_{1}, …, x_{n})) = x_{2}
…
arg_{n}(f(x_{1}, …, x_{n})) = x_{n}
f(x_{1} … x_{n}) = f(y_{1} … y_{n}) ⊃ x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n}
f( … ⊥ …) ≠ ⊥
f ≠ g ⊃ f( …) ≠ g( …)
top f(f( …)) = true
f ≠ g ⊃ top f(g( …)) = false
x >_{d} y ⊃ f( … x …) >_{d} f( … y …)

Given a term s, we can define bot(s) to be s with all maximal subterms f(t_{1}, …, t_{n}) for all non-constructors f, replaced by ⊥. Then one can show that {bot(t) : s →^{∗} t} has a least upper bound, a possibly infinite term which may contain constructors and occurrences of ⊥, which can be taken as the semantics of s. The reason that this least upper bound must exist is that confluence implies that if some t has a constructor in a given position, then no other t can have a different constructor there. In fact, to make the computation easier, we can use the least upper bound of {bot(t) : s →_{po}^{∗} t} where →_{po} indicates parallel outermost reduction. This is computable, as required, since if there is a constructor at a given position in this least upper bound, eventually a term will be generated having that constructor there, and if there is an occurrence of ⊥ somewhere, then the search for this constructor will not terminate (or will terminate with a term having a non-constructor symbol at that position). Also, we can show that the semantics of f(t_{1} … t_{n}) is a function of the semantics of t_{1} … t_{n}; this is true because the constructor condition implies that the only parts of the t_{i} that can be “seen” by the computation of F are the constructors that eventually emerge at the top. We therefore need to define the domain as the set of such infinite terms, and show how f(t_{1} … t_{n}) is defined when t_{i} are also infinite terms; this can be done by assuming f is continuous. As before, this gives us a domain for the programs; they are continuous functions from tuples of such infinite tree domains, to an infinite tree domain. Then the program construction functions are continuous functions from tuples of program domains to a program domain.

This influences the underlying logic; for example, we can now assume that f(x) ≠ x for a constructor f and all x. This axiom is not satisfied by flat domains. In this way, we obtain that the computed function F′ satisfies the logic program R. Then we have that all logical consequences of A of the form F (u_{1} … u_{n}) = t, for constructor terms u_{i} and t, are true of F′ too, that is, F′(u_{1} … u_{n}) = t, so this can be computed by term-rewriting using parallel outermost rewriting. For this it is necessary to assume that the models of the underlying logic are rich enough to express such infinite tree semantics for R. Seen another way, we have to insure that the axioms of the underlying logic are satisfied by such a semantics. We note that if the wrong underlying logic is chosen, then unsound consequences can be derived; for example, if we assume that the domain is flat, then all but finitely many elements of the sequence ⊥, cons(0, ⊥), cons(0, cons(1, ⊥)), … must be equal. Using cdr(cons(x, y)) = y and car(cons(x, y)) = x, we have that ⊥ = cons(i, cons(i + 1, …)), so car(⊥) = i, and this must hold for infinitely many i (an obvious impossibility). If A is complete, then we know that parallel outermost rewriting will only compute consequences of A. Thus we can completely characterize which equations of the form F (u_{1} … u_{n}) = t can be computed by R with parallel outermost rewriting (exactly the underlying logical consequences of A).

8.6 Horn clause logic programming

We now give an example of a logic programming language based on Horn clauses. A Horn clause logic program is a conjunction of Horn clauses L :– L_{1} … L_{n}, where each L and L_{i} are positive literals of the form eval(s, t) for terms s and t, or of the form s = t. Input and output program variables may appear in s and t. The interface is statements of the form f(s_{1} … s_{n}) = t for constructor terms s_{i} and t. The inference rule ⊢_{LL} is SLD-resolution. Examples of clauses in this language are

eval(plus(s(x),y),s(z)) :– eval(plus(x,y),z). eval(plus(0,y),y).

The intuition is that eval(s, t) is evaluating a term s to the value t. The literals s = t are not used in the computation, but rather to insure P L-adequacy. We need to show P L-adequacy. For this, we need to show that if t[F, G] is a term involving functional program variables F, then there is a logic program L[G; F] such that L[G; F] ⊧_{UL} (∀x)F (x) = t[F, G](x). We can take the logic program

eval(F(x),z) :– eval(t[F,G](x),z). x = y :– eval(x,y). F(x) = t[F,G](x).

The first clause implements outermost rewriting to evaluate F (x). The last clause does not enter the computation at all. The middle clause answers queries of the form F (s_{1} … s_{n}) = t, and therefore serves a computational purpose in generating the interface. We also need to show that for all progam sorts, there is a logic program L(; Y) with one output variable Y and no input variables, implying Y = a for some computable a of the appropriate sort. For this we can use the following logic program: eval(Y,z) :– eval(a,z). eval(a,a).

This is enough for P L-adequacy. We can implement a conditional as follows, avoiding unnecessary evaluations, and permitting the computation of non-strict functions:

eval(if(x,y,z),w) :– eval(x,xv), eval(if2(xv,y,z),w). eval(if2(true,y,z),w) :– eval(y,w). eval(if2(false,y,z),w) :– eval(z,w).

For constructors F and constructor constants c we would have

eval(f(x1 … xn),f(y1 … yn)) :– eval(x1,y1), …, eval(xn,yn). eval(c,c).

We can also implement destructors as follows:

eval(arg1(f(x1 … xn),x1)). eval(arg2(f(x1 … xn),x2)). …

Finally, we can test for the top level constructor of a term as follows:

eval(top f(f(x1 … xn), true)). eval(top f(g( …)), false). …

This is enough to build up other computable functions. The clauses as given here evaluate a term by repeatedly rewriting at the top level until a constructor term appears, and then recursively evaluating the arguments, or else a non-constructor symbol from the underlying logic appears at the top level, for which a customized program does the evaluation. Since Horn clause style programming is very expressive, it should not be hard to see how arbitrary programs can be written. What our approach adds is an automatic way to generate such logic programs from a proof.

We note that the generation of Horn clause programs as given here is weaker than the term-rewriting translation with parallel outermost rewriting. For example, to evaluate or(s, t), the Horn clause translation would have to pick an order in which to evaluate s and t. It might choose s first, which nonterminates, while t may evaluate to true. The term-rewriting approach could evaluate both s and t in parallel. We can give a direct implementation of disjunction (“or”) as follows:

eval(or(x,y),true) :– eval(x,true). eval(or(x,y),true) :– eval(y,true). eval(or(x,y),false) :– eval(x,false), eval(y,false).

This can be made to evaluate both x and y in parallel, if some complete theorem proving strategy is applied (such as breadth-first search). Similarly, the other logical connectives can be implemented; for example, we have

eval(not(x),true) :– eval(x,false). eval(not(x),false) :– eval(x,true).

As for extensibility, it is known [22] that the deductive and least model semantics of Horn clauses agree. This is a partial answer to the question. However, this does not completely settle the issue, because we are looking for a semantics of the function symbols that satisfy the logic program (including the given equations). The typical logic programming semantics interprets the function symbols syntactically, that is, as constructors. However, as shown above, with the existence of fixpoints this requires that the model contain infinite terms, which are not in the standard least model of a set of Horn clauses. Therefore it is necessary to define the semantics in terms of infinite trees; another possibility is to use a flat domain and give up the identity f(x) = f(y) ≡ x = y or the rule f(x) ≠ x for constructors f. Of course, this restricts the evaluation strategies that can be used to compute such functions. Another possibility is to say that the constructors are not computable; this formally solves the problem, but is intuitively unsatisfying and also makes extensions of the language difficult. As for evaluation strategies, note that depth-first search as usually done in Prolog is incomplete, so a better (but slower) search method is needed in general to guarantee that all formulae in the interface can be generated. The translation as defined above, however (except for the implementation of “or”), will work for depth-first search with any ordering of the clauses and literals because of the absence of nondeterminism in the resulting Horn clause program. That is, depth-first search gives an operational semantics permitting the same interface to be generated as by a complete breadth-first search.

In general, for Prolog it is convenient to consider predicates as mappings from tuples of ground terms to {true,false}, with false identified with ⊥. This turns out to be reasonable, because it is possible to enumerate the true literals P (t_{1}, …, t_{n}) in the minimal model of a set of Horn clauses. If such a literal is true, that can eventually be detected, but if it is false, the search may not terminate, which corresponds to ⊥. Then the predicates can be seen as continuous functions from the set of ground terms (with ⊥) to {⊥, true}, and the program construction functions can be taken as continuous functions from tuples of such program domains, to a program domain. This does not treat the constructors as computable; this can be remedied by interpreting them as strict functions over a flat domain of ground terms. One shortcoming of this approach is that it does not distinguish nontermination from finite failure; another is that it does not explicitly consider the answer substitutions returned for a non-ground query. But the purpose is just to sketch how our general framework can be applied to Horn clause logic programming, and not to give an exhaustive account.

One interesting feature of the logic programming approach is that it permits nondeterminism. We can allow a “choice” operator where choice(x, y) can evaluate to either x or y. This can be implemented in Prolog as follows:

eval(choice(x,y),z) :– eval(x,z). eval(choice(x,y),z) :– eval(y,z).

Of course, to show extensibility, it now becomes necessary to use some kind of a nondeterministic denotational semantics.

This approach does not fully exploit the power of Prolog, since the programs derived are of a very special form. It would be interesting to find other P L-adequate logic programming languages based on Horn clauses. One possibility would be to look at methods of compiling concept description languages such as the KL-ONE system of [7] into Horn clauses.

8.7 von Neumann machines

The Horn clause implementation can be made to look a lot more like a von Neumann language. The “logic programs” in this case are sequences of procedure definitions, in which the program variables appear as the names of the procedures. A formal semantics would interpret these programs as state transformations. For this, we assume that terms on right-hand sides of assignment statements are evaluated, but the actual parameters to procedures are not evaluated and that the statement “return(y)” does not evaluate y (in order to make the structure of the computation more explicit). We mostly use innermost (normal order) evaluation; this means that the computation rule is less powerful than lazy evaluation. However, we are more careful about evaluating the arguments of “If,” permitting a little more flexibility and some non-strict functions. We obtain programs then as follows:

procedure F(x1, ..., xn) % assume F(x1 ... xn) = G(t1 ... tm) y1 ← t1(x1 ... xn); y2 ← t2(x1 ... xn); … ym ← tm(x1 ... xn); y ← G(y1, …, ym); return(y)

end F;

procedure A(x);

return(a) end A;

procedure If(x,y,z); x1 ← x; if x1 = true then y1 ← y; return(y1) else z1 ← z; return(z1)

end If;

procedure f(x1, ..., xn) % assume f is a constructor y1 ← x1 ; y2 ← x2 ; … yn ← xn ; return f(y1, ..., yn)

end f;

…

Of course, it should be possible to directly generate reasonably efficient programs in machine language, too.

8.8 Lambda calculus

We now briefly give a logic programming language based on the lambda calculus. For this, the logic programs L(X; Y) are conjunctions of equations of the form Y_{i} = α_{i} where Y_{i} is a program variable and α_{i} is a lambda calculus term, possibly containing variables from X, functions from the underlying logic, and applications of a fixpoint operator μx.t(x) which returns a value y such that t(y) = y. We prefer a μ operator to the lambda term (λx.t(xx))(λx.t(xx)) since the latter seems difficult to type. To show P L-adequacy, for point 2 we have initially L[X, U; Y, Z] of the form (∧_{i}Y_{i} = α_{i}(X, U)) ∧ (∧_{j}(Z_{j} = β_{j}(X, U))). We have L[X; Y, Y, Z] then as ∧_{i}(Y_{i} = α_{i}(X, Y))∧(∧_{j}(Z_{j} = β_{j}(X, Y))). We can eliminate the occurrences of Y from the α_{i} and β_{j} by a sequence of introductions of the μ operator. For example, from Y_{1} = α_{1}(X, Y_{1}, …, Y_{n}) we can obtain that Y_{1} = μW.α_{1}(X, W, Y_{2}, …, Y_{n}) and then replace all occurrences of Y_{1} by μW.α_{1}(X, W, Y_{2}, …, Y_{n}). Repeated applications of this idea eliminate all the Y_{i}, giving us M[X; Y, Z] as required. We need to show that there exists a constructible h : P C → P C such that for all F and G in P C, if (F, G) ⊧ L then (H(F), G) ⊧ M. This H is obtained by a sequence of fixpoint operations, as indicated above, and these produce another function in P C by properties of programming structures. For point 4 we have the equation G = t[F]. For point 5, we have the equation Y = a. The inference mechanism is α, β, and η reduction of the lambda calculus, together with the rule μx.t(x) = t(μx.t(x)). These inference rules are sound, by properties of P C.

The interface is equations of the form (Y_{i}s_{1} … s_{n}) = t, where s_{i} and t are lambda terms containing the fixpoint operator and possibly constants from the underlying logic. It looks like we could show extensibility by letting μ be a leastfixpoint operator, which guarantees that the specified functions are the least functions satisfying their definitions, and thus are in some sense “initial.” Of course, this would require the existence of an appropriate domain structure with least-fixpoints.

We should also assume that functions to compute constructors, destructors, and test for the top constructor symbol are available; this can be done by including some function constants for these functions with the corresponding equations for computing them. Or else this can be done by a suitable encoding into the lambda calculus itself. This lambda calculus approach has some similarity to LISP, and so it might be possible to extend it in that direction. This might give us an approach based on a von Neumann-style architecture, since LISP has efficient implementations on such architectures. Also, the equations Y_{i} = α_{i} are remeniscent of assignment statements.

8.9 Derived rules of inference and efficiency

We now go back to the derived rule of inference from section 7.1 and show how it could be realized for term-rewriting systems. We then give a general technique by which such derived rules of inference, with customized logic programs, may be proven correct. Recall that the point is to find more efficient realizations of derived rules of inference, when possible. The rule in question is the following:

\frac{[→ S]P (S, 0) [→ X](∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1))}{[→ Y](∀n)(n ≥ 0 ⊃ P (Y (n), n))} (It_{1})

From the given proof of this rule we obtain a term-rewriting system something like this:

S → …  (rules for computing S)
X(w) → …  (rules for computing X)
Y (n) → (if n = 0 then S else X(Y (n − 1))) (from the proof)

However, we can also use the following system to realize this inference rule:

S → …  (as above)
X(w) → …  (as above)

Y (n) → F (S, n) F (z, s(v)) → F (X(z), v) F (z, 0) → z

This uses an iterative rather than a recursive approach, and also a more efficient representation for n; this may be more efficient than the automatically generated program. And of course for more complicated inference rules, the savings obtained by customizing the programs could be much greater, allowing increased efficiency within the framework of a reliable program generation method. Of course, it is also necessary to prove the correctness of the customized program.

We now expand on this, and give a systematic method for proving the correctness of such customized programs.

Theorem 8.19 A computable mapping G : L_{1} … L_{n} → L from logic programs to logic programs realizes an inference rule

\frac{[X_{1} → Y_{1}]A_{1} … [X_{n} → Y_{n}]A_{n}}{[X → Y]A}

if the following inference rule is derivable in PL:

\frac{[X_{1} → Y′_{1}]L_{1} … [X_{n} → Y′_{n}]L_{n}}{[X → Y′]G(L_{1} … L_{n})}

and if the following formula is valid in PL:

((∀X_{1}Y′_{1})(L_{1} ⊃ A_{1}) ∧ … ∧ (∀X_{n}Y′_{n})(L_{n} ⊃ A_{n})) ⊃ (∀XY′)(G(L_{1} … L_{n}) ⊃ A).

Here we assume that Y′_{i} are the output variables of L_{i}, and Y′ are the output variables of G(L_{1} … L_{n}), and Y_{i} ⊂ Y′_{i} for all i, and Y ⊂ Y′.

Proof. We need to show that if L_{i} implements [X_{i} → Y_{i}]A_{i} for all i, then G(L_{1} … L_{n}) implements [X → Y]A. For this, we need to show that there is a computable F such that for functions F_{1} … F_{n} in the program domains satisfying A_{1} … A_{n}, respectively, if F_{i} satisfies L_{i} for all i then F satisfies G(L_{1} … L_{n}). But this is just what is guaranteed by the above inference rule. We also need to know that if (∀X_{i}Y′_{i})(L_{i} ⊃ A_{i}) for all i, then (∀XY′)(G(L_{1} … L_{n}) ⊃ A). This is guaranteed by the above P L formula. Note that the proof of the inference rule given above, will automatically generate another logic program; however, this program is not necessarily the one that is wanted.

□

For our example, we prove the following annotated inference rule:

\frac{[L_{1}(S) :→ S]P (S, 0) [L_{2}(X) :→ X](∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1))}{[L_{1}(S) ∧ L_{2}(X) ∧ L_{3}(F, X, Y, S) → Y](∀n)(n ≥ 0 ⊃ P (Y (n), n))} (It_{1})

where L_{3}(F, X, Y, S) is the following term-rewriting system:

Y (n) = F (S, n) F (z, s(v)) = F (X(z), v) F (z, 0) = z

That is, these are equalities which are executed as rewrite rules. Here F, X, Y, and S are all output variables. According to the preceding theorem, in order to prove the correctness of this annotated inference rule we need to derive the following in P L:

\frac{[→ S]L_{1}(S) [→ X]L_{2}(X)}{[→ F, X, Y, S]L_{1}(S) ∧ L_{2}(X) ∧ L_{3}(F, X, Y, S)}

For this, we derive [F, S → Y]Y (n) = F (S, n) by the functional composition rule with individual functions. We derive [X → F]F (z, w) = ( if W = 0 then Z else F (X(z), w − 1)) by the functional compositional rule with recursion and individual functions. We then need to do a derivation of the following form to put everything together:

\frac{[→ S]L_{1}(S) [→ X]L_{2}(X) [X → F]L′_{3}(F X) [F, S → Y]L′′_{3}(F, S, Y)}{[→ F, X, Y, S]L_{1}(S) ∧ L_{2}(X) ∧ L′_{3}(F, X) ∧ L′′_{3}(F, S, Y)}

This can be done by repeated application of the following inference rule:

\frac{[X → Y]A [Y, W → Z]B}{[X, W → Y, Z]A ∧ B} (assuming X, Z and W, Y disjoint)

This inference rule can be proven as follows:

1. [X → Y]  A[X, Y]  (given)
2. [Y, W → Z]  B[Y, W, Z]  (given) (note that Y, Z and W, Z are disjoint)
3. [V, W → Z]  B[V, W, Z]  (renaming, 2) (so that V, Z are disjoint)
4. [X, V, W → Y, Z] A[X, Y] ∧ B[V, W, Z] (combination rule)

(Y, Z and X, Z and V, Y and W, Y disjoint)

5. [X, W → Y, Z]  A[X, Y] ∧ B[Y, W, Z] (recursion rule)

We also need to show that the following formula is valid in the underlying logic:

((∀S)(L_{1}(S) ⊃ A_{1}) ∧ (∀X)(L_{2}(X) ⊃ A_{2}))
⊃ (∀F XY S)(L_{1}(S) ∧ L_{2}(X) ∧ L_{3}(F, X, Y, S) ⊃ A)

where A_{1} is P (S, 0), A_{2} is (∀n)(∀w)(n ≥ 0 ∧ P (w, n) ⊃ P (X(w), n + 1)), and A is (∀n)(n ≥ 0 ⊃ P (Y (n), n)). This can be done by an induction on n.

9 Examples of Underlying Logics

We have seen examples of programming languages for P L, and in the process have observed some connections between the evaluation strategy, the derivability relation ⊢_{LL}, the semantics, and the underlying logic. The only place where the underlying logic enters the system is the underlying logic rule, so the derivability relation ⊢_{UL} needs to be chosen so that this rule is sound, and this is a function of the semantics. In particular, this depends on the choice of a semantics for P C. Generally, we choose the rest of the logic to be something like the usual language of mathematics (e.g., ZF), so the main variation between underlying logics will typically be in the axioms referring to program construction functions. Now we consider more closely some examples of underlying logics. These are often similar to the programming languages just considered. Note that most of the rules of inference of P L are independent of the underlying logic, as long as it obeys the classical first-order laws with respect to quantifiers. So the only rules that need to be checked for specific underlying logics and program domains and the program construction domains P C are the functional composition rules (where assumed) and the recursion rule.

9.1 Partial recursive functions

Consider for example the underlying logic where the domains are the non-negative integers and for each n, we have a program domain of partial recursive functions with n arguments. The set P C can be specified as the recursive mappings from program domains (partial recursive functions) to program domains, where partial recursive functions are encoded as integers according to some enumeration of the partial recursive functions. We assume that the syntax allows arithmetic operations (at least 0, successor, and predecessor), conditionals, first-order quantifiers, definitions of primitive and partial recursive functions, and maybe more. In this underlying logic we may have a number of axioms, including the assumptions that 0, successor, and predecessor are computable. We also assume that the conditional function defined by cond(x, y, z) = (if x = 0 then y else z) is computable. For this underlying logic we would also include the functional composition rules. These are satisfied because the composition of partial recursive functions is partial recursive.

The recursion rule is satisfied because of the recursion theorem. We note however that the recursion theorem is inconvenient for actual programming; there are much simpler ways of constructing partial recursive functions. For example, we can express partial recursive functions by means of a first-order term-rewriting system, and then one can get the effect of recursion by adding a recursive call as shown in section 8.2.

As an example, we derive other partial recursive functions and show their correctness. For example, we can derive the function F (x, y) defined by (if (x = y) then 1 else 0) as follows:

1. [→ F]  (∀x, y, z)(x = 0 ⊃ F (x, y, z) = y) ∧ (x ≠ 0 ⊃ F (x, y, z) = z)

assumption)

2. [→ F]  (∀x)(F (x) = x + 1)

(assumption)

3. [→ F]  (∀x)(F (x) = x − 1)

(assumption)

4. [→ X]  (X = 0)

(assumption)

5. [X, F, H, K, G′ → G] (∀xy)(G(x, y) = F (x, F (y, H(X), X), F (y, X, G′(K(x), K(y)))))

(functional composition)

6. [G′ → G] (∃XF HK)(∀xyz)(X = 0 ∧ F (x, y, z) = (if x = 0 then y else z)

∧h(x) = x + 1 ∧ K(x) = x − 1

∧(G(x, y) = F (x, F (y, H(X), X), F (y, X, G′(K(x), K(y)))))) (renaming rule and several applications of the program composition rule)

7. [G′ → G] (∀x, y)G(x, y) = (if x = 0 then (if y = 0 then 1 else 0)

else if (y = 0 then 0 else G′(x − 1, y − 1)))

(underlying logic rule)

8. [→ G]  (∀Xy)G(x, y) = (if x = 0 then (if y = 0 then 1 else 0) else

if (y = 0 then 0 else G(x − 1, y − 1)))

(recursion rule)

9. [→ G]  (∀Xy) (x = y ⊃ G(x, y) = 1 ∧ x ≠ y ⊃ G(x, y) = 0)

(underlying logic rule)

We now show the programs (expressed as term-rewriting systems over the nonnegative integers) for each of the above steps except applications of the underlying logic rule, which do not affect the term-rewriting system:

1. F_{1}(0, y, z) → y
F_{1}(s(x), y, z) → z
2. F_{2}(x) → s(x)
3. F_{3}(s(x)) → x
4. X → 0
5. G(x, y) → F (x, F (y, H(X), X), F (y, X, G′(K(x), K(y)))))

6. G(x, y) → F_{1}(x, F_{1}(y, F_{2}(X), X), F_{1}(y, X, G′(F_{3}(x), F_{3}(y)))))
F_{1}(0, y, z) → y
F_{1}(s(x), y, z) → z
F_{2}(x) → s(x)
F_{3}(s(x)) → x
X → 0
8. G(x, y) → F_{1}(x, F_{1}(y, F_{2}(X), X), F_{1}(y, X, G(F_{3}(x), F_{3}(y)))))
F_{1}(0, y, z) → y
F_{1}(s(x), y, z) → z
F_{2}(x) → s(x)
F_{3}(s(x)) → x
X → 0

The above step shows how the recursion rule affects the program; the call to G′ is replaced by a recursive call to G. We note that programs expressed as termrewriting systems in this way are fairly efficient to execute in many cases. Although this program uses the successor notation, it would be possible to use a more efficient representation for the integers. There are also possibilities for concurrency as in any functional programming language. We can optimize this program by eliminating occurrences of F_{2} and X to obtain the following program:

G(x, y) → F_{1}(x, F_{1}(y, s(0), 0), F_{1}(y, 0, G(F_{3}(x), F_{3}(y)))) F_{1}(0, y, z) → y F_{1}(s(x), y, z) → z F_{3}(s(x)) → x

This generation of term-rewriting systems has already been formalized in a more general context in section 8.5.

The following theorem is evidence that the recursion mechanism of P L is powerful enough to capture computable recursions.

Theorem 9.1 Suppose f is a partial recursive function, extended so that f(x) = ⊥ if f does not terminate on input x. Then the following is deriviable in P L with underlying logic as given above, and with the least fixpoint and first functional composition rule::

[→ F](∀x)(F (x) = f(x))

Proof. By induction on the length of the definition of f as a partial recursive function. We can imitate recursion, composition, and the minimization operator by appropriate inference rules in P L, especially the least fixpoint rule and the first functional composition rule.

□

9.2 Lambda calculus

Another example would be typed lambda calculus with the μ (least fixpoint) operator. Here the program domains would be continuous mappings from integers (with ⊥) to integers, and higher sorts based on it. We would need a domain structure for the sorts. The program construction functions P C would be mappings from program domains to a program domain. The syntax of the logic would have typed lambda calculus terms with the μ operator, integers (i.e., zero, successor, and predecessor), the equality predicate, and maybe more. We would interpret the logic in the usual way, with application in the lambda calculus interpreted as functional application on the domains. Also, we interpret μ(x)A to be the least x (in the domain ordering) such that Ax = x. Note that this always exists if the domain has certain necessary properties, since we can take the least upper bound of A^{i}(⊥). The μ operator guarantees the fixpoint property. In fact, in this case one can use the least fixpoint rule. We can also use the functional composition rules; they are sound because one can compose lambda terms in the lambda calculus.

9.3 Horn clause logic programming

For pure Prolog (sets of Horn clauses) interpreted as in first-order logic, we might have the following “fixpoint” rule:

[L → P](Horn(L) ⊃ (for all terms x)([(∀y)L ⊢_{F OL} q(x)] ≡ P (x)))

where Horn(L) means L is a set of first-order Horn clauses and ⊢_{F OL} represents derivability in first-order logic and y = y_{1} … y_{n} are the variables in L and q is some predicate in L and x = x_{1} … x_{m} are variables in the query. This says that there is a program to compute logical consequences of sets of Horn clauses. Such a computation may fail (or fail to terminate) on inputs for which P is false; since we haven’t formally specified what it means to compute P, this is permissible. The execution mechanism would have to be some complete inference method such as breadth-first search or depth-first iterative deepening; Prolog’s depth-first search would not work because it is incomplete. Now, suppose we have a specific logic program L expressing membership in a list:

[A → L]Horn(L) ∧ (for all terms x)[(∀y)L ⊢_{F OL} member(x)] ≡ x ∈ list(A)

Here list(A) is a list and A is a program that outputs this list. A can be for example a functional program that outputs the desired list, or a program which, given an integer i, gives the i^{th} element of a list. Then, from this rule and the above Prolog fixpoint rule, we can obtain the following by an application of program composition:

[A → P](∃L)(Horn(L) ⊃ (for all terms x)([(∀y)L ⊢_{F OL} member(x)] ≡ P (x))

∧Horn(L) ∧ (for all terms x)([(∀y)L ⊢_{F OL} member(x)] ≡ x ∈ list(A)))

By an application of the underlying logic rule we obtain

[A → P](P (x) ≡ x ∈ list(A))

Thus by a roundabout route we have constructed a proof, which can be effectively converted into a program that will test for membership in a list list(A). This program would execute by applying some general inference mechanism or complete execution strategy to the set of Horn clauses expressing membership in a list.

We now give a couple of more examples of programs in different formalisms. It would also be interesting to do this for the unification algorithm.

9.4 Derivation of Factorial program

We now show how a proof corresponding to the factorial function can be derived in this system, where the underlying logic is assumed to be the partial recursive functions, with initially only a few functions assumed to be computable. In particular, we start out with the assumptions that a conditional function, the constants 0 and 1, subtracting one, and multiplication are computable. Using the functional composition rule with individual functions we obtain the formula 1. [X_{1} → Y](∀x)(Y (x) = if x = 0 then 1 else x ∗ X_{1}(x − 1)))

Now using the underlying logic rule we obtain

2. [X_{1} → Y](∀n)((∀x)(0 ≤ x ≤ n − 1 ⊃ X_{1}(x) = fact(x)) ⊃ (∀x)(0 ≤ x ≤ n ⊃ Y (x) = fact(x)))

Using the recursion rule we obtain

3. [→ Y](∀n)((∀x)(0 ≤ x ≤ n − 1 ⊃ Y (x) = fact(x)) ⊃ (∀x)(0 ≤ x ≤ n ⊃ Y (x) = fact(x)))

Using the underlying logic rule (mathematical induction) we get

4. [→ Y](∀x)(0 ≤ x ⊃ Y (x) = fact(x))

This is a specification of the factorial function, with individual functions for the zero test, multiplication, decrementing by one, and the conditional test. Assuming the use of term-rewriting systems to express the underlying programs as above, we obtain the following sequence of programs:

1. Y (x) → (if x = 0 then s(0) else x ∗ X_{1}(x − 1))

… definition of multiplication … (if 0 = 0 then y else z) → y (if s(x) = 0 then y else z) → z s(x) − 1 → x

(The definitions of multiplication etc. come from the assumptions that these are computable. These are by-products of the derivation of the functional composition rule with individual functions.)

3. Y (x) → (if x = 0 then s(0) else x ∗ Y (x − 1))

… definition of multiplication … (if 0 = 0 then y else z) → y (if s(x) = 0 then y else z) → z s(x) − 1 → x

We note that multiplication could be defined in terms of the successor function, which is rather slow. Or we could substitute a more efficient definition and a more efficient representation of the integers. A sample computation of Y (2) using outermost (lazy) rewriting would be

Y (s(s(0))) → if s(s(0)) = 0 then s(0) else s(s(0)) ∗ Y (s(s(0)) − 1) → s(s(0)) ∗ Y (s(s(0)) − 1) → s(s(0)) ∗ (if s(0) = 0 then s(0) else s(0) ∗ Y (s(0) − 1)) → s(s(0))∗(s(0)∗Y (s(0)−1)) → s(s(0))∗(s(0)∗(if 0 = 0 then s(0) else 0∗Y (0−1))) → s(s(0)) ∗ (s(0) ∗ s(0)) → … → s(s(0)) ∗ s(0) → … → s(s(0)).

The proof could have been obtained faster by a use of the functional composition rule with recursion, as follows:

1. [→ Y] (∀x)(Y (x) = if x = 0 then 1 else x ∗ Y (x − 1))

(functional composition rule with recursion)

2. [→ Y] (∀x)(0 ≤ x ⊃ Y (x) = fact(x))

(underlying logic rule)

If we had instead started with a formula

[X_{1}X_{2} → Y](∀x)(Y (x) = if x = 0 then 1 else X_{2}(x, X_{1}(x − 1))))

we would end up with the formula

[X_{2} → Y]((∀x, y)(X_{2}(x, y) = x ∗ y) ⊃ (∀x)(0 ≤ x ⊃ Y (x) = fact(x)))

The proof of this formula corresponds to the factorial function with the multiplication parameterized. Thus, an arbitrary proof that X_{2}(x, y) = x ∗ y can be substituted to obtain a version of the factorial function, corresponding to the use of an arbitrary procedure for multiplying integers. In this way we obtain a kind of abstract data structures. The program (term rewriting system) corresponding to this formula would have no definition for the function X_{2} and so could not be directly executed.

9.5 Termination

We now sketch how it is possible to reason about termination in this system. For this, we again use the factorial function. We assume that the integers are extended with a “bottom” (⊥) element indicating nontermination and that the functions are defined also on ⊥ in a reasonable way. We show that x ≥ 0 ⊃ Y (x) ≠ ⊥ in the specification of the factorial function. That is, we assume that this statement is added to the specification of the factorial function and attempt to derive a function satisfying this specification. This is done as before, except that this extra assertion is proved using mathematical induction in an application of the underlying logic rule, since Y (0) = 1 and if Y (x) ≠ ⊥ then Y (x + 1) ≠ ⊥. We would like to show that if x < 0 then Y (x) = ⊥. For this, we need to use the least fixpoint rule. Then we consider the function Z(x) defined as (if x < 0 then ⊥ else fact(x)). We show that this is also a fixpoint of the given specification. Therefore the least fixpoint (least in the domain ordering <_{d}) must be no larger. This implies that if x < 0 then Y (x) = ⊥. It should be clear (in principle) how this can be extended to many examples using arbitrary well-founded orderings and arbitrary least-fixpoints of functions, to prove both termination and nontermination.

9.6 Term-rewriting systems

We give an example of a derivation of a program involving term-rewriting systems. Here we are proving properties of term-rewriting systems at a meta-level, instead of using them as the computational mechanism. First we assume the computability of the one-step derivability relation for a term-rewriting system R. By taking a suitable fixpoint, we obtain a program to compute the result of arbitrarily many rewrites. We then show that if R is terminating and confluent, this program computes normal forms. Next we construct a program to decide if s =_{R} t for terms s, t where =_{R} is the underlying equality theory. We use comp reduction(Y) as an abbreviation for the formula (if s is R-irreducible then Y (s) = s else s →_{R} Y (s)).

1. [Y, Z → W] (∀u)(W (u) = Z(Y (u)))

(functional composition)

2. [Y, Z → W] (if s is R irreducible then Y (s) = s else s →_{R} Y (s))

implies (∀u)(W (u) = Z(Y (u)))

(underlying logic rule)

3. [Y → W]  comp reduction(Y) implies (∀u)(W (u) = W (Y (u)))

(recursion rule)

4. [Y → W]  comp reduction(Y) ∧ (R terminating and confluent)

implies (∀u)(W (u) = normal form of u)

(underlying logic rule)

5. [Y → W]  comp reduction(Y) ∧ (R terminating and confluent)

implies (∀u, v)(W (u) = normalformofu ∧W (v) = normalformofv) (underlying logic rule)

6. [Y → W] comp reduction(Y) ∧ (R terminating and confluent)

implies (∀u, v)(W (u) = W (v)) ≡ (u =_{R} v) (underlying logic rule, Church Rosser property)

7. [W → W′] (∀u, v)(W′(u, v) = (if W (u) = W (v) then true else false))

(computability of conditional, assumed)

8. [Y → W′] (∃W)comp reduction(Y) ∧ (R terminating and confluent)

implies (∀u, v)(W (u) = W (v)) ≡ (u =_{R} v)

∧(∀u, v)(W′(u, v) = (ifW (u) = W (v) then true else false)) (composition rule)

9. [Y → W′] comp reduction(Y) ∧ (R terminating and confluent) implies

(∀u, v)(W′(u, v) ≡ (u =_{R} v))

(underlying logic rule)

Thus we have derived a function W′ to decide the equational theory of R, given that R is terminating and confluent and that some one-step rewrite relation is computable.

10 Goal-Directed Derivations

Many program generation systems permit a program to be derived in a systematic way from its specification. We make some general comments about how this can also be done with the current approach. We present a collection of derived inference rules for facilitating goal-directed program generation. These rules may also be useful in a more general context, that is, for arbitrary applications of the logic P L. These rules are not necessarily original with us, just formalized in a different framework. The idea is that we are given a formula A(X, Y) expressing the desired relationship between the inputs X and the outputs Y of the desired program. By backward reasoning, we typically derive a collection of formulae B_{i}(t_{i}(X), Z) and conditions C_{i}(X) such that C_{i}(X) ∧ B_{i}(t_{i}(X), Z) ⊃ A(X, r_{i}(X, Z)). Also, the C_{i}, t_{i},and r_{i} are assumed to be computable. The idea is that we can test C_{i}, and if it is true, recursively compute Z such that B_{i}(t_{i}(X), Z) and then return r_{i}(X, Z) as the output. The B_{i} are then additional specifications that must be computed in a similar way, and hopefully we can obtain enough recursions so that the computation can be carried out. Also, we would like to have that (∀X)(C_{1}(X)∨…∨C_{n}(X)). For our formalism, we introduce a function variable F intended to represent a function computing a value (or sequence of values) F (X) such that (∀X)A(X, F (X)). We then derive the formula [→ F](∀X)A(X, F (X)) in our system, which will construct an F as desired.

10.1 General subgoaling principle

We first give a general scheme for goal-directed program generation based on a specification and properties of a function or program at the top level. We can express this as follows.

Suppose we are trying to prove [→ F](∀x)P (F, x). We can start with the valid formula [G → F](∀x)(P (G, x) ⊃ P (F, x)). Then we can begin a process of subgoaling, working on the leftmost P (G, x) and eventually eliminating it altogether. In general, this process of subgoaling operates as follows: In a formula of the form [Y_{1} … Y_{n} → F](∀x)(B_{1}(Y_{1}, x)∧…∧B_{n}(Y_{n}, x) ⊃ P (F, x)), we regard the B_{i}(Y_{i}, x) as subgoals and attempt to replace them by something simpler and eventually eliminate them. For this we can use the following rule:

\frac{\begin{matrix}[X_{1} → Y_{1}](∀x)A_{1}(X_{1}, x) ⊃ B_{1}(Y_{1}, x) … [X_{n} → Y_{n}](∀x)A_{n}(X_{n}, x) ⊃ B_{n}(Y_{n}, x) \\ [Y_{1} … Y_{n} → F](∀x)(B_{1}(Y_{1}, x) ∧ … ∧ B_{n}(Y_{n}, x) ⊃ P (F, x)) \end{matrix}}{[X_{1} … X_{n} → F](∀x)(A_{1}(X_{1}, x) ∧ … ∧ A_{n}(X_{n}, x) ⊃ P (F, x))} (S_{1})

Here X_{i} and Y_{i} can be single program variables or sequences of program variables. This rule operates on all of the subgoals B_{i} at once, and allows us to replace B_{i} by A_{i}. A special case is when A_{i} is “true”, and then B_{i} is eliminated. Another special case is when A_{i} and B_{i} are identical; then B_{i} is unchanged. We use this rule in a forward direction, but it has the effect of backward reasoning. This can be proven using the composition rule a number of times.

We now give another version of this principle that is related to the underlying logic rule.

\frac{\begin{matrix}(∀x, X_{1})A_{1}(X_{1}, x) ⊃ B_{1}(X_{1}, x) … (∀x, X_{n})A_{n}(X_{n}, x) ⊃ B_{n}(X_{n}, x) \\ [X_{1} … X_{n} → F](∀x)(B_{1}(X_{1}, x) ∧ … ∧ B_{n}(X_{n}, x) ⊃ P (F, x)) \end{matrix}}{[X_{1} … X_{n} → F](∀x)(A_{1}(X_{1}, x) ∧ … ∧ A_{n}(X_{n}, x) ⊃ P (F, x))} (S_{2})

This permits the subgoals B_{i} to be modified according to the rules of the underlying logic, without considering how X_{i} is computed. If A_{i} is true, then B_{i} has been proved in the underlying logic and can be omitted.

10.2 Booleans and computability

Conditional functions are of the form (if P then A else B) where P is a computable predicate. In order to develop rules for conditionals, therefore, we have to consider more closely the relationship between Booleans and computability. To say that a predicate C is computable means that we can compute a function F such that C(x) = f(x) for all X. We abbreviate this by comp(C). We also use comp(f) where f is a function to abbreviate [→ F](F = f), and say then that f is computable. In general, if t is a term containing variables x_{1} … x_{n} then comp(t) abbreviates [→ F](∀x_{1} … x_{n})f(x_{1} … x_{n}) = t. However, this introduces some difficulties in the system. The problem has to do with ⊥ and other such elements that one must add to obtain domains with fixpoints, as required by our fixpoint rule. Any computable function or predicate has to be monotone. That implies that if P (⊥) is true then P (x) is true for all x, and if P (⊥) is false then P (x) is false for all x. Therefore, the only non-trivial predicates are those for which P (⊥) is some element other than true and false, typically ⊥. This means that all of our logical operations must be somehow extended to consider ⊥, and we have to give up the identity (∀x)(P (x) ∨ ¬(P (x))) or else change the meaning of the connectives in some way to cope with ⊥. There is also a problem with conditionals, since (if ⊥ then A else B) is ⊥.

Our solution to this is to separate the logical formalism from the computational formalism. Since computability is already explicitly accounted for by the [X → Y] quantifier, the underlying logic need not be concerned with it. We require that logical connectives and quantifiers only take Boolean values. Program variables, including predicates, may evaluate to non-Booleans like ⊥. We convert from non-Boolean values to Boolean values by means of the functions true(A), false(A), and def(A), defined respectively by A = true, A = false, and (A = true ∨ A = false). We note that these functions are not computable, since true(⊥) = false but true(true) = true, so the function true is not monotone. When a quantifier or logical connective is applied to a non-Boolean, we assume that the function “true” is implicitly applied to the arguments. Note that we have for all A, true(A) ∨ neg(true(A)) but we do not have true(A) ∨ false(A) always. Also note that A ∨ neg(A) holds even if A is computable since this implicitly coerces to true(A) ∨ neg(true(A)). However, comp(A ∧ B) is false if A ∧ B is nontrivial, since A and B are here implicitly converted to Booleans, and thus A ∧ B can nowhere be ⊥.

10.3 Conditional rules

We now specialize the general rules given above to conditionals, since they are common and have special logical properties. We start with a conditional rule corresponding to a program with a conditional at the top. We assume the function if(x, y, z) is computable and satisfies (x = true ⊃ if(x, y, z) = y ∧ x = false ⊃ if(x, y, z) = z).

One plausible (but wrong) conditional rule is

\frac{comp(C) comp(if)}{[G_{1}G_{2} → G](∀x)(C(x) ⊃ G(x) = G_{1}(x)) ∧ (¬C(x) ⊃ G(x) = G_{2}(x))}

This is “proved” by noting that the conditional (if C(x) then G_{1}(x) else G_{2}(x)) satisfies the conclusion and is computable, using the functional composition rule. The problem occurs if G_{1} and G_{2} are both constant functions (say, 0 and 1) and x is ⊥. Then (if C(x) then G_{1}(x) else G_{2}(x)) evaluates to ⊥, so G(x) = G_{1}(x) and G(x) = G_{2}(x) are both false. We fix this rule as follows:

\frac{comp(C) comp(if)}{[G_{1}G_{2} → G](∀x)(C(x) ⊃ G(x) = G_{1}(x)) ∧ (false(C(x)) ⊃ G(x) = G_{2}(x))} (C_{1})

The proof of this corresponds to the construction of the conditional (if C(x) then G_{1}(x) else G_{2}(x)).

Another conditional rule is as follows:

\frac{comp(C) comp(if) [→ G](∀x)(C(x) ⊃ A(G, x)) [→ G](∀x)(false(C(x)) ⊃ A(G, x))}{[→ F](∀x)(def(C(x)) ⊃ A(F, x))} (C_{2})

However, this rule is only sound for A(G, x) of the form A′(G(x), x). To show that this rule is unsound for general A, let C(x) be even(x) (“x is even”) and let A(G, x) be (even(x) ⊃ G(x)G(x−1) < 0∧odd(x) ⊃ G(x)G(x+1) > 0). Now, we can satisfy [→ G](∀x)(C(x) ⊃ A(G, x)) by taking G(x) as (if even(x) then 1 else −

1) and we can satisfy [→ G](∀x)(false(C(x)) ⊃ A(G, x)) by taking G(x) as 1. However, there is no function F satisfying [→ F](∀x)def(C(x)) ⊃ A(F, x), since such a function would have to satisfy G(x)G(x − 1) < 0 and G(x)G(x − 1) > 0 simultaneously for even x. When A depends only on the value of G(x), that is, A is of the form A′(G(x), x) (a common case), then C_{2} can be shown by the functional composition rule, noting that if g_{1} satisfies (∀x)(true(C(x)) ⊃ A(g_{1}, x)) and g_{2} satisfies (∀x)(false(C(x)) ⊃ A(g_{2}, x)) then (if C(x) then g_{1}(x) else g_{2}(x)) satisfies (∀x)(def(C(x)) ⊃ A(F, x)). A slightly stronger form of this rule, suitable for use with the subgoal rule S_{1} given above, is as follows, again assuming that A(G, x) is of the form A′(G(x), x):

\frac{comp(C) comp(if)}{[G_{1}G_{2} → F](∀x)((C(x) ⊃ A(G_{1}, x)) ∧ (false(C(x)) ⊃ A(G_{2}, x)) ⊃ (def(C(x)) ⊃ A(F, x)))} (C_{3})

Here the subgoals are (C(x) ⊃ A(G_{1}, x)) and (false(C(x)) ⊃ A(G_{2}, x)) and the goal is def(C(x)) ⊃ A(F, x). This form of the rule is better when x needs to be remembered for purposes of mathematical induction. From now on we assume that the conditions A(G, x) are all of the form A′(G(x), x) and similarly for B(G, x) and P (G, x) (when used).

10.3.1 A multiple choice conditional rule

From now on we assume comp(if) as a hypothesis for all rules, so this condition is often omitted. We extend the above rule to more than one condition as follows:

\frac{(∧_{i}comp(C_{i})) (∀x)(C(x) ⊃ ∨_{i}C_{i}(x))}{[G_{1} … G_{n} → F](∀x)(∧_{i}(C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)) ⊃ (C(x) ⊃ A(F, x)))}

Assuming the hypotheses, this rule creates subgoals (C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)) of the goal C(x) ⊃ A(F, x); these can be used with the above subgoaling rule. The problem with this rule is that we need to compute which one of the C_{i} is true, for a given X. This can only be done by computing them in parallel and waiting until one of them returns “true.” however, in general, this kind of parallel computation is non-monotonic. We could retain this rule anyway, since we have computability in an intuitive sense, but the non-monotonicity could cause the fixpoint property to be violated for the constructed function F. Therefore we add a hypothesis, and obtain the following rule:

\frac{(∧_{i}comp(C_{i})) (∀x)(C(x) ⊃ ∨_{i}C_{i}(x)) (∧_{i}(C(x) ⊃ def(C_{i}(x))))}{[G_{1} … G_{n} → F](∀x)(∧_{i}(C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)) ⊃ (C(x) ⊃ A(F, x)))} (CM_{1})

Of course this rule also has the following alternative form:

\frac{\begin{matrix}(∧_{i}comp(C_{i})) (∀x)(C(x) ⊃ ∨_{i}C_{i}(X)) \\ (∧_{i}(C(x) ⊃ def(C_{i}(x)))) ∧_{i} [→ G_{i}](∀x)(C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)) \end{matrix}}{[→ F](∀x)(C(x) ⊃ A(F, x))} (CM_{2})

Using the second deduction principle and some logical rewriting, we obtain another form that will be used later:

\frac{\begin{matrix}(∧_{i}comp(C_{i})) (∀x)(C(x) ⊃ ∨_{i}C_{i}(X)) \\ (∧_{i}(∀x)(C(x) ⊃ def(C_{i}(x)))) ∧_{i} [F → G_{i}](∀x)(C(x) ∧ C_{i}(x) ⊃ (B(F) ⊃ A(G_{i}, x))) \end{matrix}}{[F → G](∀x)(C(x) ⊃ (B(F) ⊃ A(G, x)))} (CM_{3})

10.3.2 A rule for term structure and conditionals

The conclusion of the multiple choice conditional rule CM_{1} has subgoals (C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)); used with the subgoaling principle S_{1}, these correspond to assumptions of the form [X_{i} → G_{i}](∀x)(A_{i}(X_{i}, x) ⊃ (C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x))) that permit the subgoal (C(x) ∧ C_{i}(x) ⊃ A(G_{i}, x)) to be replaced by A_{i}(X_{i}, x). We give a rule that can generate such formulas:

\frac{(∀f)(∀x)(A_{i}(f, t_{i}(x)) ⊃ (C_{i}(x) ⊃ A(u_{i}(f, x), x))) comp(u_{i})}{[X → G](∀x)(A_{i}(X, t_{i}(x)) ⊃ (C_{i}(x) ⊃ A(G(x), x)))} (CT_{1})

For example, since we know that (∀f, x)(f(x − 1) = fact(x − 1) ⊃ (x > 0 ⊃ x ∗ fact(x − 1) = fact(x))), we can derive [X → G](∀x)(X(x − 1) = fact(x − 1) ⊃ (x > 0 ⊃ G(x) = fact(x))).

10.4 Functional composition and subgoaling

We now give a rule that permits the elimination of computable functions at the top of an expression. This may be used together with the subgoaling rule S_{1}. Recall that comp(f) is an abbreviation for [→ F](F = f).

[Z_{1} … Z_{n}Z → Y](∀x)[(C(x) ⊃ Z_{1}(x) = t_{1}) ∧ … ∧ (C(x) ⊃ Z_{n}(x) =

t_{n}) ∧ (C(x) ⊃ Z(t_{1} … t_{n}) = f(t_{1} … t_{n})) ⊃ (C(x) ⊃ Y (x) = f(t_{1} … t_{n}))] (F_{1})

If F is computable then the rule is a little simpler:

\frac{comp(f)}{\begin{matrix}[Z_{1} … Z_{n} → Y](∀x)[(C(x) ⊃ Z_{1}(x) = t_{1}) ∧ … ∧ (C(x) ⊃ Z_{n}(x) = t_{n}) \\ ⊃ (C(x) ⊃ Y (x) = f(t_{1} … t_{n}))] \end{matrix}} (F_{2})

This rule is also suitable for use with the subgoal principle S_{1}. The goal (C(x) ⊃ Y (x) = f(t_{1} … t_{n})) generates the subgoal (C(x) ⊃ Z(t_{1} … t_{n}) = f(t_{1} … t_{n})) and the subgoals (C(x) ⊃ Z_{i}(x) = t_{i}). Here x can be a sequence of variables. We can push (∀x) in and split up the hypotheses if desired. We prove this rule by the underlying logic (for equality) and functional composition rules. Using the composition rule, we can derive a related rule as follows:

\frac{comp(f) [→ Z_{1}](∀x)(C(x) ⊃ Z_{1}(x) = t_{1}) … [→ Z_{n}](∀x)(C(x) ⊃ Z_{n}(x) = t_{n})}{[→ Y](∀x)(C(x) ⊃ Y (x) = f(t_{1} … t_{n}))} (F_{3})

10.5 Mathematical induction

We now derive the following inference rule:

\frac{\begin{matrix}comp(x > 0) [→ G_{1}]A(G_{1}(0), 0) \\ [F → G_{2}](∀x)(x > 0 ∧ A(F (x − 1), x − 1) ⊃ A(G_{2}(x), x)) \end{matrix}}{[→ G](∀x)(x ≥ 0 ⊃ A(G(x), x))} (I_{1})

1. [→ G_{1}]  A(G_{1}(0), 0)

(assumed)

2. [F → G_{2}]  (∀x)(x > 0 ∧ A(F (x − 1), x − 1) ⊃ A(G_{2}(x), x))

(assumed)

3. [G_{1}G_{2} → G] (∀x)(x > 0 ⊃ G(x) = G_{2}(x)) ∧ (false(x > 0) ⊃ G(x) = G_{1}(x))

(using conditional rule C_{1}, since x > 0 is computable)

4. [F → G]  (∃G_{1}G_{2})(∀x)(A(G_{1}(0), 0) ∧ (x > 0 ∧ A(F (x − 1), x − 1) ⊃ A(G_{2}(x), x))

∧(x > 0 ⊃ G(x) = G_{2}(x)) ∧ (false(x > 0) ⊃ G(x) = G_{1}(x))) (the program composition rule, 1,2,3)

5. [F → G] (∀x)((x = 0) ⊃ A(G(x), 0) ∧ ((x > 0) ⊃ A(F (x − 1), x − 1) ⊃ A(G(x), x)))

(underlying logic rule)

6. [F → G] (∀x)(A(G(0), 0) ∧ ((x ≥ 0) ⊃ A(F (x), x) ⊃ A(G(x + 1), x + 1)))

(rewriting a little)

7. [→ G]  (∀x)(A(G(0), 0) ∧ ((x ≥ 0) ⊃ A(G(x), x) ⊃ A(G(x + 1), x + 1)))

(recursion rule)

8. [→ G]  (∀x)(x ≥ 0 ⊃ A(G(x), x))

(induction and the underlying logic rule)

Note that if x is ⊥ then x > 0 is undefined, but the induction hypotheses is x ≥ 0 ⊃ A(G(x), x), that is, true(x ≥ 0) ⊃ A(G(x), x), so only defined elements are considered. The term x − 1 in this rule can be replaced by any other term t(x) satisfying (x > 0 ⊃ t(x) < x):

\frac{\begin{matrix}comp(x > 0) (x > 0 ⊃ t(x) < x) [→ G_{1}]A(G_{1}(0), 0) \\ [F → G_{2}](∀x)(x > 0 ∧ A(F (t(x)), t(x)) ⊃ A(G_{2}(x), x)) \end{matrix}}{[→ G](∀x)(x ≥ 0 ⊃ A(G(x), x))} (I_{2})

Assuming as usual that A(F, x) is of the form A′(F (x), x), we can write this as follows:

\frac{\begin{matrix}comp(x > 0) (x > 0 ⊃ t(x) < x) [→ G_{1}]A(G_{1}, 0) \\ [F → G_{2}](∀x)(x > 0 ∧ A(F, t(x)) ⊃ A(G_{2}, x)) \end{matrix}}{[→ G](∀x)(x ≥ 0 ⊃ A(G, x))} (I_{3})

We can generalize this to an arbitrary well-founded ordering as follows:

\frac{[F → G](∀x)((∀y)(y < x ⊃ A(F, y)) ⊃ A(G, x)) < well − founded}{[→ G](∀x)A(G, x)} (I_{4})

Here we can let x be a tuple of variables as well as a single variable. By < well founded, we mean that the ordering true(x < y) is well-founded. Note that if “x < ⊥” is undefined always, then the hypotheses imply A(G, ⊥). Thus A must be stated in a way so as to include such undefined elements.

10.6 Induction and conditionals

Combining the above rule I_{4} with the conditional rule CM_{3}, we obtain the following rule that combines conditionals and induction:

\frac{\begin{matrix}(∧_{i}comp(C_{i})) (∀x)(C(x) ⊃ ∨_{i}C_{i}(x)) (∀x, i)(C(x) ⊃ def(C_{i}(x))) \\ ∧_{i}[F → G_{i}](∀x)(C(x) ∧ C_{i}(x) ⊃ (∀y)(y < x ⊃ A(F, y)) ⊃ A(G, x)) < well − founded \end{matrix}}{[→ G](∀x)(C(x) ⊃ A(G, x))} (IC_{1})

This is proven as follows: By the conditional rule CM_{3} given above, we conclude from the hypotheses that [F → G](∀x)(C(x) ⊃ (∀y)(y < x ⊃ A(F, y)) ⊃ A(G, x)). By the above well-founded induction rule I_{4}, we obtain [→ G](∀x)(C(x) ⊃ A(G, x)). We now have the problem of how to prove the hypotheses [F → G_{i}](∀x)(C(x) ∧ C_{i}(x) ⊃ (∀y)(y < x ⊃ A(F, y)) ⊃ A(G, x)). For this we can use the following rule:

\frac{\begin{matrix}(∀x, F)(C_{i}(x) ⊃ (∧_{i}A(F (t_{i}(x)), t_{i}(x)) ⊃ A(t(F (t_{1}(x)), …, F (t_{n}(x))), x))) \\ (∀x)(C_{i}(x) ⊃ t_{i}(x) < x) comp(t_{i}) comp(t) \end{matrix}}{[F → G](∀x)(C_{i}(x) ⊃ (∀y)(y < x ⊃ A(F (y), y)) ⊃ A(G(x), x))} (IC_{2})

The proof is by taking G(x) to be t(F (t_{1}(x)), …, F (t_{n}(x))); in our system, we can prove this using a functional composition rule.

10.6.1 Constructor rules

The rule I_{1} can also be generalized to constructors; for this we have the following rule:

\frac{comp(x > 0) [→ G_{1}]A(G_{1}, 0) [F → G_{2}](∀x)(x ≥ 0 ∧ A(F, x) ⊃ A(G_{2}, s(x)))}{[→ G](∀x)(x ≥ 0 ⊃ A(G, x))} (Co_{1})

This is more appropriate because the successor function s(x) suggests a constructor. We now consider the case of lists in more detail. For this we have the constructor “cons” and the destructors “car” and “cdr.” It is often the case that functions on lists are obtained by computing the first element of the list and then doing some recursion to obtain the tail of the list; thus, F (cons(x, y)) = cons(t(x, y), F (u(x, y))) where t, u are computable. We can express this in an inference rule as follows, where < orders lists by length:

\frac{\begin{matrix}comp(empty(x)) comp(u) comp(t) [→ G_{1}](∀x)(empty(x) ⊃ A(G_{1}, x)) \\ (∀F, x)(false(empty(x)) ∧ A(F, u(x)) ⊃ A(cons(t(x), F (u(x))), x)) \\ (∀x)(false(empty(x)) ⊃ u(x) < x ∧ t(x) < x) \end{matrix}}{[→ G](∀x)(list(x) ⊃ A(G, x))} (L_{1})

Note that empty(⊥) will be ⊥, and empty(x) in the hypotheses is coerced to true(empty(x)). Here list(x) is a predicate that is true of all lists without ⊥. The proof of this rule involves induction rules developed above (especially IC_{1}). It should be clear that many more such rules could be derived as needed.

We now develop a constructor rule for arbitrarily many constructors. Let T (F, X) be the set of terms over a set F of function symbols and a set X of variables. We have the following rule:

\frac{\begin{matrix}comp(s ∈ X) [→ F](∀s ∈ X)A(F, s) \\ [F → G](∀f(s_{1} … s_{n}) ∈ T (F, X))((∧_{i}A(F, s_{i})) ⊃ A(F, f(s_{1} … s_{m}))) \end{matrix}}{[→ F](∀s, t ∈ T (F, X))A(F, s)} (Co_{2})

This may be proven using rule I_{4} or IC_{1}, since the depth ordering on finite terms is well-founded. We now consider the case of many constructors and two arguments; this is useful for the unification function synthesis. We have the following rule:

\frac{\begin{matrix}comp(s ∈ X) [→ F](∀s ∈ X)(∀t ∈ T (F, X))A(F, s, t) \\ [→ F](∀t ∈ X)(∀s ∈ T (F, X))A(F, s, t) \\ [F → G](∀f(s_{1} … s_{m}), g(t_{1} … t_{n}) ∈ T (F, X)) \\ ((∧i, jA(F, s_{i}, t_{j})) ⊃ A(F, f(s_{1} … s_{m}), g(t_{1} … t_{n}))) \end{matrix}}{[→ F](∀s, t ∈ T (F, X))A(F, s, t)} (Co_{3})

Here we are assuming A(F, s, t) is of the form A′(F (s), F (t)) for some A′, as usual. This is also proven using I_{4} or IC_{1}, where pairs < s, t > of terms are ordered by the sum of their depths; this ordering is well-founded for pairs of finite terms.

Of course, one could also develop rules based on I_{4} or IC_{1} for more than one term, that perform induction on the sum of their depths; this would be a generalization of the above rule Co_{3} and is often useful too.

10.6.2 Induction and goal-directed program construction

We comment on how these rules can be used in goal-directed program generation. When attempting to derive [→ G](∀x)(x ≥ 0 ⊃ A(G, x)), the cases x = 0 and x > 0 are likely to be generated automatically. The case x = 0 may be solved first, and then the subgoal remains to solve the case x > 0. This may automatically generate a subgoal of the form A(F, t(x))); in our approach (using rules S_{1} and S_{2}) this is represented by the formula [F → G_{2}](∀x)(x > 0 ∧ A(F, t(x)) ⊃ A(G_{2}, x)). When such a formula is generated, it suggests to see if t(x) < x and if the induction principle can be applied. For this it is only necessary to generate the formula [→ G_{1}]A(G_{1}, 0) and one application of the derived rule for induction generates the conclusion [→ G](∀x)(x ≥ 0 ⊃ A(G, x)). Thus this fits into our general proof strategy and also gives a method to automatically detect when induction should be attempted. Or, if we solve the case x = 0 first, this may suggest to try an induction, although this gives less guidance about how it should be done.

In fact we can adapt the subgoal principle S_{1} to an arbitrary rule of inference; this corresponds to a proof transformation of the following type:

If we have a proof of the form

\frac{[X_{1} → Z_{1}](∀x)A_{1}(X_{1}, Z_{1}) … [X_{m} → Z_{m}](∀x)A_{m}(X_{m}, Z_{m})}{[→ Y](∀x)B_{1}(Y_{1}, x)}

(possibly an induction proof) then we can derive a rule of the form

\frac{\begin{matrix}[X_{1} → Z_{1}](∀x)A_{1}(X_{1}, Z_{1}) … [X_{m} → Z_{m}](∀x)A_{m}(X_{m}, Z_{m}) \\ [Y_{1} … Y_{n} → F](∀x)(B_{1}(Y_{1}, x) ∧ … ∧ B_{n}(Y_{n}, x) ⊃ P (F, x)) \end{matrix}}{[Y_{2} … Y_{n} → F](∀x)(B_{2}(Y_{2}, x) ∧ … ∧ B_{n}(Y_{n}, x) ⊃ P (F, x))}

Although formally fairly trivial, this shows us for example how the induction rules can be used together with the goal-directed approach.

10.6.3 A well-founded recursion rule

We now give another combination of an induction principle with a conditional rule; this one essentially eliminates all computable functions from an expression at once.

\frac{\begin{matrix}[F → G](∀x)C_{i}(x) ∧ A(F, t_{i}(x)) ⊃ A(G, x) [F → G](∀x)D_{i}(x) ⊃ A(G, x) \\ comp(C_{i}) comp(D_{i}) \\ (∀x)(C(x) ⊃ (∨_{i}C_{i}(x)) ∨ (∨_{i}D_{i}(x))) \\ (∀x)t_{i}(x) < x < well founded \\ (∀x, i)(C(x) ⊃ def(C_{i}(x))) (∀x, i)(C(x) ⊃ def(D_{i}(x))) \end{matrix}}{[→ G](∀x)(C(x) ⊃ A(G, x))} (R_{1})

This rule may seem somewhat unwieldy. But it can be used in a fairly natural way. The idea is to find (computable) conditions C_{i} and D_{i}, where the C_{i} permit G to be computed recursively and the D_{i} permit G to be computed nonrecursively. These conditions should be exhaustive and should permit induction on some well founded ordering. We can think of t_{i} as the argument of recursive calls of F; these are important for induction. For example, for factorial we have D_{1}(x) as x = 0 and C_{1}(x) as x > 0. We have t_{1}(x) as x − 1. We note that the recursive call of fact(x) is on x − 1, which is smaller in the usual ordering on the natural numbers. We can also do mutual recursion by having more than one program variable F and G. We can prove this rule R_{1} using the inference rules IC_{1} and IC_{2}. From IC_{2} we can derive [F → G](∀x)(C_{i}(x) ⊃ (∀y)(y < x ⊃ A(F (y), y)) ⊃ A(G(x), x)) and [F → G](∀x)(D_{i}(x) ⊃ (∀y)(y < x ⊃ A(F (y), y)) ⊃ A(G(x), x)). Then from IC_{1} we can derive [→ G](∀x)A(G, x).

10.7 Examples

We now give some examples of goal directed program generation. For these examples we assume that the underlying logic is the usual language of mathematics, possibly Zermelo-Fraenkel set theory. First we give a goal-directed derivation of the factorial function. We start with the goal [→ F](∀x)(x ≥ 0 ⊃ F (x) = fact(x)). The condition we use initially is x = 0; using the rule C_{2}, this generates the subgoals [→ F](∀x)(x = 0 ⊃ F (x) = fact(x)) and [→ F](∀x)(x > 0 ⊃ F (x) = fact(x)). The first may be rewritten using the underlying logic rule to [→ F](∀x)(x = 0 ⊃ F (x) = fact(0)) which simplifies to [→ F](∀x)(x = 0 ⊃ F (x) = 1); this can generate the subgoal [→ F](∀x)F (x) = 1. Since 1 is computable, this subgoal is solved. We now return to the subgoal [→ F](∀x)(x > 0 ⊃ F (x) = fact(x)). Using the underlying logic rule, this generates the subgoal [→ F](∀x)(x > 0 ⊃ F (x) = x ∗ fact(x − 1)). Since ∗ is computable, we generate from rule F_{2} the two subgoals [→ F](∀x)(x > 0 ⊃ F (x) = x) and [→ F](∀x)(x > 0 ⊃ F (x) = fact(x − 1)). The first is solvable since the identity is computable. The second generates the subgoals [→ F](∀x)(x > 0 ⊃ F (x − 1) = fact(x − 1)) and [→ F](∀x)(x > 0 ⊃ F (x) = x − 1). The second is easily solved since −, 1, and x are computable. The first remains unsolved. It is significant incidentally that the argument to F in the first subgoal is x−1 and not x; otherwise, the induction would require more intelligence to discover. The rule F_{1} was carefully constructed to generate this argument automatically.

Gathering all this together, we have shown that [G → F](∀x)((x > 0 ⊃ G(x − 1) = fact(x − 1)) ⊃ (x ≥ 0 ⊃ F (x) = fact(x))). (This could have been shown formally using the above rules, but it is simpler to give an informal proof.) This fits into the format of our induction rule I_{1} and so it only remains to prove the subgoal [→ F](∀x)(x = 0 ⊃ F (x) = fact(x)) (which has already been proven). We note that it was necessary to remember the value of x so that this induction could be done. The rules (especially the rules S_{1} and S_{2}) were structured to make this possible.

The formal structure of this proof is as follows:

1. [G → F] (∀x)[(x ≥ 0 ⊃ F (x) = fact(x)) ⊃ (x ≥ 0 ⊃ F (x) = fact(x))]

(underlying logic rule, computability of identity)

2. [G → F] (∀x)[(x > 0 ⊃ G(x − 1) = fact(x − 1)) ⊃ (x ≥ 0 ⊃ F (x) = fact(x))]

(1, by proof as sketched above, doing subgoaling)

3. [→ F]  (∀x)(x = 0 ⊃ F (x) = fact(x))

(as shown above)

4. [→ F]  (∀x)(x ≥ 0 ⊃ F (x) = fact(x))

(2,3, induction rule I_{1})

We now derive a simple sorting algorithm in a goal-directed manner. We chose an algorithm complex enough so that some nontrivial reasoning is involved in the derivation. We represent lists as usual, and use car, cdr, and cons as in LISP. Suppose the specification A(F, x) is sorted(F (x))∧mset(F (x)) = mset(x), where mset(x) is the multiset of elements of a list and sorted(x) means x is empty or car(x) = min(x) and sorted(cdr(x)). Also, min(x) is the smallest element in a list x. We start with the condition (x is empty) generating the subgoals (x is empty and A(F, x)) and (x is not empty and A(F, x)). The first is easily solved since all empty lists are sorted. This suggests to use an induction principle. From the induction principle IC_{1}, it suffices to show [G → F](∀x)(¬empty(x) ⊃ (A(G, u(x)) ⊃ A(F, x))) for some u(x) smaller than x. However, we choose to use the even more specific rule L_{1} for lists given earlier:

\frac{\begin{matrix}comp(empty(x)) comp(u) comp(t) [→ F_{1}](∀x)(empty(x) ⊃ A(F_{1}, x)) \\ (∀G, x)(¬empty(x) ∧ A(G, u(x)) ⊃ A(cons(t(x), G(u(x))), x)) \\ (∀x)(¬empty(x) ⊃ (u(x) < x) ∧ t(x) < x) \end{matrix}}{[→ F](∀x)(list(x) ⊃ A(F, x))}

Here < orders lists by their length. From the proof of this we know that ¬empty(x) ⊃ F (x) = cons(t(x), G(u(x))). We need to show (∀G, x)(¬empty(x) ∧ A(G, u(x)) ⊃ A(F (x), x)). Recall that A(F, x) is sorted(F (x)) ∧ mset(F (x)) = mset(x) for non-empty x. Also, sorted(y) is car(y) = min(y) ∧ sorted(cdr(y)) then. Therefore, replacing sorted(F (x)) by its definition, A(F, x) is car(F (x)) = min(F (x)) ∧ sorted(cdr(F (x))) ∧ mset(F (x)) = mset(x). Since car(F (x)) = min( F (x)) and mset(F (x)) = mset(x), car(F (x)) = min(x). Since F (x) = cons(t(x), G ( u(x))), t(x) = min(x) and G(u(x)) = cdr(F (x)). To determine u(x), we try to derive properties of cdr(F (x)). We can derive that mset(F (x)) is the union of {car(F (x))} and mset(cdr(F (x))); thus mset(cdr(F (x))) = mset(F (x)) − mset(car(F (x))) = mset(x) − mset(min(x)). The expression mset(x) − {min(x)} involves removing an element from a multiset. We want to use computable functions on lists instead of functions like “−” on multisets. Let remove(x, e) be a function that removes one of the occurrences of e from x, if x occurs in e. As a subgoal (not shown here) we can derive that such a function is computable. (We also can derive that min(x) is computable.) Thus we obtain mset(cdr(F (x))) = mset(remove(x, min(x))). Now, A(G, u(x)) is sorted(cdr(F (x)))∧mset(cdr(F (x))) = mset(u(x)) since G(u(x)) = cdr(F (x)). This suggests that u(x) is remove(x, min(x)), and with this we can derive (∀G, x)(¬empty(x)∧A(G, u(x)) ⊃ A(cons(t(x), G(u(x))) , x)) as required. Noting that u(x) < x and t(x) < x and u and t are computable, the proof is completed.

Another easy example of a program that can be derived this way is sublist(x, y) that checks that every element in x appears in y; this can be expressed (for nonempty x) as element(car(x), y) ∧ sublist(cdr(x), y). This fits a modification of rule I_{4} (or IC_{1}) in which the well-founded ordering is the sum of the term depths. It can also be regarded as a modified induction principle L_{1} for lists (regarding x as the argument of the function) with “cons” replaced by an arbitrary computable function.

We now discuss the most general unifier function, since it is a frequent test case for program generation methods. Our method permits much of the derivation to be done in the underlying logic; thus the proof becomes relatively short, but possibly not representative of the difficulty of deriving the program. Also, part of the proof is already done in the derivation of the derived inference rules (especially Co_{3}). We sketch the derivation here. Let [→ F](∀s, t ∈ T (F, X))mgu(s, t) = F (s, t) be our specification, where mgu(s, t) is a most-general unifier of terms s and t in T (F, X) if they are unifiable, else “fail.” Using the constructor rule Co_{3}, we obtain the subgoals [→ F](∀s ∈ X)mgu(s, t) = F (s, t), [→ F](∀t ∈ X)mgu(s, t) = F (s, t), and mgu(f(s_{1} … s_{m}), g(t_{1} … t_{n})) = F (f(s_{1} … s_{m}), g(t_{1}, …, t_{n})). The first two subgoals are solved by noting that if s = t, then mgu(s, t) = {}, else if s occurs in t, then mgu(s, t) = “fail”, else mgu(s, t) = {s ← t}. (This can be derived in the underlying logic.) Thus we can derive [→ F]mgu(s, t) = F (s, t) using a conditional rule, assuming the occurrence check is computable. Of course, that must be shown as a lemma, which is easy using the rule Co_{3} again. For the last subgoal, we use the fact that the most general unifier of f(s_{1} … s_{m}) and g(t_{1} … t_{n}) is fail, if f ≠ g, and otherwise it does not depend on f or g. This also can all be shown in the underlying logic. So we have a function mgu list([s_{1}, …, s_{m}], [t_{1}, …, t_{n}]) to compute the most general (simultaneous) unifier of these two lists and the fact that mgu(f(s_{1} … s_{n}), f(t_{1} … t_{n})) = mgu list([s_{1}, …, s_{m}], [t_{1}, …, t_{n}]). We can then apply Co_{3} again, or use our above scheme for list computations (extended to two arguments) to find a simple recursive computation of mgu list([s_{1} … s_{m}], [t_{1} … t_{n}]) in terms of mgu list([s_{2} … s_{m}], [t_{2} … t_{n}]). This requires methods for composing and applying substitutions, which also have to be derived in P L.

11 Deriving Programs versus Deriving Outputs

We note that the fixpoint property requires that the program variables represent programs and not specific inputs and outputs. Thus in this formalism it is not convenient to derive statements like (∀x)(∃y)A(x, y) where x are input variables and y are output variables. Such statements can be derived in the above formalism if y is computable by a finite straight-line program, but it is difficult or impossible (we think) to do if the computation of A requires recursion. This is because the recursion rule is difficult to apply in a natural way at this level. For example, it’s not typical recursion to look for an x such that x = x^{2} + 5. We note that it is theoretically possible to find a (real) x such that x = x^{2} + 5; we can let x be “bottom.” Or we can let x be a complex number. However, this is not usually what is wanted when reasoning about recursion and inputs and outputs in this manner. Instead, we state the specification in the form [→ Z](∀x)A(x, Z(x)). In this way, it becomes more natural to do recursion since it is more natural to look for a program Z such that Z = F (Z) where F is some program-forming operation. We have demonstrated above that recursive programs can easily be generated in this way. In fact, the fact that we can generate all partial recursive functions is a kind of evidence of completeness of this approach. Also, it is easy to show that if a program can be verified within a certain formalism (such as Floyd’s method) then we can construct a proof representing that program. This probably also applies to Hoare-style logics.

12 Higher-Order Features

It is possible to get much of the power of this system in a first-order logic. The program variables may be higher order variables, but it is not necessary. They may be individual (first-order) variables. This allows the underlying logic to be first-order. This is reasonable since the progam variables refer to programs, which are textual objects (character strings). We can then indicate the application of a program variable X to arguments t_{1} … t_{n} by f_{eval}(X, t_{1} … t_{n}) or P_{eval}(X, t_{1} … t_{n}) where f_{eval} is a function and P_{eval} is a predicate, depending on the sort of X. Also, if we are reasoning about several kinds of semantics, then we can use several such f_{eval} and P_{eval} functions together.

We note that the program variables typically represent first-order functions or predicates. These can be informally regarded as of sort [input^{m} → output]. The program construction functions then represent higher-order functions, since they map tuples of programs to programs. These are therefore informally of sort PC, which can approximately be written as [program^{n} → program]. A proof can be regarded as a way to obtain new program construction functions, so it can be regarded as a yet higher-order function which permits the program-construction functions in the hypothesis to be mapped onto the program-construction functions in the conclusion. A proof would then have sort something like [P C^{p} → P C]. By considering deduction rules of the form “If A is derivable from B then C is derivable from D” we can obtain still higher-order such functions. Therefore, even though the logic does not explicitly specify methods for obtaining arbitrarily high order programs, it does give some implicit mechanism for doing this.

However, there is a more direct way to incorporate higher order features into this logic. For this we have to extend the definition of a programming structure so that P C also contains computable functions from P C to P C. The idea is to permit the quantifier [X → Y] to be more general, for example, something like [(X → Y) → (U → V)], signifying a function from X → Y to U → V. The semantic formula corresponding to [(X → Y) → (U → V)]A(X, Y, U, V) would then be (∃G)(∀XF U)A(X, F (X), U, G(F)(U)). Thus G maps functions X → Y to functions U → V. Such quantifiers (analogous to types) could be arbitrarily complicated, as, [(X → Y) → (U → (V → W))]. This feature may be compatible with certain forms of polymorphism, too. As an example of reasoning with this kind of logic, we may have a rule that says that if we can derive [U → V]B from [X → Y]A then we can conclude [(X → Y) → (U → V)](A ⊃ B). Also, we might allow a program variable X in [X → Y]A(X, Y) to be instantiated by U → V to obtain [(U → V) → Y]A(F, Y) where F maps the sort of U to the sort of V. We have not needed this facility so far, and so we have not presented it in much detail. Also, we can have inference rules as follows:

\frac{[X → Y]A(X, Y)}{[→ F](∀X)A(X, F (X))}

\frac{[→ F](∀X)A(X, F (X))}{[X → Y]A(X, Y)}

The first rule permits us to go from the level of reasoning about inputs and outputs, to the level of reasoning about programs (and higher levels). The second rule permits us to go from the level of reasoning about programs to the level of reasoning about inputs and outputs. These would have to be restricted so that the sorts of the variables X,Y, and F are all program sorts. Using these rules, we can for example reason about inputs and outputs, and then go up to the level of reasoning about programs in order to do a recursion, which may not be possible at the lower level.

References

[1] Penny Anderson. Program Derivation by Proof Transformation. PhD thesis, Carnegie-Mellon University, October 1993.

[2] Philippe Audebaud. Partial objects in the calculus of constructions. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 86–95, Amsterdam, The Netherlands, July 15–18 1991.

[3] David Basin. Isawhelk: Whelk interpreted in Isabelle. Abstract accepted at the 11th International Conference on Logic Programming (ICLP94). Full version available via anonymous ftp to mpi-sb.mpg.de in pub/papers/conferences/Basin-ICLP94.dvi.Z.

[4] David Basin, Alan Bundy, Ina Kraan, and Sean Matthews. A framework for program development based on schematic proof. In 7th International Workshop on Software Specification and Design, Los Angeles, December 1993. IEEE Computer Society Press.

[5] Joseph L. Bates and Robert L. Constable. Proofs as programs. ACM Transactions on Programming Languages and Systems, 7(1):113–136, January 1985.

[6] W. Bibel. Syntax-directed, semantics-supported program synthesis. Artificial Intelligence, 14:243–261, 1980.

[7] R.J. Brachman and J.G. Schmolze. An overview of the kl-one knowledge representation system. Cognitive Science, 9(2):171–216, 1985.

[8] A. Bundy, F. van Harmelen, C. Horn, and A. Smaill. The Oyster-Clam system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 647–648. Springer-Verlag, 1990. Lecture Notes in Artificial Intelligence No. 449. Also available from Edinburgh as DAI Research Paper 507.

[9] Rod M. Burstall and Joseph A. Goguen. The semantics of clear, a specification language. In Advanced Course on Abstract Software Specification. LNCS 86, 1980.

[10] J. Cai and R. Paige. Program derivation by fixed point computation. Science of Computer Programming, 11:197–261, 1988/89.

[11] Robert L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986.

[12] Thierry Coquand and Gérard Huet. The Calculus of Constructions. Information and Computation, pages 95–120, 1988.

[13] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 243–309. North-Holland, 1990.

[14] Gilles Dowek, Amy Felty, Hugo Herbelin, Gerard Huet, Christine Paulin-Mohring, and Benjamin Werner. The coq proof assistant user’s guide. Technical report, INRIA, Rocquencourt, France, December 1991.

[15] J.Y. Girard. A new constructive logic: classical logic. Mathematical Structures in Computer Science, 1:255–296, 1991.

[16] C.A. Goad. Computational Uses of the Manipulation of Formal Proofs. PhD thesis, Stanford University, 1980.

[17] Michael J. Gordon, Robin Milner, and Christopher P. Wadsworth. Edinburgh LCF: A Mechanized Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

[18] Cordell Green. Application of theorem proving to problem solving. In Proceedings of the IJCAI-69, pages 219–239, 1969.

[19] T. Griffin. A formula-as-types notion of control. In Proceedings of the 17th Annual ACM Symposium on Principles of Programming Languages, pages 47– 58, San Francisco, California, January 17-19 1990.

[20] W. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus, and Formalism, pages 479–490. Academic Press, NY, 1980.

[21] Ina Kraan, David Basin, and Alan Bundy. Logic program synthesis via proof planning. In K.K. Lau and T. Clement, editors, Logic Program Synthesis and Transformation, pages 1–14. Springer-Verlag, 1993. Also available as Max-Planck-Institut für Informatik Research Paper MPI-I-92-244.

[22] J.W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. 2nd edn.

[23] Z. Manna and R. Waldinger. A deductive approach to program synthesis. ACM Transactions on Programming Languages and Systems, 2(1):90–121, 1980.

[24] Per Martin-Löf. Constructive mathematics and computer programming. In Sixth International Congress for Logic, Methodology, and Philosophy of Science, pages 153–175, Amsterdam, 1982. North Holland.

[25] C.R. Murthy. An evaluation semantics for classical proofs. In Proceedings of the Sixth Annual IEEE Symposium on Logic in Computer Science, pages 96–107, Amsterdam, The Netherlands, July 15–18 1991.

[26] M. Parigot. Free deduction: an analysis of computations in classical logic. In Proc. Russian Conference on Logic Programming, pages 361–380, St. Petersburg, Russia, 1991.

[27] M. Parigot. Lambda-mu calculus: an algorithmic interpretation of classical natural deduction. In Proc. International Conference on Logic Programming and Automated Reasoning, pages 190–201, St. Petersburg, Russia, 1992.

[28] M. Parigot. Strong normalization for second order classical natural deduction. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science, pages 39–46, Montreal, Canada, June 19-23 1993.

[29] Lawrence C. Paulson. Introduction to Isabelle. Technical Report 280, Cambridge University Computer Laboratory, Cambridge, January 1993.

[30] D. Plaisted. Equational reasoning and term rewriting systems. In D. Gabbay and J. Siekmann, editors, Handbook of Logic in AI and Logic Programming, volume 1. Oxford University Press, 1993.

[31] Scott F. Smith. Partial Objects in Type Theory. PhD thesis, Cornell, 1988.

[figure: I N F O R M A T I K]

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. If you have any questions concerning ftp access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Regina Kraemer Im Stadtwald D-66123 Saarbrücken GERMANY

            e-mail: kraemer@mpi-sb.mpg.de

MPI-I-94-230 H. J. Ohlbach  Temporal Logic Proceedings of the ICTL Workshop

MPI-I-94-228 H. J. Ohlbach Computer Support for the Development and Investigation of Logics

MPI-I-94-226 H. J. Ohlbach, D. Gabbay, D. Plaisted  Killer Transformations

MPI-I-94-225 H. J. Ohlbach Synthesizing Semantics for Extensions of Propositional Logic

MPI-I-94-224 H. Aït-Kaci, M. Hanus, J. J. M. Navarro Integration of Declarative Paradigms Proceedings of the ICLP’94 Post-Conference Workshop Santa Margherita Ligure, Italy

MPI-I-94-223 D. M. Gabbay LDS – Labelled Deductive Systems Volume 1 — Foundations

MPI-I-94-218 D. A. Basin  Logic Frameworks for Logic Programs
MPI-I-94-216 P. Barth  Linear 0-1 Inequalities and Extended Clauses
MPI-I-94-209 D. A. Basin, T. Walsh  Termination Orderings for Rippling
MPI-I-94-208 M. Jäger  A probabilistic extension of terminological logics
MPI-I-94-207 A. Bockmayr  Cutting planes in constraint logic programming

MPI-I-94-201 M. Hanus The Integration of Functions into Logic Programming: A Survey

MPI-I-93-267 L. Bachmair, H. Ganzinger  Associative–Commutative Superposition
MPI-I-93-265 W. Charatonik, L. Pacholski  Negativ set constraints: an easy proof of decidability

MPI-I-93-264 Y. Dimopoulos, A. Torres Graph theoretical structures in logic programs and default theories

MPI-I-93-260 D. Cvetković The logic of preference and decision supporting systems

MPI-I-93-257 J. Stuber Computing Stable Models by Program Transformation

MPI-I-93-256 P. Johann, R. Socher  Solving simplifications ordering constraints
MPI-I-93-250 L. Bachmair, H. Ganzinger  Ordered Chaining for Total Orderings
MPI-I-93-249 L. Bachmair, H. Ganzinger  Rewrite Techniques for Transitive Relations