From Reduction-Based to Reduction-Free Normalization

We document an operational method to construct reduction-free normalization functions. Starting from a reduction-based normalization function from a reduction semantics, i.e., the iteration of a one-step reduction function, we successively subject it to refocusing (i.e., deforestation of the intermediate successive terms in the reduction sequence), equational simplification, refunctionalization (i.e., the converse of defunctionalization), and direct-style transformation (i.e., the converse of the CPS transformation), ending with a reduction-free normalization function of the kind usually crafted by hand. We treat in detail four simple examples: calculating arithmetic expressions, recognizing Dyck words, normalizing lambda-terms with explicit substitutions and call/cc, and flattening binary trees.

The overall method builds on previous work by the author and his students on a syntactic correspondence between reduction semantics and abstract machines and on a functional correspondence between evaluators and abstract machines. The measure of success of these two correspondences is that each of the inter-derived semantic artifacts (i.e., man-made constructs) could plausibly have been written by hand, as is the actual case for several ones derived here.