Improvements in a call-by-need functional core language: Common subexpression elimination and resource preserving translations

An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is not strictly increased in any context. This paper investigates improvements in both - an untyped and a polymorphically typed variant - of a call-by-need lambda calculus with letrec, case, constructors and seq. Besides showing that several local transformations are optimizations, a main result of this paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in the improvement theory of Moran and Sands. The improvement relation used in this paper is generic in which essential computation steps are counted and thus the obtained results apply for several notions of improvement. Besides the small-step operational semantics, also an abstract machine semantics is considered for counting computation steps. We show for several length measures that the call-by-need calculus of Moran and Sands and our calculus are equivalent.