18
$\begingroup$

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.

$\endgroup$
2
  • 5
    $\begingroup$ 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. $\endgroup$
    – Li-yao Xia
    Feb 9, 2022 at 15:40
  • $\begingroup$ @GuyCoder clarified. I appreciate the criticism (I don't know nbe is a general technique) $\endgroup$
    – ice1000
    Feb 9, 2022 at 16:15

1 Answer 1

11
$\begingroup$

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

$\endgroup$
1
  • 1
    $\begingroup$ Another tidbit: eta reduction is liable to ruin confluence. Some terms can be either β or η reduced, and the result of each choice won't lead to a common reduct. This means it can't be used for equality testing unless you can ensure you always make the same choices. But, this seems infeasible, because you might be making the decision before some other reduction/substitution reveals that this sort of β-η conflict was in play. $\endgroup$
    – Dan Doel
    Feb 12, 2022 at 19:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.