A General Technique for Automatic Optimization by Proof Planning

The use of *proof plans* -- formal patterns of reasoning for theorem proving -- to control the (automatic) synthesis of efficient programs from standard definitional equations is described. A general framework for synthesizing efficient programs, using tools such as higher-order unification, has been developed and holds promise for encapsulating an otherwise diverse, and often ad hoc, range of transformation techniques. A prototype system has been implemented. We illustrate the methodology by a novel means of affecting *constraint-based* program optimization through the use of proof plans for mathematical induction. \par Proof plans are used to control the (automatic) synthesis of functional programs, specified in a standard equational form, E, by using the proofs as programs principle. The goal is that the program extracted from a constructive proof of the specification is an optimization of that defined solely by E. Thus the theorem proving process is a form of program optimization allowing for the construction of an efficient, *target*, program from the definition of an inefficient, *source*, program. \par The general technique for controlling the syntheses of efficient programs involves using E to specify the target program and then introducing a new sub-goal into the proof of that specification. Different optimizations are achieved by placing different characterizing restrictions on the form of this new sub-goal and hence on the subsequent proof. Meta-variables and higher-order unification are used in a technique called *middle-out reasoning* to circumvent eureka steps concerning, amongst other things, the identification of recursive data-types, and unknown constraint functions. Such problems typically require user intervention