# Exercise 3.40
(a) NTS: For associative f,
foldL f e (lzw f (Cons x xs) ys) = f x (foldL f e (lzw f ys xs))
The proof is by induction on list ys and non-empty list xs.
Our assumption is that
f (f x y) z = f x (f y z)
for all x, y, z.
Case arbitrary xs, ys = Nil:
foldL f e (lzw f (Cons x xs) Nil)
= { lzw.2 }
foldL f e (Cons x xs)
= { foldL.2 }
f x (foldL f e xs)
= { lzw.1 }
f x (foldL f e (lzw f Nil xs))
which establishes the case.
Case (Cons x (Cons x' xs)), (Cons y ys). We assume that:
foldL f e (lzw f (Cons x' xs) ys) = f x' (foldL f e (lzw f ys xs))
and reason as follows:
foldL f e (lzw f (Cons x (Cons x' xs)) (Cons y ys))
= { lzw.3 }
foldL f e (Cons (f x y) (lzw f (Cons x' xs) ys))
= { foldL.2 }
f (f x y) (foldL f e (lzw f (Cons x' xs) ys))
= { hypothesis }
f (f x y) (f x' (foldL f e (lzw f ys xs)))
= { associativity of f }
f x (f y (f x' (foldL f e (lzw f ys xs))))
= { associativity of f }
f x (f (f y x') (foldL f e (lzw f ys xs)))
= { foldL.2 }
f x (foldL f e (Cons (f y x') (lzw f ys xs)))
= { lzw.3 }
f x (foldL f e (lzw f (Cons y ys) (Cons x' xs)))
which establishes the case. ∎
(b) Derive
bff = unfoldL nil first rest
where
first (Cons t ts) = root t
rest (Cons t ts) = appendL ts (kids t)
as "a simple consequence of the universal property of unfoldL".
We have
bff = concatL ∘ levelf
By the universal property,
bff = unfoldL p f g
iff
bff xs = if p xs then Nil else Cons (f xs) (bff (g xs))
We know that bff xs = Nil iff xs = Nil, so the solution
p = nil
is immediate. We know consider the case nil (Cons x xs) = False:
bff (Cons x xs) = if nil (Cons x xs)
then Nil
else Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { nil (Cons x xs) = False, ITE }
bff (Cons x xs) = Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { bff.1, levelf.1 (unfold version) }
concatL (unfoldL nil (mapL root) (concatL ∘ mapL kids) (Cons x xs)) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { unfoldL.1, nil (Cons x xs) = False, ITE }
concatL (Cons (mapL root (Cons x xs))
(unfoldL (mapL root) (concatL ∘ mapL kids)
(concatL (mapL kids (Cons x xs))))) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { levelf.1 (?) }
concatL (Cons (mapL root (Cons x xs))
(bff (concatL (mapL kids (Cons x xs))))) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { concatL.1, mapL.2 }
appendL (Cons (root x) (mapL root xs))
(concatL (bff (concatL (mapL kids (Cons x xs))))) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { appendL.2 }
Cons (root x)
(appendL (mapL root xs)
(concatL (bff (concatL (mapL kids (Cons x xs)))))) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
≡ { define: first (Cons x xs) = root x }
Cons (first (Cons x xs))
(appendL (mapL root xs)
(concatL (bff (concatL (mapL kids (Cons x xs)))))) =
Cons (f (Cons x xs)) (bff (g (Cons x xs)))
We’ve derived a solution for f. Now we try to disentangle the knot
around g.
Maybe this is simpler?
We need solutions for f and g in the equation:
bff (Cons t ts) = Cons (f (Cons t ts)) (bff (g (Cons t ts)))
We reason:
concatL (levelf (Cons t ts)) = Cons (f (Cons t ts)) (bff (g (Cons t ts)))
≡ { levelf.1, foldF.1 }
concatL (k (mapL (foldR h k) (Cons t ts))) =
Cons (f (Cons t ts)) (bff (g (Cons t ts)))
where
h x xss = Cons (wrap x) xss
k = foldL (lzw appendL) Nil
≡ { mapL.2, k def. }
concatL (foldL (lzw appendL) Nil (Cons (foldR h k t) (mapL (foldR h k) ts))
= Cons (f (Cons t ts)) (bff (g (Cons t ts)))
where
h x xss = Cons (wrap x) xss
k = foldL (lzw appendL) Nil
≡ { foldL.2 }
concatL (lzw appendL (foldR h k t)
(foldL (lzw appendL) Nil (mapL (foldR h k) ts)))
= Cons (f (Cons t ts)) (bff (g (Cons t ts)))
where
h x xss = Cons (wrap x) xss
k = foldL (lzw appendL) Nil