# Normalisation by evaluation > Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Normalisation_by_evaluation > Markdown URL: https://mediated.wiki/source/Normalisation_by_evaluation.md > Source: https://en.wikipedia.org/wiki/Normalisation_by_evaluation > Source revision: 1300130726 > License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/) {{format|date=April 2014}} In [programming language](/source/programming_language) [semantics](/source/formal_semantics_of_programming_languages), '''normalisation by evaluation (NBE)''' is a method of obtaining the [normal form](/source/beta_normal_form) of terms in the [λ-calculus](/source/Lambda_calculus) by appealing to their [denotational semantics](/source/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](/source/term_rewrite_system) where [β-reduction](/source/%CE%B2-reduction)s are allowed deep inside λ-terms. NBE was first described for the [simply typed lambda calculus](/source/simply_typed_lambda_calculus).{{cite journal|author=Berger, Ulrich|author2=[Schwichtenberg, Helmut](/source/Helmut_Schwichtenberg) |year=1991|title=An inverse of the evaluation functional for typed λ-calculus|journal=[LICS](/source/Logic_in_Computer_Science)}} It has since been extended both to weaker [type system](/source/type_system)s such as the [untyped lambda calculus](/source/untyped_lambda_calculus){{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}} using a [domain theoretic](/source/domain_theory) approach, and to richer type systems such as several variants of [Martin-Löf type theory](/source/Martin-L%C3%B6f_type_theory).{{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 }}{{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](/source/Mathematical_Foundations_of_Programming_Semantics)}}{{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](/source/Logic_in_Computer_Science)}}{{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](/source/International_Conference_on_Functional_Programming)}} == Outline == Consider the [simply typed lambda calculus](/source/simply_typed_lambda_calculus), where types τ can be basic types (α), function types (→), or products (×), given by the following [Backus–Naur form](/source/Backus%E2%80%93Naur_form) grammar (→ associating to the right, as usual): :(Types) τ ::= α | τ1 → τ2 | τ1 × τ2 These can be implemented as a [datatype](/source/datatype) in the meta-language; for example, for [Standard ML](/source/Standard_ML), we might use: datatype ty = Basic of string | Arrow of ty * ty | Prod of ty * ty Terms are defined at two levels.{{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=[gzip](/source/gzip)ped [PostScript](/source/PostScript)|year=1996|server=[POPL](/source/Principles_of_Programming_Languages) |url-status=dead |pages=242–257}} 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](/source/introduction_rule)/[elim](/source/elimination_rule) forms for → (resp. ×), and ''x'' are [variables](/source/Variable_(programming)). These terms are intended to be implemented as a [first-order](/source/first-order_logic) 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](/source/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:
\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}
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](/source/mathematical_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:
\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}
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](/source/identity_function) in [combinatory logic](/source/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 == Variants == Using [de Bruijn levels](/source/de_Bruijn_index) instead of names in the residual syntax makes reify a pure function in that there is no need for fresh_var.{{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}} 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.{{cite journal|last1=Danvy|first1=Olivier|last2=Rhiger|first2=Morten|last3=Rose|first3=Kristoffer|journal=[Journal of Functional Programming](/source/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}} Normalization by evaluation also scales to the simply typed lambda calculus with sums (+), using the [delimited control operators](/source/delimited_continuation) shift and reset.{{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 }} == See also == * [MINLOG](/source/MINLOG), a [proof assistant](/source/proof_assistant) that uses NBE as its rewrite engine. == References == {{reflist}} {{DEFAULTSORT:Normalisation By Evaluation}} Category:Lambda calculus Category:Programming language semantics --- Adapted from the Wikipedia article [Normalisation by evaluation](https://en.wikipedia.org/wiki/Normalisation_by_evaluation) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Normalisation_by_evaluation?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.