Using middle-out reasoning to control the synthesis of tail-recursive programs

Abstract

We describe a novel technique for the automatic synthesis of tail-recursive programs. The technique is to specify the required program using the standard equations and then synthesise the tail-recursive program using the proofs as programs technique. This requires the specification to be proved realisable in a constructive logic. Restrictions on the form of the proof ensure that the synthesised program is tail-recursive.

The automatic search for a synthesis proof is controlled by proof plans, which are descriptions of the high-level structure of proofs of this kind. We have extended the known proof plans for inductive proofs by adding a new form of generalisation and by making greater use of middle-out reasoning. In middle-out reasoning we postpone decisions in the early part of the proof by the use of meta-variables which are instantiated, by unification, during later parts of the proof. Higher order unification is required, since these meta-variables can represent higher order objects.

The program synthesised is automatically verified to ensure that it satisfies its specification. This type of verification is contrasted with template-based transformation approaches which require proofs that the general transformations described by the templates preserve equivalence.

The technique described is more general than template-based approaches, since it is not tied to program patterns which must be specified in advance. Detailed information about proof structure enables it to use a wider repertoire of rewritings in a more goal-directed way than comparable transformational techniques.

The research reported in this paper was supported by SERC grant GR/E/71799, and an SERC Senior Fellowship to the second author. We are grateful for feedback on this paper from Andrew Ireland and Toby Walsh, and for conversations with Dale Miller and other members of the Mathematical Reasoning Group at Edinburgh.