From Self-Interpreters to Normalization by Evaluation

TL;DR

This paper systematically derives an untyped normalization by evaluation algorithm from a standard interpreter for the lambda calculus, highlighting the connection between self-interpreters, self-reducers, and normalization techniques.

Contribution

It provides a systematic derivation of normalization by evaluation from an interpreter, clarifying the role of representation schemes in the process.

Findings

Derivation of normalization by evaluation from a standard interpreter

Connection between self-interpreters, self-reducers, and normalization algorithms

Framework applicable to various representation schemes

Abstract

We characterize normalization by evaluation as the composition of a self-interpreter with a self-reducer using a special representation scheme, in the sense of Mogensen (1992). We do so by deriving in a systematic way an untyped normalization by evaluation algorithm from a standard interpreter for the ?-calculus. The derived algorithm is not novel and indeed other published algorithms may be obtained in the same manner through appropriate adaptations to the representation scheme.