<p>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 <a href="https://en.wikipedia.org/wiki/Defunctionalization" rel="noreferrer">defunctionalisation</a> of the higher-order algorithm.</p>
<p>This was first introduced (to my knowledge) in Andreas Abel's 2013 habilitation thesis, <a href="https://www.cse.chalmers.se/%7Eabela/habil.pdf" rel="noreferrer"><em>Normalization by Evaluation: Dependent Types and Impredicativity</em></a></p>

CC BY-SA 4.0
2022-11-14T10:24:48.343Z
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...
hirrolot
CC BY-SA 4.0
2022-11-14T09:20:18.743Z
2022-11-14T09:20:18.743Z
Neel Krishnaswami
<p>The <a href="https://en.wikipedia.org/wiki/Normalisation_by_evaluation" rel="noreferrer">Wikipedia article</a> suggests that NbE is a technique for obtaining &quot;the normal form of terms&quot; by translating the object language into abstractions of the meta (host) language:</p>
<blockquote>
<p>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.</p>
</blockquote>
<p>One consequence is that we are now restricted to use <a href="https://en.wikipedia.org/wiki/Higher-order_abstract_syntax" rel="noreferrer">Higher-Order Abstract Syntax (HOAS)</a> to represent lambda terms, since De Bruijn indices and named representations are formally not &quot;features&quot; of the host language, e.g., Haskell. That article uses HOAS, accordingly.</p>
<p>Another publication (or rather a tutorial) called <a href="https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf" rel="noreferrer">&quot;Checking Dependent Types with Normalization by Evaluation: A Tutorial&quot;</a>, however, uses a bit different approach; in particular, it employs string variable identifiers instead of HOAS and a so-called &quot;closure&quot; construction, which is essentially a lambda abstraction packaged up with all the free variables occurring in its body:</p>
<pre><code>data Value
  = VZero
  | VAdd1 Value
  | VClosure (Env Value) Name Expr
  | VNeutral Ty Neutral
  deriving (Show)
</code></pre>
<p>Another thing to note is that the closure's body is not fully evaluated even after invoking <code>eval</code> (under eager evaluation), as witnessed by the <code>Expr</code> type. Also, in the aforementioned Wikipedia article, <code>reflect</code> (<code>eval</code>) and <code>reify</code> (<code>readBack</code>) are mutually recursive, whereas in the Haskell tutorial only <code>readBack</code> calls <code>eval</code> when it encounters an unevaluated closure body. The author still recognizes the approach as NbE though.</p>
<p>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 &quot;Normalization by Evaluation&quot;. The only common thing I was able to notice is that all implementations include the evaluation (<code>eval</code>, <code>reflect</code>) and quoting (<code>readBack</code>, <code>reify</code>) functions which, when composed together, yield an interpreter.</p>
<p>In the PLT discourse, what is NbE exactly?</p>

CC BY-SA 4.0
2022-11-13T14:51:45.453Z
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.
Andrej Bauer
CC BY-SA 4.0
2022-11-13T14:57:26.793Z
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?
hirrolot
CC BY-SA 4.0
2022-11-13T19:55:19.027Z
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.
Andrej Bauer
CC BY-SA 4.0
2022-11-14T04:55:52.350Z
Ok, thanks, that makes sense.
hirrolot
<type-theory><pl.programming-languages><lambda-calculus><denotational-semantics><normalization>
The precise definition of Normalization By Evaluation?
hirrolot
# The precise definition of Normalization By Evaluation?

(Asked by: username_0 on 2022-11-13)

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?

**Tags:** type-theory, pl.programming-languages, lambda-calculus, denotational-semantics, normalization
> **Comments:**
> **username_1**: 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.  
> **username_0**: 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?  
> **username_1**: 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.  
> **username_0**: Ok, thanks, that makes sense.  

---

## 1 answers

### Answer by username_2 on 2022-11-14. Score: 8 | Accepted answer

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](https://en.wikipedia.org/wiki/Defunctionalization) 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*](https://www.cse.chalmers.se/%7Eabela/habil.pdf)

> **Comments:**
> **username_0**: 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...  

---

