|
From Reduction-Based to Reduction-Free Normalization
Olivier Danvy December 2004 |
Abstract:
We present a systematic construction of a reduction-free
normalization function. Starting from a reduction-based normalization
function, i.e., the transitive closure of a one-step reduction function, we
successively subject it to refocusing (i.e., deforestation of the
intermediate reduced terms), simplification (i.e., fusing auxiliary
functions), refunctionalization (i.e., Church encoding), and direct-style
transformation (i.e., the converse of the CPS transformation). We consider
two simple examples and treat them in detail: for the first one, arithmetic
expressions, we construct an evaluation function; for the second one, terms
in the free monoid, we construct an accumulator-based flatten function. The
resulting two functions are traditional reduction-free normalization
functions.
The construction builds on previous work on refocusing and on a functional correspondence between evaluators and abstract machines. It is also reversible. Available as PostScript, PDF, DVI. |