5
$\begingroup$

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?

$\endgroup$
4
  • 1
    $\begingroup$ 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. $\endgroup$ Nov 13 at 14:51
  • $\begingroup$ 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? $\endgroup$
    – Hirrolot
    Nov 13 at 14:57
  • $\begingroup$ 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. $\endgroup$ Nov 13 at 19:55
  • $\begingroup$ Ok, thanks, that makes sense. $\endgroup$
    – Hirrolot
    Nov 14 at 4:55

1 Answer 1

7
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ Wow, thank you! I've heard about defunctionalization a bit, but the idea that closures are basically defunctionalized HOAS hasn't come to my mind... $\endgroup$
    – Hirrolot
    Nov 14 at 10:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.