Operational aspects of untyped Normalisation by Evaluation
Klaus Aehlig, Felix Joachimski · Mathematical Structures in Computer Science · 2004
A purely syntactic and untyped variant of Normalisation by Evaluation for the $\lambda$ -calculus is presented in the framework of a two-level $\lambda$ -calculus with rewrite rules to model the inverse of the evaluation functional. Among its operational properties there is a standardisation theorem that formally establishes the adequacy of implementation in functional programming languages. An example implementation in Haskell is provided. The relation to the usual type-directed Normalisation by Evaluation is highlighted, using a short analysis of $\eta$ -expansion that leads to a perspicuous strong normalisation and confluence proof for $\beta\eta\!\up$ -reduction as a byproduct.