Improvements in a functional core language with call-by-need operational semantics

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 decreased. This paper investigates improvements in both – an untyped and a polymorphically typed – call-by-need lambda-calculus with letrec, case, constructors and seq. Besides showing that several local optimizations are improvements, the main result of the paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in Moran and Sands’ improvement theory. We also prove that several different length measures used for improvement in Moran and Sands’ call-by-need calculus and our calculus are equivalent.

• Type: Journal
• Year: 2015
• Where: PPDP
• Authors: Manfred Schmidt-Schauß, David Sabel
• Keywords: PPDP 2015, Programming Languages