Section. Fixing the inefficiency, a plan [nbe-weak-normalisation-plan]

From the discussion above, we see that the problem with nf0 is that when it sees a function application f a, it may too eagerly normalise f and a. If we want to fix this source of inefficiency, what is the minimum amount of normalisation work that we should do to f and a instead?

1. We must at least normalise f to expose its outermost lambda abstraction, because that's what we need for doing a beta-reduction. We can normalise f more, but exposing its outermost layer is the minimum requirement. In jargon, we must at least normalise f to its weak head normal form (WHNF).

2. We have no constraints on how much normalisation that we do for a. We can leave it totally unnormalised when supplying it to the function, or we can also normalise it to expose the outermost lambda abstraction, or we can fully normalise it as we did in nf0.

For the function f, doing the minimum amount of work (i.e. normalising f to its WHNF) is optimal. To see this, suppose the WHNF of f is \x. M. In the term M, the variable x may be used both as a function and as an argument, so M looks like

... (x M1) ... (M2 x) ...

By substituting (some partially normalised form of) the argument a for x before normalising this function body M, we may be able to avoid normalising M1 if a doesn't use M1. And substituting a in before normalising M doesn't create any additional overhead.

On the other hand, how much we normalise the argument a before supplying it to the function is more interesting:

1. As we said before, full normalisation is not optimal because in the function body a may be unused or it may be used as a function.

2. Completely no normalisation is a bad idea too because the argument of f may occur multiple times in f. Substituting unnormalised a for each of these occurrences leads us to duplicated normalisation work for a.

Our third choice is to normalise the argument a to the same extent as f, since the argument a may be used as a function inside f as well. A precise way to summarise this choice is that we would like to compute weak normal forms (WNFs) of terms (in the process of full normalisation): a term is in weak normal form if it is either

1. a lambda abstraction, or

2. a variable applied to zero or more arguments that are weak normal form themselves.

Moreover, we can (weakly) normalise a lazily, so that if the function body of f doesn't actually use its argument, the work of (weakly) normalising a can be saved. Although we will see later that this strategy is not optimal either, it is pretty decent one, so let's make it our plan for now.