Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


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

Madden, Peter and Green, Ian

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.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-239.pdfMPI-I-94-239.pdfArticles: 1. Madden-JAR Database 'MPII AG2 Publications', View '1. Author/Editor \ 2. by Group', Document 'Recursive Program Optimization Through Inductive Synthesis Proof Transformation', 2. MaddenGreen94b-aismc2 Database 'MPII AG2 Publications', View '1. Author/Editor \ 2. by Group', Document 'A General Technique for Automatic Optimization by Proof Planning'27763 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Madden, Peter and Green, Ian},
  TITLE = {A general technique for automatically optimizing programs through the use of proof plans},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-94-239},
  MONTH = {August},
  YEAR = {1994},
  ISSN = {0946-011X},