TY - JOUR
AU - Filinski, Andrzej
AU - Rohde, Henning Korsholm
PY - 2003/12/06
Y2 - 2022/11/27
TI - A Denotational Account of Untyped Normalization by Evaluation
JF - BRICS Report Series
JA - BRICS
VL - 10
IS - 40
SE - Articles
DO - 10.7146/brics.v10i40.21808
UR - https://tidsskrift.dk/brics/article/view/21808
SP -
AB - We show that the standard normalization-by-evaluation construction for the simply-typed lambda_{beta eta}-calculus has a natural counterpart for the untyped lambda_beta-calculus, with the central type-indexed logical relation replaced by a "recursively defined'' <em>invariant relation</em>, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.<br /> <br />In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of <em>soundness</em> (the output term, if any, is beta-equivalent to the input term); <em>standardization</em> ( beta-equivalent terms are mapped to the same result); and <em>completeness</em> (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like call-by-value language.
ER -