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
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
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))))))))