# What are the advantages of normalization by evaluation over traditional reduction-based normalization?

I think in NBE, you get rid of certain substitutions, and it solves the problem of binding representation (so you don't have to use indices or capture-avoiding substitution or something). But I believe there are other differences I'm not aware of.

In particular, I'm interested in elaboration of dependently typed lambda calculus, where nbe can be used to calculate the normal forms of core terms.

• Isn't NbE a general technique, not just for lambda calculi? Notably it enables proofs by reflection in arbitrary theories okmij.org/ftp/tagless-final/NBE.html Nevertheless even in the context of lambda, the question seems well-formed to me. There are at least two ways of reducing lambda terms, by NbE, or by a conventional rewrite system, so one might wonder how they compare. Commented Feb 9, 2022 at 15:40
• @GuyCoder clarified. I appreciate the criticism (I don't know nbe is a general technique)
– ice1000
Commented Feb 9, 2022 at 16:15

If you test equality using only some kind of reduction algorithm, then generally speaking your equality will only incorporate beta-reductions such as $$(\lambda x. M)(N) \equiv M[N/x]$$. Eta-equivalences such as $$M \equiv (\lambda x. M x)$$ are quite difficult to implement with a reduction-only algorithm. There are various reasons for this, such as the fact that if you want to reduce $$\lambda x. M x$$ to $$M$$ you need to check that $$x$$ doesn't occur in $$M$$, and if you want to expand $$M$$ to $$\lambda x. M x$$ you need to have type information present to know that $$M$$ has a function-type. I won't say it's impossible, but normalization-by-evaluation is a clean, generalizable, and easy-to-reason-about family of algorithms that perform both $$\beta$$-reduction and $$\eta$$-expansion in a type-directed way.
In addition, one doesn't have to check $$\beta\eta$$-equality by first normalizing to a $$\beta\eta$$-normal form and then doing an $$\alpha$$-equivalence check: one can incorporate the two $$\beta$$ and $$\eta$$ stages directly into a "bidirectional" equality-checking algorithm. But for purposes of this answer (which is, again, not one that I invented, but was given by those in the know) we also consider that to be a form of "normalization by evaluation".