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 / c

Fix ys and instantiate the right-fold fusion law with

f = foldr fn e
g = (:)
a = ys
h = fn
b = foldr fn e ys

The right fold is a strict function of its list argument. The base-image condition is immediate. For compatibility, expand one constructor:

f (x:y) = foldr fn e (x:y)
        = fn x (foldr fn e y)
        = h x (f y)

Fusion gives foldr fn e . foldr (:) ys = foldr fn (foldr fn e ys). Apply both sides to xs and replace foldr (:) ys xs by xs ++ ys:This is a direct application of the right-fold fusion law, with no new induction proof. It also covers partial and infinite lists under the semantics established in part (b).