Predicate Logic: A Calculus for the Formal Derivation of Programs

1. Programs as computationally useful theorems

We start with a set of axioms that give an intuit­ ively correct characterization of some input-output relation we wish to compute. Under the procedural interpretation of logic [5,6] these axioms can be used to 'compute' the relation. So we 'symbolically execute' the axioms, qua program, for various forms of input. From each symbolic execution we distil a theorem that can double for the axioms in the business of computing the relation. Our set of derived theorems is a logic program whose proced­ ural use is computational.

Example

The following axioms are a specification for the input-output relation, mem-test, of a program to test if an element u is a member of a list z. The output is to be T ~f u£z, F if not. All free var­ iables (lower case) are implicitly universally quantified.

Specification

~£NIL (or u£NIL ++ false )

U£V.X ++ u=v V U£X

In several respects this axiomatisation is incom­ plete. We should really _axiomatise the equality relation for lists, and list elements, and express the finiteness condition for lists by an induction schema [~. However the absence of explicit equal­ ity axioms is an implicit assumption that things are equal only if they are identically named, which is what we intend, and we shall not need the induc­ tion schema for the program synthesis.

Synthesis

We 'evaluate' the definition of mem-test for the cases z=NIL and z=v.x ·

z=NIL

mem-test(u,NIL,t) ++ t=T & U£NIL v t=F & ~U£NIL

Using the axiom U£NIL ++false the 'call' U£NIL evaluates to false , giving

mem-test(u,NIL,t) ++ t=T & false v t=F & ~false

The definiens now reduces to t=F using only logical evaluation rules. In effect we have proved

mem-test(u,~IL,F)

z=v.x

mem-test(u,v.x,t) ++ t=T & u£v.x v t=F & ~u£v.x This time we evaluate the 'call' U£v.x by substit-

(1)

2. Proof theory analysis of computation

The computations of logic programs are resolution proofs. We can characterize such proofs as paths through an interconnectivity graph[~, the unific­ ations that appear on each path being the essential steps of the proof computation. This conceptualiz­ ation of what constitutes a proof gives us a tool for analysing, and reformulating, a logic program.

Example

The logic program

Fact(O,l)

Fact(n+l, (n+l) Xy) + Fact(n,y)

is used to compute the factorial function by asking for a refutation of a conjecture of the form ~Fact(u,v) where u is some numeral input. Below is an interconnectivity graph for the general theorem proving task in which the conditional statement has been expressed in clausal form. Unifiable comple­ mentary literals are connected with an edge labelled by the unifying substitution.

A proof of Fact(u,v) is given by any path through the graph that connects ~Fact(u,v) with Fact(O,l). In this case the set of all possible paths can be succinctly described by the regular expression a I bc*d · In effect, this is an iterative charact­ erization of the set of compositions of unifications that constitute a proof. Taking into account the intended use of the logic program, i.e. that u is to be input and v output, it is a compact notation for the iterative program:

• ll a: if u=O then v+l
• b: initialise u'+o; v'+l
• c*: repeat (zero or more times) u'+u'+l; v'+u' X v'
• d: terminate above loop when u'=u v+v'

General method

The above example was simple enough for us to read off directly from the graph a regular expression. For more complex examples we may first need to char­ acterize the set of proofs by a context free attri­ bute grammar. This we can always do [9]. The productions of such a grammar reflect the ground structure of the problem, taking into account unif­ iable pairs of literals, but ignoring the necessary substitutions. The attributes carry the substitu­ tion information. Temporarily ignoring the attri­ butes we try to re-express the language generated using regular expressions. To the extent that we are successful, we then re-introduce the substitu­ tion constraints as refinements of the regular expressions. Thus, in the Fact example, the regular expression bc*d would be refined by the constraint that c is applied the number of times to satisfy the substitution. The refined expression is there­ fore bc(u-l)d ·

Domain and range

The attributes are consistency checks on the vari­ ables; a production can be applied only if its associated substitution constraint is consistent with the substitution constraint of all previous steps in the derivation. The refined regular exp­ ression therefore gives us restrictions on each of the variables that must be satisfied in any proof. The restrictions on the input variables determine the domain, those on the output variables the range. For Fact, this analysis gives us 0+(+1)* as the domain, i.e. the natural numbers, and, for n in the natural numbers, n X ( (n-1) ·· X(2 ·x 1) ·· ) as the range.

Termination

If we are able to describe the set of computations as a regular expression we can use the attributes to replace the *'s with specific integer functions of the arguments. If we can do this for every*, that is for every implicit iteration, we have proved that every computation terminates.

3. Final remarks

So far we have only investigated the hand synthesis of logic programs. However it is intended to imple­ ment an interactive system .which becomes more aut­ onomous as the synthesis methodology is refined and understood. The idea of synthesing a recursive program from the recursive use of a specification first appeared, independently, in (1] and (7]. Indeed the reader may have noticed the similarity between our approach and that of Darlington and Burstall[l,4]. Like them we use . the same formalism for both specification and program (they use enriched recursion equations), and like them we symbolically execute the specification. We have derived much from their work.

The proof theory analysis of computation is also in its beginning stages. It is in fact an applicat­ tion of more general work, currently in progress, on the analysis of resolution proofs. We be.lieve it provides a useful conceptualization, and will provide a useful tool.