Automatic methods for program transformation
Wei Ngan Chin · Spiral (Imperial College London) · 1990
The transformational approach to software development is recognised as an important formal route for software construction.One major benefit of this approach is the possibility of providing machine assistance to this development process.This thesis works towards this goal by systematizing four major classes of transformations into automated methods (or tactics).The first class of transformations involves the fusion of composed expressions to eliminate unnecessary intermediate data structures and function calls.A producer-consumer model of functions is introduced to explain this transformation.With this model, we show how the deforestation algorithm of Wadler can be extended to all first-order programs.The extended transformation algorithm is presented, termination proof given and further improvements suggested.A similar consideration is also developed for compositions in set abstractions.The second class of transformations involves the removal of certain higher-order features from well-typed programs.Three transformation algorithms are developed.Two of them are directly concerned with the removal of higher-order features.Termination proofs for these algorithms are given.A third algorithm preserves full laziness in a manner compatible with higher-order features removal.With these transformations, the extension of deforestation to higher-order programs is also developed.The third class of transformations concerns the removal of redundant computation through tup ling.A survey of past techniques is presented, followed by the development of a new analysis technique to discover eureka tuples to remove redundancy.This new technique makes novel use of selection orderings to search for eureka tuples.We give some methods to determine appropriate orderings and provide extensions to the basic analysis technique.The last class of transformations involves the use of constraints (or invariants) to help improve recursive programs.Both the finite differencing tactic and a new base-case filter promotion tactic are part of this category of transformations.The necessary laws and semantic conditions for these two tactics are systematized.Phil Wadler for inspiring much of the work done in Chapter 3 and 4.