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.<ref name="berger schwichtenberg lics-91">{{cite journal|author=Berger, Ulrich|author2=Schwichtenberg, Helmut |year=1991|title=An inverse of the evaluation functional for typed λ-calculus|journal=LICS}}</ref> It has since been extended both to weaker type systems such as the untyped lambda calculus<ref name="filinski rohde fossacs-05">{{cite conference|last1=Filinski|first1=Andrzej|last2=Rohde|first2=Henning Korsholm|year=2005|title=A denotational account of untyped normalization by evaluation|url=https://tidsskrift.dk/brics/article/view/21870|book-title=Foundations of Software Science and Computation Structures (FOSSACS)|volume=10|issue=40|doi=10.7146/brics.v12i4.21870|doi-access=free}}</ref> using a domain theoretic approach, and to richer type systems such as several variants of Martin-Löf type theory.<ref name="coquand dybjer mscs-97">{{cite journal|last1=Coquand|first1=Thierry|last2=Dybjer|first2=Peter|journal=Mathematical Structure in Computer Science|year=1997|volume=7|issue=1|pages=75–94|title=Intuitionistic model constructions and normalization proofs|doi=10.1017/S0960129596002150 }}</ref><ref name="abel aehlig dybjer mfps-07">{{cite journal|author=Abel, Andreas|author2=Aehlig, Klaus |author3=Dybjer, Peter |year=2007|title=Normalization by Evaluation for Martin-Löf Type Theory with One Universe|url=http://www.tcs.informatik.uni-muenchen.de/~abel/nbemltt.pdf|journal=MFPS}}</ref><ref name="abel coquand dybjer lics-07">{{cite journal|author=Abel, Andreas|author2=Coquand, Thierry |author3=Dybjer, Peter |year=2007|title=Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements|url=http://www.cse.chalmers.se/~peterd/papers/NbeMLTTEqualityJudgements.pdf|journal=LICS}}</ref><ref name="gratzer sterling birkedal icpf-19">{{cite journal|author=Gratzer, Daniel|author2=Sterling, Jon |author3=Birkedal, Lars |year=2019|title=Implementing a Modal Dependent Type Theory|url=https://jozefg.github.io/papers/2019-implementing-modal-dependent-type-theory.pdf|journal=ICFP}}</ref>

== 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) τ ::= α | τ1 → τ2 | τ1 × τ2

These can be implemented as a datatype in the meta-language; for example, for Standard ML, we might use: <syntaxhighlight lang="sml"> datatype ty = Basic of string | Arrow of ty * ty | Prod of ty * ty </syntaxhighlight> Terms are defined at two levels.<ref name="danvy popl 96">{{Cite FTP |first=Olivier |last=Danvy |author-link=Olivier Danvy |title=Type-directed partial evaluation|url=ftp://ftp.daimi.au.dk/pub/empl/danvy/Papers/danvy-popl96.ps.gz|format=gzipped PostScript|year=1996|server=POPL |url-status=dead |pages=242–257}}</ref> 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 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:

<syntaxhighlight lang="sml"> datatype sem = LAM of (sem -> sem) | PAIR of sem * sem | SYN of tm </syntaxhighlight>

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:

<blockquote><math> \begin{align} \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{align} </math></blockquote>

These definitions are easily implemented in the meta-language:

<syntaxhighlight lang="sml"> (* 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 </syntaxhighlight>

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:

<blockquote><math> \begin{align} \| \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{align} </math></blockquote>

In the implementation:

<syntaxhighlight lang="sml"> 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) </syntaxhighlight>

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:

<syntaxhighlight lang="sml"> (* nbe : ty -> tm -> tm *) fun nbe a t = reify a (meaning empty t) </syntaxhighlight>

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:

<syntaxhighlight lang="sml"> - nbe (Arrow (Basic "a", Basic "a")) SKK; val it = lam ("v0",var "v0") : tm </syntaxhighlight>

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

<syntaxhighlight lang="sml"> - 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 </syntaxhighlight>

== 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>.<ref name="filinski ppdp-99">{{cite conference|title=A Semantic Account of Type-Directed Partial Evaluation|last1=Filinski|first1=Andrzej|book-title=Principles and Practice of Declarative Programming|url=https://tidsskrift.dk/brics/article/view/20074|doi=10.7146/brics.v6i17.20074|doi-access=free}}</ref>

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.<ref name="danvy rhiger rose jfp-01">{{cite journal|last1=Danvy|first1=Olivier|last2=Rhiger|first2=Morten|last3=Rose|first3=Kristoffer|journal=Journal of Functional Programming|year=2001|volume=11|issue=6|pages=673–680|title=Normalization by Evaluation with Typed Abstract Syntax|doi=10.1017/S0956796801004166 |url=https://tidsskrift.dk/brics/article/view/20473}}</ref>

Normalization by evaluation also scales to the simply typed lambda calculus with sums (<code>+</code>),<ref name="danvy popl 96"/> using the delimited control operators <code>shift</code> and <code>reset</code>.<ref name="danvy filinski lfp-90">{{cite conference|title=Abstracting Control|last1=Danvy|first1=Olivier|last2=Filinski|first2=Andrzej|book-title=LISP and Functional Programming|year=1990|pages=151–160|isbn=0-89791-368-X|doi=10.1145/91556.91622|s2cid=6426191|doi-access=free }}</ref>

== See also ==

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

== References ==

{{DEFAULTSORT:Normalisation By Evaluation}} Category:Lambda calculus Category:Programming language semantics