Formal Efficiency Analysis for Tree Transducer Composition

Author: J. Voigtländer
Published: Technical Report TUD-FI04-08, Technische Universität Dresden, June 2004.
BibTeX: Voi04b.bib
Abstract: We study the question of efficiency improvement or deterioration for a semantics-preserving program transformation technique for (lazy) functional languages, based on composition of restricted macro tree transducers. By annotating programs to reflect the intensional property "computation time" explicitly in the computed output and by manipulating such annotations, we formally prove syntactic conditions under which the composed program is guaranteed to be not less efficient than the original program with respect to the number of call-by-name reduction steps required to reach normal form. Under additional conditions the guarantee also holds for call-by-need semantics. The criteria developed can be checked automatically and efficiently, and thus are suitable for integration into an optimizing compiler.

An abridged and revised version of this work appeared in Theory of Computing Systems, see here.