MPI-I-94-240
Recursive program optimization through inductive synthesis proof transformation
Madden, Peter
September 1994, 44 pages.
.
Status: available - back from printing
The research described in this paper involved developing
transformation techniques which increase the efficiency of the
original program, the {\em source}, by transforming its synthesis
proof into one, the {\em target}, which yields a computationally more
efficient algorithm. We describe a working proof transformation
system which, by exploiting the duality between mathematical
induction and recursion, employs the novel strategy of optimizing
recursive programs by transforming inductive proofs. We compare and
contrast this approach with the more traditional approaches to
program transformation, and highlight the benefits of proof
transformation with regards to search, correctness, automatability
and generality.
Note:
To appear in the Journal of Automated Reasoning
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-240
BibTeX
@TECHREPORT{Madden94a,
AUTHOR = {Madden, Peter},
TITLE = {Recursive program optimization through inductive synthesis proof transformation},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-94-240},
MONTH = {September},
YEAR = {1994},
ISSN = {0946-011X},
NOTE = {To appear in the Journal of Automated Reasoning},
}