Normalisation by evaluation

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:

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

Terms are defined at two levels.[7] 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:

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

 datatype sem = LAM of (sem -> sem)
              | 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 (written as ↓^τ). Their definitions are mutually recursive as follows:

${\displaystyle {\begin{aligned}\uparrow _{\alpha }t&=\mathbf {SYN} \ t\\\uparrow _{\tau _{1}\to \tau _{2}}v&=\mathbf {LAM} (\lambda S.\ \uparrow _{\tau _{2}}(\mathbf {app} \ (v,\downarrow ^{\tau _{1}}S)))\\\uparrow _{\tau _{1}\times \tau _{2}}v&=\mathbf {PAIR} (\uparrow _{\tau _{1}}(\mathbf {fst} \ v),\uparrow _{\tau _{2}}(\mathbf {snd} \ v))\\[1ex]\downarrow ^{\alpha }(\mathbf {SYN} \ t)&=t\\\downarrow ^{\tau _{1}\to \tau _{2}}(\mathbf {LAM} \ S)&=\mathbf {lam} \ (x,\downarrow ^{\tau _{2}}(S\ (\uparrow _{\tau _{1}}(\mathbf {var} \ x)))){\text{ where }}x{\text{ is fresh}}\\\downarrow ^{\tau _{1}\times \tau _{2}}(\mathbf {PAIR} \ (S,T))&=\mathbf {pair} \ (\downarrow ^{\tau _{1}}S,\downarrow ^{\tau _{2}}T)\end{aligned}}}$

These definitions are easily implemented in the meta-language:

 (* fresh_var : unit -> string *)
 val variable_ctr = ref ~1
 fun fresh_var () = 
      (variable_ctr := 1 + !variable_ctr; 
       "v" ^ Int.toString (!variable_ctr))

 (* reflect : ty -> tm -> sem *)
 fun reflect (Arrow (a, b)) t =
       LAM (fn S => reflect b (app (t, (reify a S))))
   | reflect (Prod (a, b)) t =
       PAIR (reflect a (fst t), reflect b (snd t))
   | reflect (Basic _) t =
       SYN t

 (* reify   : ty -> sem -> tm *)
 and reify (Arrow (a, b)) (LAM S) =
       let val x = fresh_var () in
         lam (x, reify b (S (reflect a (var x))))
       end
   | reify (Prod (a, b)) (PAIR (S, T)) =
       pair (reify a S, reify b T)
   | reify (Basic _) (SYN t) = 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 (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:

${\displaystyle {\begin{aligned}\|\mathbf {var} \ x\|_{\Gamma }&=\Gamma (x)\\\|\mathbf {lam} \ (x,s)\|_{\Gamma }&=\mathbf {LAM} \ (\lambda S.\ \|s\|_{\Gamma ,x\mapsto S})\\\|\mathbf {app} \ (s,t)\|_{\Gamma }&=S\ (\|t\|_{\Gamma }){\text{ where }}\|s\|_{\Gamma }=\mathbf {LAM} \ S\\\|\mathbf {pair} \ (s,t)\|_{\Gamma }&=\mathbf {PAIR} \ (\|s\|_{\Gamma },\|t\|_{\Gamma })\\\|\mathbf {fst} \ s\|_{\Gamma }&=S{\text{ where }}\|s\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\\\|\mathbf {snd} \ t\|_{\Gamma }&=T{\text{ where }}\|t\|_{\Gamma }=\mathbf {PAIR} \ (S,T)\end{aligned}}}$

In the implementation:

 datatype ctx = empty 
              | add of ctx * (string * sem)

 (* lookup : ctx -> string -> sem *)
 fun lookup (add (remdr, (y, value))) x = 
       if x = y then value else lookup remdr x

 (* meaning : ctx -> tm -> sem *)
 fun meaning G t =
       case t of
         var x => lookup G x
       | lam (x, s) => LAM (fn S => meaning (add (G, (x, S))) s)
       | app (s, t) => (case meaning G s of
                          LAM S => S (meaning G t))
       | pair (s, t) => PAIR (meaning G s, meaning G t)
       | fst s => (case meaning G s of
                     PAIR (S, T) => S)
       | snd t => (case meaning G t of
                     PAIR (S, T) => 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:

 (* nbe : ty -> tm -> tm *)
 fun nbe a t = reify a (meaning empty t)

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

 val K = lam ("x", lam ("y", var "x"))
 val S = lam ("x", lam ("y", lam ("z", app (app (var "x", var "z"), app (var "y", var "z")))))
 val SKK = app (app (S, K), K)

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

 - nbe (Arrow (Basic "a", Basic "a")) SKK;
 val it = lam ("v0",var "v0") : tm

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

 - nbe (Arrow (Arrow (Basic "a", Basic "b"), Arrow (Basic "a", Basic "b"))) SKK;
 val it = lam ("v1",lam ("v2",app (var "v1",var "v2"))) : tm

Using de Bruijn levels instead of names in the residual syntax makes reify a pure function in that there is no need for fresh_var.[8]

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

Normalization by evaluation also scales to the simply typed lambda calculus with sums (+),[7] using the delimited control operators shift and reset.[10]

• MINLOG, a proof assistant that uses NBE as its rewrite engine.