TY - JOUR AU - Filinski, Andrzej AU - Rohde, Henning Korsholm PY - 2005/02/11 Y2 - 2024/03/29 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 -