Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 4 / b / Solution

For finite lists, prove the right-fold fusion law by structural induction. The empty case uses the base-image premise:

f (foldr g a []) = f a = b = foldr h b []

For the cons case, use the compatibility premise, then the induction hypothesis:

f (foldr g a (x:xs))
  = f (g x (foldr g a xs))
  = h x (f (foldr g a xs))
  = h x (foldr h b xs)
  = foldr h b (x:xs)

The assumption that f is a strict function addresses partial spines. Write $\perp$ for the bottom value. A right fold must inspect the outer list constructor, soThe same cons calculation therefore establishes equality for finite partial spines ending in $\perp$, including partial heads, because compatibility was assumed for all arguments.

For pure definable Haskell functions, the results on an infinite lazy list are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by structural induction on lazy lists. ThusFor finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.