• People
• Events
• Research

Deliverables: A categorical approach to program development in type theory

Introduction: This paper outlines a method for constructing a program together with a proof of its correctness with respect to a given specification. The technology used is type theory, in fact an extended version of Calculus of Constructions Luo's ECC as implemented in Pollack's `Lego' system; here program means a primitive recursive description of a function using simply typed lambda calculus with higher order functions and data types such as numbers and lists.

Given a precondition and a postcondition we consider pairs consisting of

• a program
• a proof that the program satisfies the postcondition given the precondition.

We call such a pair together with the pre- and postconditions a deliverable, since it is what a software house should ideally deliver to its client instead of just a program.

Now we observe that various operations, composition, pairing, iteration and so on, can be used to combine deliverables, and that these operations can be implemented in ECC. Consider for example composition. If (f, p) is a deliverable from pre to post and (f', p') is a deliverable from post to post' then their composition is a deliverable from pre to post' thus

• f o f', the composition of the functions
• a proof using p and p' that f o f' satisfies post' given pre.

In fact the combining operations (excluding iteration) are exactly those of a cartesian closed category whose objects are the pre- and postconditions and whose arrows are deliverables. This is comforting since it assures us that we have a complete set of combinators. They enable us to build a complicated program together with its correctness proof. Since the resulting expression of the calculus denotes a pair we can extract the program trivially by evaluating the first element of the pair.

We have used the Lego system to define these combinators and use them to create the deliverables for several programs as examples.

However in many cases a precondition and a postcondition do not satisfactorily specify a desired program. For example when developing a sorting program the precondition might ask for an arbitrary list and the postcondition demand that the result be a sorted list. But we would get little thanks for a program which always returned the nil list, even though this is sorted. We need to specify that the output list should also be a permutation of the input one.

If we try to replace the pre- and postconditions by a single statement specifying a relation between input and output there do not seem to be convenient combination operators; so we discard that approach. Thinking syntactically, we could allow the pre- and postconditions to share a free variable. For example using a free variable l for lists

pre(x) = x = l

post(y) = isPermutation(y, l)

This ties the pre- and postconditions together, but such free variables should have a definite scope.

We can think, more semantically, that l satisfies some base condition (it must be a list) and the pre- and post conditions are relations whose first argument is l. Thus we can talk of pre- and post conditions relative to l. Now a deliverable relative to l is a program which takes the precondition to the postcondition for all l. We will refer to these as second order specifications and deliverables in contrast to the original first order ones.

How should we represent specifications and deliverables in type theory? We choose the following:

A first order specification is a predicate over a type, thus

• a type, s;
• a function, S, from s to Prop (the type of propositions);

and a first order deliverable from specification (s, S) to specification (t, T) is a program paired with a proof thus

• a function, f : s -> t;
• a proof, phi : forall x : s.Sx -> T(f x) where forall is the Pi quantifier on propositions.

Now we can generalise these to work relative to a first order specification (u, U), which corresponds to the free variable l in our example. Call u the base type; now the second order specification becomes a relation over the base type and another type, and the second order deliverable must respect the pre- and postrelations. We leave the details to the body of the paper.

We might try to characterise the first order deliverables as a cartesian closed category whose objects are specifications and whose arrows are deliverables; this is almost correct, but we have to modify the CCC to a semi-cartesian closed category, a mild generalisation due to Hayashi. The second order deliverables are then characterised using a fibration whose fibres are categories of first order deliverables. In fact this structure constitutes a model of type theory.

The paper includes some illustrative examples of program development using deliverables and brief mention of others, of which the most substantial is an algorithm for the Chinese Remainder theorem.

We also discuss the relation to earlier work on extracting programs from proofs, particularly the work of Martin-Lof as developed by Nordstrom, Petersson and Smith. They define a translation from a type theory, say S, to an underlying type theory U such that the types in S correspond to our specifications and the unary terms in S correspond to our deliverables. A somewhat similar approach is taken by Paulin-Mohring in her work on program extraction using the realisability interpretation.

The virtue of our method is that it can quite easily be coded up in an existing system, and there is no difficulty about extracting the program from the proof, since they are built together but as separate components of a pair; normalising the first component gives us the program. We have mentioned operations for combining deliverables, and this might suggest a bottom-up approach; but we can just as well start with a specification of the desired program and derive the corresponding deliverable top-down by refinement in Lego.

The weakness of our method is that we have to use a combinatory notation which is less perspicuous than the usual lambda notation of type theory. Since deliverables form a model of type theory, this might possibly be rectified by extending ECC with an extra kind whose types would be specifications and whose terms would be deliverables, thus following the insight of Martin-Lof; but we have not yet worked out this approach. The basic approach was proposed in an unpublished talk by Burstall at the Baastad Workshop on type theory in 1988. A brief account by the present authors appeared as Deliverables: an approach to program development in Constructions, and a full treatment of work so far is in McKinna's thesis.

LFCS report ECS-LFCS-92-242, October 1992.

A revised version of this report was presented at Mathematical Foundations of Computing Science '93 in Gdansk. The proceedings are published by Springer-Verlag as LNCS 711, 1993.