Normalisation by evaluation

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) τ ::= α | τ₁ → τ₂ | τ₁ × τ₂

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 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 ↑_τ, reflects the term syntax into the semantics, while the second reifies the semantics as a syntactic term (written as ↓^τ). Their definitions are mutually recursive as follows:

↑ α t = S Y N   t ↑ τ 1 → τ 2 v = L A M ( λ S .   ↑ τ 2 ( a p p   ( v , ↓ τ 1 S ) ) ) ↑ τ 1 × τ 2 v = P A I R ( ↑ τ 1 ( f s t   v ) , ↑ τ 2 ( s n d   v ) ) ↓ α ( S Y N   t ) = t ↓ τ 1 → τ 2 ( L A M   S ) = l a m   ( x , ↓ τ 2 ( S   ( ↑ τ 1 ( v a r   x ) ) ) )  where  x  is fresh ↓ τ 1 × τ 2 ( P A I R   ( S , T ) ) = p a i r   ( ↓ τ 1 S , ↓ τ 2 T )

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., ↓^τ 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∥_Γ, where Γ is a context of bindings, proceeds by induction solely on the term structure:

∥ v a r   x ∥ Γ = Γ ( x ) ∥ l a m   ( x , s ) ∥ Γ = L A M   ( λ S .   ∥ s ∥ Γ , x ↦ S ) ∥ a p p   ( s , t ) ∥ Γ = S   ( ∥ t ∥ Γ )  where  ∥ s ∥ Γ = L A M   S ∥ p a i r   ( s , t ) ∥ Γ = P A I R   ( ∥ s ∥ Γ , ∥ t ∥ Γ ) ∥ f s t   s ∥ Γ = S  where  ∥ s ∥ Γ = P A I R   ( S , T ) ∥ s n d   t ∥ Γ = T  where  ∥ t ∥ Γ = P A I R   ( S , T )

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 SKK 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: