max planck institut
informatik

MPI-I-94-239

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

MPI-I-94-239. August 1994, 16 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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.
Acknowledgement:
References to related material:

Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-239
BibTeX