Abstract:

We present a framework for automatic program transformation of a strict and pure functional language with a well-defined semantics. It will be shown that such a framework can be implemented most declaratively and concisely in a recently developed higher-order logic programming language called LambdaProlog.

The most important component of this framework is an efficient, always terminating partial evaluator that can handle higher-order functions and preserves the effect behaviour of programs by making use of monads, a construct which originated in category theory. This allows us to fully exploit the higher-order capabilities of the implementation language to reason about computations as required for partial evaluation. Due to this technique, the only factor that limits the optimisation power of the partial evaluator seems to be the generally undecidable problem of inferring termination behaviour of computations. The information gathered by the partial evaluator is most useful for subsequent improvements such as, for example, common sub-expression elimination.

We will also give a broad overview of techniques to automate program transformation, how their correct application can be guaranteed and how such transformation processes can be guided to quickly find more efficient programs. The framework should provide for a strong basis to try out some of the more advanced transformations.

• Acknowledgements
• Contents
• Introduction
  • Purpose of program transformations
  • Why transform functional programs?
  • Difficulties
  • Goals and structure of this work
• A Simple Functional Language with Call-by-Value Semantics
  • Description of types, values and informal semantics
  • Abstract syntax
  • Formal typing rules
  • Operational semantics
  • Denotational semantics
• Automated Transformations
  • Partial evaluation
  • Fold/Unfold method
  • Bird/Meertens formalism
• Correctness of Transformations
  • Preserving termination behaviour
  • Other side effects
  • Practical correctness issues
• Controlling Transformations
  • Reducing the number of choice points
  • Giving priority to choices
  • Control and completeness
  • Examples of control heuristics
• Implementing Transformations
  • Implementation in LambdaProlog
  • Structuring partial evaluation using monads
  • Maintaining types during partial evaluation
• System Evaluation
  • Type inference
  • Evaluation
  • Partial evaluation
  • Common sub-expression elimination
  • Inlining
• Conclusion
  • A better partial evaluator?
  • Correctness issues
  • Control issues
  • New ways of implementation
  • Future work
  • Completely different ways
• Miscellaneous Examples
  • Fibonacci in O(log_n) — Haskell code
• Components of the system
• Examples of System Code
  • Code of effect monad
  • Code of monadic partial evaluator

This document was translated from L^AT_EX by H^EV^EA.