Normalisation by evaluation

In programming language semantics, normalisation by evaluation (NBE) 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 (β-normal and η-long) 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. ↑ α 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 ) {displaystyle {egin{aligned}uparrow _{alpha }t&=mathbf {SYN} t\uparrow _{ au _{1} o au _{2}}v&=mathbf {LAM} (lambda S. uparrow _{ au _{2}}(mathbf {app} (v,downarrow ^{ au _{1}}S)))\uparrow _{ au _{1} imes au _{2}}v&=mathbf {PAIR} (uparrow _{ au _{1}}(mathbf {fst} v),uparrow _{ au _{2}}(mathbf {snd} v))\downarrow ^{alpha }(mathbf {SYN} t)&=t\downarrow ^{ au _{1} o au _{2}}(mathbf {LAM} S)&=mathbf {lam} (x,downarrow ^{ au _{2}}(S (uparrow _{ au _{1}}(mathbf {var} x)))){ ext{ where }}x{ ext{ is fresh}}\downarrow ^{ au _{1} imes au _{2}}(mathbf {PAIR} (S,T))&=mathbf {pair} (downarrow ^{ au _{1}}S,downarrow ^{ au _{2}}T)end{aligned}}} ‖ 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 ) {displaystyle {egin{aligned}|mathbf {var} x|_{Gamma }&=Gamma (x)\|mathbf {lam} (x,s)|_{Gamma }&=mathbf {LAM} (lambda S. |s|_{Gamma ,xmapsto S})\|mathbf {app} (s,t)|_{Gamma }&=S (|t|_{Gamma }){ ext{ where }}|s|_{Gamma }=mathbf {LAM} S\|mathbf {pair} (s,t)|_{Gamma }&=mathbf {PAIR} (|s|_{Gamma },|t|_{Gamma })\|mathbf {fst} s|_{Gamma }&=S{ ext{ where }}|s|_{Gamma }=mathbf {PAIR} (S,T)\|mathbf {snd} t|_{Gamma }&=T{ ext{ where }}|t|_{Gamma }=mathbf {PAIR} (S,T)end{aligned}}} In programming language semantics, normalisation by evaluation (NBE) 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 (β-normal and η-long) 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. 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): 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. 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: