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 interpretationS 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