Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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.
When I asked this question of some people with experience implementing proof assistants, their answer was "eta-laws".
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.
To be sure, I believe this answer depends on a somewhat broader meaning of "normalization by evaluation" than is sometimes used. For instance, this property doesn't depend on the representation of values of function-type as actual metalanguage functions; it's sufficient to defunctionalize them and we can still call that "normalization by evaluation" for this purpose.
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".
