<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](https://en.wikipedia.org/wiki/Normalisation_by_evaluation) 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)](https://en.wikipedia.org/wiki/Higher-order_abstract_syntax) 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"](https://davidchristiansen.dk/tutorials/implementing-types-hs.pdf), 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...  

---

