We show that the standard normalization-by-evaluation construction for the
simply-typed λβη-calculus
has a natural counterpart for the untyped
λβ-calculus, with the central type-indexed logical relation
replaced by a “recursively defined” invariant relation, 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.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 soundness (the output term, if
any, is in normal form and β-equivalent to the input term);
identification (β-equivalent terms are mapped to the
same result); and completeness (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. Finally, we generalize the construction to produce an
infinitary variant of normal forms, namely Böhm trees.
We show that the three-part characterization of correctness,
as well as the proofs, extend naturally to this generalization.