Alternatives to Normalization by Evaluation

Question

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 of A. Abel).

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

I too would like to know alternatives to nbe other than heriditary 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, Commented May 17, 2021 at 7:32
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, Commented May 17, 2021 at 9:00

cody · Accepted Answer · 2021-05-26 15:28:31Z

NbE really has 2 goals:

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!
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.

1 Answer 1