Normalisation by evaluation


In programming language semantics, normalisation by evaluation is a style of obtaining the normal form of terms in the λ calculus by appealing to their denotational semantics. A term is first interpreted into a denotational model of the λ-term structure, and then a canonical representative is extracted by reifying the denotation. Such an essentially semantic approach differs from the more traditional syntactic description of normalisation as a reductions in a term rewrite system where β-reductions are allowed deep inside λ-terms.
NBE was first described for the simply typed lambda calculus. It has since been extended both to weaker type systems such as the untyped lambda calculus using a domain theoretic approach, and to richer type systems such as several variants of Martin-Löf type theory.

Outline

Consider the simply typed lambda calculus, where types τ can be basic types, function types, or products, given by the following Backus–Naur form grammar :
These can be implemented as a datatype in the meta-language; for example, for Standard ML, we might use:

datatype ty = Basic of string
| Arrow of ty * ty
| Prod of ty * ty

Terms are defined at two levels. The lower syntactic level is the representation that one intends to normalise.
Here lam/app are the intro/elim forms for →, and x are variables. These terms are intended to be implemented as a first-order in the meta-language:

datatype tm = var of string
| lam of string * tm | app of tm * tm
| pair of tm * tm | fst of tm | snd of tm

The denotational semantics of terms in the meta-language interprets the constructs of the syntax in terms of features of the meta-language; thus, lam is interpreted as abstraction, app as application, etc. The semantic objects constructed are as follows:
Note that there are no variables or elimination forms in the semantics; they are represented simply as syntax. These semantic objects are represented by the following datatype:

datatype sem = LAM of
| PAIR of sem * sem
| SYN of tm

There are a pair of type-indexed functions that move back and forth between the syntactic and semantic layer. The first function, usually written ↑τ, reflects the term syntax into the semantics, while the second reifies the semantics as a syntactic term. Their definitions are mutually recursive as follows:

These definitions are easily implemented in the meta-language:


fun reflect t =
LAM
| reflect t =
PAIR
| reflect t =
SYN t

and reify =
let x = fresh_var in
Lam )
end
| reify =
Pair
| reify = t

By induction on the structure of types, it follows that if the semantic object S denotes a well-typed term s of type τ, then reifying the object produces the β-normal η-long form of s. All that remains is, therefore, to construct the initial semantic interpretation S from a syntactic term s. This operation, written ∥sΓ, where Γ is a context of bindings, proceeds by induction solely on the term structure:

In the implementation:


fun meaning G t =
case t of
var x => lookup G x
| lam => LAM
| app =>
| pair => PAIR
| fst s =>
| snd t =>

Note that there are many non-exhaustive cases; however, if applied to a closed well-typed term, none of these missing cases are ever encountered. The NBE operation on closed terms is then:


fun nbe a t = reify a

As an example of its use, consider the syntactic term SKK defined below:

val K = lam
val S = lam, app ))))
val SKK = app

This is the well-known encoding of the identity function in combinatory logic. Normalising it at an identity type produces:

- nbe SKK;
val it = lam : tm

The result is actually in η-long form, as can be easily seen by normalizing it at a different identity type:

- nbe, Arrow )) SKK;
val it = lam : tm