Section. Normalisation by evaluation with de Bruijn levels [nbe-nf5]

Let's continue our optimisation journey. The NbE normaliser nf3 (and nf4) still has one shifting operation: when reifying a closure we had:

reify2 (Closure2 b sub) = Abs (reify2
  (wnf2 b (Spine2 0 [] : shift0List 1 sub)))

The shifting operation is not cheap: it needs to traverse the whole substitution to increment all de Bruijn indices by 1. How can we make this faster? Lazy tagging! Well lazy tagging will do the job (and we will do it later), but there is in fact an extremely simple trick that would work here too.

At the moment, variables are represented as de Bruijn indices, and to bring a de Bruijn index v from a context of n variables to a context of n+1 variables, we need to shift v to v+1 (an O(1) operation). Can we find another representation of variables so that shifting a variable from a context of n variables to a context of n+1 variables is is even better than O(1)? The answer is yes! We represent a variable by an integer just like de Bruijn indices, but count from outside in rather than inside out. For example, in the context of b in the following term (assuming b has no free variables other than x, y, z):

\x. \y. \z. b

We will represent x as 0, y as 1, and z as 2. In comparison, de Bruijn indices would represent z as 0, y as 1, and x as 2. In this way, if b is a lambda abstraction, b = \w. c, in the context of c, the variables x, y, and z would still be 0, 1, and 2. Shifting variables into the next level is O(0) (i.e. a no-op)! This kind of variable representation is sometimes called de Bruijn levels.

Using this idea, we can optimise nf3 by using de Bruijn levels (instead of de Bruijn indices) in our semantic domain. The input terms can still use de Bruijn indices as before, and we don't need to transform them into de Bruijn levels. Note that this optimisation is only possible because in the process of weak normalisation (wnf2, wnf3, and wnf4), we always (weakly) normalise a function body when it receives its concrete argument. Therefore all variables are instantiated from outside to inside.

For this optimisation, we don't need to change wnf3, as integer representations of variables are only dealt in the reify and reflect functions. We change reify2 :: Val2 -> Tm to the following:

reify5 :: Int -> Val2 -> Tm
reify5 lvl (Closure2 b sub) = Abs (reify5 (lvl + 1) (wnf3 b (Spine2 lvl [] : sub)))

Here when we reify a function body, we (lazily) substitute the current de Bruijn level lvl for the newly bound variable, instead of the de Bruijn index 0 as we did previously in reify2. This necessitates us to know the current level of the input value, so reify5 now has an additional Int argument lvl. Because of this representation, we do no need to do shift0List 1 to sub anymore.

Conversely, when we reify a spine back to a normal form, the output has type Tm, which still use de Bruijn indices. Hence we need to convert a de Bruijn level v back to a de Bruijn index lvl - v - 1:

reify5 lvl (Spine2 v as) = foldr (\a s -> s `App` reify5 lvl a) (Var (lvl - v - 1)) as

Similarly, the reflect function should be refactored to use de Bruijn levels as well. Therefore we change reflect2 n = map (\v -> Spine2 v []) [0 .. n] to

reflect5 :: Int -> Subst2
reflect5 n = map (\v -> Spine2 (n - v) []) [0 .. n]

We don't need to change wnf3 at all. Therefore our new normaliser is

nf5 :: Tm -> Tm
nf5 t = let n = fv t
        in reify5 (n+1) (wnf3 t (reflect5 n))

-- >>> nf5 c2
-- \x0. \x1. x0 (x0 x1)

-- >>> nf5 (cmul `App` c2 `App` (cinc `App` c2))
-- \x0. \x1. x0 (x0 (x0 (x0 (x0 (x0 x1)))))

-- >>> nf5 ((cmul `App` c2 `App` (cinc `App` c2)) `App` Var 0 `App` Var 1)
-- x1 (x1 (x1 (x1 (x1 (x1 x0)))))

The normaliser nf5 is exactly the version of NbE that you would find in András Kovács's elaboration zoo (which by the way is probably the best online resource for anyone who wants to learn practical implementations of type theories). This is an efficient normaliser of untyped lambda calculus and we have reconstructed it by a series of optimisations from the naive applicative-order normaliser.