@article{Danvy_2004, title={From Reduction-Based to Reduction-Free Normalization}, volume={11}, url={https://tidsskrift.dk/brics/article/view/21855}, DOI={10.7146/brics.v11i30.21855}, abstractNote={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.<br /> <br />The construction builds on previous work on refocusing and on a functional correspondence between evaluators and abstract machines. It is also reversible.}, number={30}, journal={BRICS Report Series}, author={Danvy, Olivier}, year={2004}, month={Dec.} }