<p>NbE really has 2 goals:</p>
<ol>
<li><p>As an evaluation mechanism for <span class="math-container">$\lambda$</span>-terms. In this regard there are many many alternatives, basically any interpreter, virtual machine or compiler is a possible approach. NbE is just a way to get the host language to do the compilation for you!</p>
</li>
<li><p>As a <em>proof technique</em> to show the decidability of convertability for <em>typed</em> lambda calculi. E.g. it is decidable to prove <span class="math-container">$t =_{\beta\eta} u$</span> if <span class="math-container">$t$</span> and <span class="math-container">$u$</span> are simply typed terms of the same type. The obvious alternative is: proving that <span class="math-container">$\beta\eta$</span>-reduction is strongly normalizing and confluent. It's not clear whether you're lumping this in with NbE, because they (usually) both use logical relations at their core. Certainly there are systems for which SN does <em>not</em> hold, but for which we can carry out NbE though.</p>
</li>
</ol>

CC BY-SA 4.0
2021-05-26T15:28:31.077Z
2021-05-26T15:28:31.077Z
cody
<p>Reading about lambda calculus I got the impression that normalization <strong>is</strong> evaluation.</p>
<p>So I don't understand what is meant by Normalization by Evaluation (used e.g. in several <a href="https://www.cse.chalmers.se/%7Eabela/publications.html" rel="noreferrer">publications</a> of A. Abel).</p>
<p>Can you explain what are the alternative paths to the goals achieved by NbE?</p>

CC BY-SA 4.0
2021-05-17T07:32:19.283Z
I too would like to know alternatives to nbe other than [heriditary substitution](http://twelf.org/wiki/Hereditary_substitution). The difference between NBE and evaluation is that evaluation, for example, does not reduce "inside" a lambda term.  Given the term `t = (λ x ((λ y y) x))`, evaluation will get stuck, since there is no outer redex. NBE will evaluate the inner redex of `(λ y y) x)` to the normal form `x`. This normalizes the term `t` into `t -> (λ x x)`. Intuitively, NBE extends the evaluation rules of lambda calculus to work "inside stuck terms" as well.
Siddharth Bhat
CC BY-SA 4.0
2021-05-17T09:00:21.840Z
You should be careful with terminology here because it is not universally agreed upon. Some people call "evaluation" what you're describing, but others equation evaluation and normalization.
Andrej Bauer
<lo.logic><type-theory><lambda-calculus>
Alternatives to Normalization by Evaluation
nbe
# Alternatives to Normalization by Evaluation

(Asked by: username_0 on 2021-05-17)

Reading about lambda calculus I got the impression that normalization **is** evaluation.

So I don't understand what is meant by Normalization by Evaluation (used e.g. in several [publications](https://www.cse.chalmers.se/%7Eabela/publications.html) of A. Abel).

Can you explain what are the alternative paths to the goals achieved by NbE?

**Tags:** lo.logic, type-theory, lambda-calculus

> **Comments:**
> **username_1**: I too would like to know alternatives to username_0 other than [heriditary substitution](http://twelf.org/wiki/Hereditary_substitution). The difference between NBE and evaluation is that evaluation, for example, does not reduce "inside" a lambda term.  Given the term `t = (λ x ((λ y y) x))`, evaluation will get stuck, since there is no outer redex. NBE will evaluate the inner redex of `(λ y y) x)` to the normal form `x`. This normalizes the term `t` into `t -> (λ x x)`. Intuitively, NBE extends the evaluation rules of lambda calculus to work "inside stuck terms" as well.  
> **username_2**: You should be careful with terminology here because it is not universally agreed upon. Some people call "evaluation" what you're describing, but others equation evaluation and normalization.  

---

## 1 answers

### Answer by username_3 on 2021-05-26. Score: 1

NbE really has 2 goals:

1. As an evaluation mechanism for $\lambda$-terms. In this regard there are many many alternatives, basically any interpreter, virtual machine or compiler is a possible approach. NbE is just a way to get the host language to do the compilation for you!
2. As a *proof technique* to show the decidability of convertability for *typed* lambda calculi. E.g. it is decidable to prove $t =\_{\beta\eta} u$ if $t$ and $u$ are simply typed terms of the same type. The obvious alternative is: proving that $\beta\eta$-reduction is strongly normalizing and confluent. It's not clear whether you're lumping this in with NbE, because they (usually) both use logical relations at their core. Certainly there are systems for which SN does *not* hold, but for which we can carry out NbE though.


---

