A formal development of an efficient supercombination compiler (Q1820575)

This paper presents a formal development, employing techniques of transformational programming, of a non-trivial algorithm in the field of functional language implementation. The problem deals with the translation of lambda calculus expressions into combinator form, using Hughes-style supercombinators rather than the fixed repertoire of combinators proposed by Turner. The final algorithm is presented as a functional program and is efficient in the sense that its worst-case running time is proportional to n log n, where n is the size of the output. This efficiency is obtained by means of a number of simple transformations on the initial specification of the problem, the most significant of which is a data structure refinement step for tabulating partial results.