Section. Reflection on NbE [nbe-reflection]

Now let's a good time to reflect on what we have done from the very beginning:

1. We made the normalisation of arguments lazy.

   Our rationale for this is that if the argument doesn't get used in the function body at all, we don't waste any time on normalising the argument.

2. We switched our evaluation strategy from applicative order to what may be called weak applicative order.

   This strategy can be summarised as no beta-reductions are allowed under the scope of a lambda abstraction, unless the lambda abstraction has no arguments, or alternatively, normalising a term to a weak normal form first before normalising under lambda abstractions.

   Our rationale for this is that if we delay normalising a function body b until the bound variable x receives its concrete value a, we can skip normalisation of arguments M that are supplied to x but are actually not used by a when x becomes a.

3. We used the trick of lazy tagging to implement substitutions to make substitutions fast.

4. We optimised out shifting de Bruijn indices by some algebraic simplification and using de Bruijn levels in weak normal forms.

Therefore, now we may say we understand normalisation by evaluation better!

Normalisation by evaluation is just weak-applicative-order normalisation with meta-level laziness, lazy substitution, and de Bruijn levels.

In fact, the version of NbE that we extract from glueing proofs is just weak-applicative-order normalisation with lazy substitution.