Section. Weak-applicative-order normalisation with lazy substitutions [nbe-nf2]

Coming back to wnf1, we'd like to use lazy tagging to make substitution more efficient. Just like the add example above, when we want to substitute an argument for the binder variable in a function body, we will just lazily remember this substitution at the root of the syntax tree without actually performing the substitution.

Moreover, recall that our wnf1 only normalises a function body when we have a concrete value for the function argument. Consequently, if there are two variables x and y in a term such that y is bound in the scope of x, like in

(\x. ... (\y. ... x ...) N ...) M

the variable x always receives its concrete value (wnf1 M for the term above), before y receives its concrete value (wnf1 N for the term above). Therefore we can simply represent a lazy substitution applied to a term as a list of terms. More precisely, we will lazily store a substitution

((((t [a1/x1]) [a2/x2]) [a3/x3]) ... [aN/xN])

as a pair of the original term t and the list [aN, ..., a3, a2, a1]. Applying a new substitution (for the de Bruijn index 0) is just cons-ing a value to the head of the list.

Notice the correctness of this representation hinges on the fact that we are doing capture-avoiding substitution. When we substitute a value aN for a bound variable xN, we can just cons aN to the list [..., a3, a2, a1] of existing substitutions for the outer bound variables because we know for sure that xN doesn't occur in the arguments [..., a3, a2, a1] from outer layers. For example, consider the term

(\x. ... (\y. ... x ...) N ...) M

We first substitute wnf1 M for x and then later substitute wnf1 N for y, and we know for sure that y doesn't occur in wnf1 M because our substitution is capture avoiding. Therefore the lazy substitution for the inner function body can just be [wnf1 N, wnf1 M], which means that variable of de Bruijn index 0 (i.e. y) has been substituted by wnf1 N, the variable of de Bruijn index 1 (i.e. x) has been substituted by wnf1 M.

Side Remark: In modal type theory, there is a concept called delayed substitution for dealing with type formers that do not commute with substitutions. There is similarity between delayed substitution and our idea here, but the motivation is completely different: there the problem is that some syntactic constructors don't commute with substitution, whereas our syntactic constructors do commute with substitution and we delay substitution for efficiency considerations.

Enough with talking, let's implement our ideas. The first thing that we are going to do is to define the type of weak normal forms with lazy substitutions. Previously, wnf1 has type Tm -> Tm, but now we want to work with lazy substitutions, so the output type can't be Tm anymore (the input term can still be Tm). We need to define a new type for the output of wnf1. The name 'weak normal forms with lazy substitutions' is too verbose, so we will just call them values. A value is either

  1. a lambda function, represented by Closure2 below, which has two fields: the function body and the lazy substitution applied to this function (stored as a lazy list of values); or

  2. a variable applied to a list of arguments, represented by Spine2 above, which also has two fields: the de Bruijn index of the variable and the arguments (also stored as a lazy list of values).

data Val2 = Closure2 Tm Subst2 | Spine2 Int (LazyList Val2)
type Subst2 = LazyList Val2

Here we use lazy lists (which is just the default Haskell list type [a]) rather than strict lists because we want to make normalisation of function arguments lazy, like how we did in wnf1. Strictly speaking we only need the payloads of the list to be lazy and the structure of the list itself can remain strict:

data PayloadLazyList a = Nil | Cons ~a (PayloadLazyList a)

but let's just use LazyList (lazy lists of lazy payloads) because I am too lazy to re-define the standard list functions that we are going to use.

The type of wnf1 :: Tm -> Tm becomes then

wnf2 :: Tm -> Subst2 -> Val2

where the output is a value (i.e. a weak normal form with lazy substitutions) and the input is a term paired with lazy substitutions applied to this term. Whenever wnf2 sees a variable, the variable logically has been replaced by the lazy substitution, so we just look up the substitution:

wnf2 (Var n) sub = sub !! n

When wnf2 sees a lambda abstraction, it is already a weak normal form, so we just store it along with the lazy substitution:

wnf2 (Abs b) sub = Closure2 b sub

The interesting case is again function application App f a. We will do recursion on f and a as before:

wnf2 (App f a) sub =
  let f' = wnf2 f sub
      ~a' = wnf2 a sub
  in case f' of
       Closure2 b sub' -> _what_do_we_do_here
       Spine2 v as -> Spine2 v (a' : as)

but what should we do this time when the function is a lambda abstraction? Previously we did wnf1 (beta b a') where

beta b a = shift 0 (-1) (subst b 0 (shift 0 1 a))

Substituting a' for the variable 0 in b should now be just a' : sub'. However, we now need to shift the de Bruijn indices of the whole substitution by 1 rather than just a, because sub' is a lazy substitution applied to Abs b rather than b. Therefore our new substitution for b should be shift0List 1 (a' : sub') where

shift0Val :: Int -> Val2 -> Val2
shift0Val i (Spine2 n as) = Spine2 (n + i) (shift0List i as)
shift0Val i (Closure2 b sub) = Closure2 b (shift0List i sub)

shift0List :: Int -> Subst2 -> Subst2
shift0List i = map (shift0Val i)

Note that shift0Val doesn't need to shift the indices in the function body b, because these variables logically have already been substituted by sub.

Another difficulty is the shift 0 (-1) in the definition of beta b a. Because now our substitution is lazy, we don't really have the result of substitution to perform this shift 0 (-1) on. However, in wnf1 we really wanted to do is wnf1 (beta b a'), and we can rewrite it a bit:

  wnf1 (beta b a')
= wnf1 (shift 0 (-1) (subst b 0 (shift 0 1 a')))
= shift 0 (-1) (wnf1 (subst b 0 (shift 0 1 a')))

The first equality is just the definition of beta and the second equality is because removing the variable 0 that is substituted away before or after weak normalisation gives the same result. This observation then allows us to translate wnf1 to wnf2:

wnf2 :: Tm -> Subst2 -> Val2
wnf2 (Abs b) sub = Closure2 b sub
wnf2 (Var n) sub = sub !! n
wnf2 (App f a) sub =
  let f' = wnf2 f sub
      ~a' = wnf2 a sub
  in case f' of
       Closure2 b sub' -> shift0Val (-1) (wnf2 b (shift0List 1 (a' : sub')))
       Spine2 v as -> Spine2 v (a' : as)

Reifying values to normal forms works the same as reify1, except that for the case of a lambda abstraction Closure2 t sub, the new substitution for the function body b should now be Spine2 0 [] : shift0List 1 sub, where Spine2 0 [] means that the bound variable 0 of the function body b is still 0 itself, applied to no arguments. And shift0List 1 is applied to sub because sub is a substitution applied to Abs b rather than b.

reify2 :: Val2 -> Tm
reify2 (Closure2 b sub) = Abs (reify2 (wnf2 b (Spine2 0 [] : shift0List 1 sub)))
reify2 (Spine2 v as) = foldr (\a r -> r `App` reify2 a) (Var v) as

Putting things together, we have our new normaliser:

nf2 :: Tm -> Tm
nf2 t = let n = fv t
        in reify2 (wnf2 t (reflect2 n))

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

The function reflect2 creates the trivial substitution for the free variables of the term t, substituting each free variable v for v itself. (Side remark: reflect2 is rather trivial here, but if we do normalisation for typed languages with eta-equalities, this reflect function would be more interesting.)

Let's do some sanity checks again:

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

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

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

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