TY - JOUR
AU - Danvy, Olivier
PY - 2004/12/11
Y2 - 2023/09/29
TI - From Reduction-Based to Reduction-Free Normalization
JF - BRICS Report Series
JA - BRICS
VL - 11
IS - 30
SE - Articles
DO - 10.7146/brics.v11i30.21855
UR - https://tidsskrift.dk/brics/article/view/21855
SP -
AB - 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.
ER -