From Reduction-Based to Reduction-Free Normalization
AbstractWe 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.
How to Cite
Danvy, O. (2004). From Reduction-Based to Reduction-Free Normalization. BRICS Report Series, 11(30). https://doi.org/10.7146/brics.v11i30.21855
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.