# Item

ITEM ACTIONSEXPORT

Released

Report

#### A general technique for automatically optimizing programs through the use of proof plans

##### Locator

There are no locators available

##### Fulltext (public)

MPI-I-94-239.pdf

(Any fulltext), 28MB

##### Supplementary Material (public)

There is no public supplementary material available

##### Citation

Green, I.(1994). *A general technique for automatically optimizing
programs through the use of proof plans* (MPI-I-94-239). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B7BB-8

##### Abstract

The use of {\em 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 {\em
constraint-based} program optimization through the use of proof plans
for mathematical induction.
Proof plans are used to control the (automatic) synthesis of
functional programs, specified in a standard equational form, {$\cal
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 {$\cal E$}. Thus the theorem
proving process is a form of program optimization allowing for the
construction of an efficient, {\em target}, program from the
definition of an inefficient, {\em source}, program.
The general technique for controlling the syntheses of efficient
programs involves using {$\cal 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 {\em 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.