max planck institut
informatik

# MPI-I-94-240

## Recursive program optimization through inductive synthesis proof transformation

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:

MPI-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
BibTeX