The precise definition of Normalization By Evaluation?

Question

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
  | VAdd1 Value
  | 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?

Answer 1

The difference you see between higher-order and closure-based representations is a lot smaller than it first seems: the closure-based representation arises as the defunctionalisation of the higher-order algorithm.

This was first introduced (to my knowledge) in Andreas Abel's 2013 habilitation thesis, Normalization by Evaluation: Dependent Types and Impredicativity