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

MPI-I-94-240

Recursive program optimization through inductive synthesis proof transformation

Madden, Peter

MPI-I-94-240. September 1994, 44 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
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
Acknowledgement:
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-240.pdfMPI-I-94-240.pdf41603 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: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-240
Hide details for BibTeXBibTeX
@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},
}