Properties of Unfolding-based Meta-level Systems

Abstract

It is well known that one can often transform a given program into a more efficient equivalent: by introducing some ''eureka definitions'' and then performing a sequence of unfold/fold/... steps, or by applying the technique of dynamic programming. A framework is set up, general enough to account for both of those techniques, enabling us to reason formally about complexity improvements. It is shown that under the absence of certain features, transformation is able to speed up execution time by at most a constant factor only. In order to have a chance of achieving a more substantial speed up, a transformation system thus must contain at least one of those features. Finally, it is shown that under very weak conditions termination properties are preserved by transformation.