Section. Functional normalisation by evaluation [nbe-nf4]

I have been saying that wnf3 t evaluates a term into a semantic domain. However, if we are pedantic with terminology, we should only use the word the word 'evaluate' if wnf3 is computed compositionally (i.e. wnf3 should be a fold of terms). Unfortunately, wnf3 is not (at least, not on the nose) compositional because of this line:

       Closure2 b sub' -> wnf3 b (a' : sub')

where we do recursion on b but b isn't a subterm of the input App f a. However, if we look more closely at wnf3, we see that the stem of problem is that when wnf3 sees a lambda abstraction, we simply stored the function body b and the lazy substitution sub as Closure2 b sub without doing structural recursion into the subterm b. Later, when wnf3 uses Closure2 b sub, it is used as a structural recursion wnf3 b (a' : sub') into the function body b (with an extended substitution). Therefore the computation of wnf3 is in fact compositional -- we just need to refactor wnf3 a bit to make wnf3 (Abs b) sub a function \a. wnf3 b (a : sub) of type Val2 -> Val2 that performs structural recursion into the subterm b. Correspondingly, in places where we previously do Closure2 b sub' -> wnf3 b (a' : sub'), we now no longer need to do the recursion wnf3 b here, as this job has been done by wnf3 (Abs b) sub now.

Turning Closure2 Tm Subst2 into a genuine function Val2 -> Val2 is the key idea, but there is one more small change that we also need to do too. Another place that Closure2 is involved is when it is reified

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

where the free variables in the original substitution sub is shifted by 1. After refactoring Closure2 b sub into a function Val2 -> Val2, we no longer have direct access to sub to do shift0List 1 sub. But this problem is easy to fix: we can just make the function Val2 -> Val2 to take an additional integer argument and apply it to sub.

Now let's execute this refactoring. First of all, we need to change the constructor Closure2 Tm Subst2 from storing a function body and a lazy substitution to a genuine function:

data Val4 = Closure4 (Int -> Val4 -> Val4) | Spine4 Int (LazyList Val4)
type Subst4 = LazyList Val4

wnf4 :: Tm -> Subst4 -> Val4
wnf4 (Var n) sub = sub !! n

And when wnf4 sees a lambda abstraction, it defines a function that structurally recurs into b:

wnf4 (Abs b) sub = Closure4 (\i (~a) -> wnf4 b (a : shift0List4 i sub))

Correspondingly, in the case of App f a, we just need to call the function in the place where we previously had Closure2 b sub' -> wnf3 b (a' : sub'):

wnf4 (App f a) sub =
  let f' = wnf4 f sub
      ~a' = wnf4 a sub
  in case f' of
       Closure4 b -> b 0 a'
       Spine4 v as -> Spine4 v (a' : as)

And in reification, where we previously did

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

now we just need to do:

reify4 :: Val4 -> Tm
reify4 (Closure4 b) = Abs $ reify4 (b 1 (Spine4 0 []))
reify4 (Spine4 v as) = foldr (\a r -> r `App` reify4 a) (Var v) as

Shifting on closures needs some slight refactoring as well:

shift0Val4 :: Int -> Val4 -> Val4
shift0Val4 0 v = v
shift0Val4 i (Spine4 n as) = Spine4 (n + i) (shift0List4 i as)
shift0Val4 i (Closure4 b) = Closure4 (b . (+i))

shift0List4 :: Int -> Subst4 -> Subst4
shift0List4 0 vs = vs
shift0List4 i vs = map (shift0Val4 i) vs

Reflection however stays the same:

reflect4 :: Int -> Subst4
reflect4 n = map (\v -> Spine4 v []) [0 .. n]

And our new normaliser is again:

nf4 :: Tm -> Tm
nf4 t = let n = fv t
        in reify4 (wnf4 t (reflect4 n))

Just to check again that 3 times 3 is still 9:

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

After performing this refactoring, wnf4 becomes compositional -- it is a fold on the syntax of lambda terms. I'd like to emphasise that we have wnf4 only for making the hidden compositional nature wnf3 explicit. In terms of performance, wnf4 makes no improvement over wnf3. They do normalisation in exactly the same way. In fact, we prefer wnf3 in practice because it doesn't need the host language to support higher-order functions, while wnf4 does. Therefore we can easily port wnf3 to languages such as C. In the literature, the way that wnf3 deals with lambda abstractions is called defunctionalization: it implements (higher-order) functions as first-order data (a syntax tree paired with the lazy substitution).

The normaliser nf4 is a milestone of this article: it is essentially what you would get if you extract the algorithmic content of a categorical-glueing normalisation proof for typed calculi and erase all the type information. The functions shift0Val4 and shift0List4 correspond to the presheaf actions in the normalisation proof, and the integer arguments of those shifting functions correspond to the weakening substitutions in the proof.

The only major difference between nf4 and the algorithmic content of a normalisation proof is that nf4 only computes beta-normal forms while normalisation proofs of typed calculi typically also do normalisation of eta-equalities for (dependent) functions and pairs. However, this is not because we did anything wrong -- this is just because normalising eta-equalities is type directed while here we are in the setting of an untyped language, which doesn't give us any information telling us which variables should be eta-expanded (this is the reason why our reflection functions look so trivial).