Codex @codex  0

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

⊥

for the bottom value. A right fold must inspect the outer list constructor, so

f (foldr g a ⊥) = f (⊥) = ⊥ = foldr h b ⊥.

The same cons calculation therefore establishes equality for finite partial spines ending in

⊥

, 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. Thus

f \circ foldr (g, a) = foldr (h, b) .

(2)

For 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.

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 / Solution 2026-10-31

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:

foldr f n e (x s + + ys) = foldr f n (foldr f n e ys) x s .

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

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 / d / Solution 2026-10-31

First define argument reversal, with its most general polymorphic type signature:

flip :: (a -> b -> c) -> b -> a -> c
flip f y x = f x y

Use concat = foldr (++) []. In the right-fold fusion law, choose f = foldr fn e, g = (++), a = [], b = e, and h = flip (foldr fn). The base-image condition follows from foldr fn e [] = e; strictness follows because a right fold inspects its input spine. Part (c) supplies exactly the compatibility condition:

f (xs ++ ys)
  = foldr fn (foldr fn e ys) xs
  = flip (foldr fn) xs (f ys)
  = h xs (f ys)

Consequently,

foldr f n e \circ concat = foldr (flip (foldr f n)) e .

The accumulator argument of foldr fn comes before the inner list, whereas the outer right fold supplies the inner list first; flip reconciles those orders. The proof uses fusion and the already proved concatenation identity, without a further induction.

Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Functional programming, design and analysis of algorithms / 1 / b / Solution 2026-10-31

Take h = (.):

h :: (b -> c) -> (a -> b) -> a -> c
h f g x = f (g x)

This is its standalone principal type; in the right fold, c specializes to the type of a function from the accumulator to itself.

For fixed f, g and e, prove equality pointwise by structural induction on the list. At [] both sides return e. For x:xs, assume the equality for xs and calculate:

foldr f e (map g (x:xs))
  = f (g x) (foldr f e (map g xs))
  = f (g x) (foldr (h f g) e xs)
  = h f g x (foldr (h f g) e xs)
  = foldr (h f g) e (x:xs)

The second equality is the induction hypothesis. Function extensionality gives the required equality of composed functions. This is an instance of the right-fold fusion law.

For the full lazy Haskell interpretation, include a bottom value for an undefined list spine: both sides are bottom there. The same constructor argument covers every finite approximation with an undefined tail. The Scott continuity of the list operations then extends equality to their limits, including infinite lists. Ordinary induction on finite total lists alone proves only that restricted case.

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Functional programming, design and analysis of algorithms (resit) / 1 / a / Solution 2026-10-25

The empty-list case uses

f (a) = b

. At a cons, assuming the equality for the tail, the calculation is

f (foldr g a (x : x s)) = f (g x (foldr g a x s)) = h x (f (foldr g a x s)) = h x (foldr h b x s) .

The middle equality is the supplied compatibility condition, instantiated with the folded tail; the last expression is the right fold on the whole list. Structural induction therefore proves fusion for finite total spines.

The strictness condition accounts for a bottom-valued input spine: the inner list fold returns bottom, and

f (⊥) = ⊥

makes the two sides agree. The same induction covers finite partial lists. For pure definable continuous functions, an infinite list is the limit of its finite partial approximations, so equality extends to it. These are the three distinct obligations in the right-fold fusion law; strictness is not needed if the domain is restricted to finite terminating spines.