my-server
← Wiki Redirected from Normalization by evaluation

Normalisation by evaluation

In programming language semantics, normalisation by evaluation (NBE) is a method 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 (β-normal and η-long) representative is extracted by reifying the denotation. Such an essentially semantic, reduction-free, approach differs from the more traditional syntactic, reduction-based, description of normalisation as 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 (→ associating to the right, as usual):

(Types) τ ::= α | τ<sub>1</sub> → τ<sub>2</sub> | τ<sub>1</sub> × τ<sub>2</sub>

These can be implemented as a datatype in the meta-language; for example, for Standard ML, we might use:

Terms are defined at two levels. The lower syntactic level (sometimes called the dynamic level) is the representation that one intends to normalise.

(Syntax Terms) s,t,… ::= var x | lam (x, t) | app (s, t) | pair (s, t) | fst t | snd t

Here lam/app (resp. pair/fst,snd) are the intro/elim forms for → (resp. ×), and x are variables. These terms are intended to be implemented as a first-order datatype in the meta-language:

The denotational semantics of (closed) 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:

(Semantic Terms) S,T,… ::= LAM (λx. S x) | PAIR (S, T) | SYN t

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:

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

<blockquote></blockquote>

These definitions are easily implemented in the meta-language:

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 (i.e., ↓<sup>τ</sup> S) 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∥<sub>Γ</sub>, where Γ is a context of bindings, proceeds by induction solely on the term structure:

<blockquote></blockquote>

In the implementation:

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:

As an example of its use, consider the syntactic term <code>SKK</code> defined below:

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

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

Variants

Using de Bruijn levels instead of names in the residual syntax makes <code>reify</code> a pure function in that there is no need for <code>fresh_var</code>.

The datatype of residual terms can also be the datatype of residual terms in normal form. The type of <code>reify</code> (and therefore of <code>nbe</code>) then makes it clear that the result is normalized. And if the datatype of normal forms is typed, the type of <code>reify</code> (and therefore of <code>nbe</code>) then makes it clear that normalization is type preserving.

Normalization by evaluation also scales to the simply typed lambda calculus with sums (<code>+</code>), using the delimited control operators <code>shift</code> and <code>reset</code>.

See also

References