MPI-I-94-239
A general technique for automatically optimizing programs through the use of proof plans
Madden, Peter and Green, Ian
August 1994, 16 pages.
.
Status: available - back from printing
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.
-
MPI-I-94-239.pdfArticles: 1. Madden-JAR , 2. MaddenGreen94b-aismc2
- Attachement: MPI-I-94-239.pdf (27763 KBytes)
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-239
BibTeX
@TECHREPORT{MaddenGreen94,
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},
}