ausblenden:
Schlagwörter:
-
Zusammenfassung:
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.
