TY - JOUR
AU - Filinski, Andrzej
AU - Rohde, Henning Korsholm
PY - 2005/02/11
Y2 - 2022/11/27
TI - Denotational Aspects of Untyped Normalization by Evaluation
JF - BRICS Report Series
JA - BRICS
VL - 12
IS - 4
SE - Articles
DO - 10.7146/brics.v12i4.21870
UR - https://tidsskrift.dk/brics/article/view/21870
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 in normal form and beta-equivalent to the input term); <em>identification</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.<br /> <br />Finally, we generalize the construction to produce an infinitary variant of normal forms, namely <em>Böhm trees</em>. We show that the three-part characterization of correctness, as well as the proofs, extend naturally to this generalization.
ER -