# The precise definition of Normalization By Evaluation?

The Wikipedia article suggests that NbE is a technique for obtaining "the normal form of terms" by translating the object language into abstractions of the meta (host) 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.

One consequence is that we are now restricted to use Higher-Order Abstract Syntax (HOAS) to represent lambda terms, since De Bruijn indices and named representations are formally not "features" of the host language, e.g., Haskell. That article uses HOAS, accordingly.

Another publication (or rather a tutorial) called "Checking Dependent Types with Normalization by Evaluation: A Tutorial", however, uses a bit different approach; in particular, it employs string variable identifiers instead of HOAS and a so-called "closure" construction, which is essentially a lambda abstraction packaged up with all the free variables occurring in its body:

data Value
= VZero
| VClosure (Env Value) Name Expr
| VNeutral Ty Neutral
deriving (Show)


Another thing to note is that the closure's body is not fully evaluated even after invoking eval (under eager evaluation), as witnessed by the Expr type. Also, in the aforementioned Wikipedia article, reflect (eval) and reify (readBack) are mutually recursive, whereas in the Haskell tutorial only readBack calls eval when it encounters an unevaluated closure body. The author still recognizes the approach as NbE though.

Many NbE implementations that I was able to find throughout the Internet differ in these tiny but important aspects. I am therefore a tad perplexed with regard to what to call "Normalization by Evaluation". The only common thing I was able to notice is that all implementations include the evaluation (eval, reflect) and quoting (readBack, reify) functions which, when composed together, yield an interpreter.

In the PLT discourse, what is NbE exactly?

• It's pretty much what you described. A method for finding normal forms by evaluating expressions to "some place" and then reconstructing the normal form from the result. Nov 13 at 14:51
• Ok, so basically NbE means that I have some "value" representation of an object language and two functions mapping a term to a value and vice versa; the rest of the stuff are just implementation details? In particular, if I employ the same approach as with closures, but fully evaluate the closure's body in eval, leaving its environment empty, can I still call this NbE? Nov 13 at 14:57
• As you said, it's a technique. I am not aware of a broad formal definition. Anything that is done in the spirit of existing examples can probably be called NbE. Nov 13 at 19:55
• Ok, thanks, that makes sense. Nov 14 at 4:55