Division of Informatics

Forrest Hill & 80 South Bridge

## Research Paper #512 | |
---|---|

Title: | Using Middle-Out Reasoning to Transform Naive Programs into Tail-Recursive Ones |

Authors: | Hesketh,J; Bundy,A; Smaill,AD |

Date: | Dec 1990 |

Presented: | Submitted to IJCAI-91 |

Keywords: | |

Abstract: | We describe a novel technique for the automatic transformation of naive computer programs into tail-recursive ones, with a consequent gain in efficiency. The technique is to specify the required program using the naive definition 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 be higher order. |

Download: | POSTSCRIPT COPY |