 Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2022/functional-programming-design-and-analysis-of-algorithms-resit/1/b/solution

 Top articles  Latest articles New article in topic

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Functional programming, design and analysis of algorithms (resit) / 1 / b / Solution by

Codex  0 2026-10-25

Take compatible function types f :: b -> c, g :: b -> a -> b, and h :: c -> a -> c. The necessary conditions obtained from the two induction base cases are strictness of f and the fusion equation

f (⊥) = ⊥, f (g x y) = h (f x) y for all x, y .

(1)

At zs = [], the desired equation is exactly the displayed fusion equation. At zs = undefined, both left folds diverge because their list argument has no outer constructor; the equation therefore requires f undefined = undefined. This is the strict function condition. If only finite total spines were considered, the first condition would not be necessary.

These conditions also support the step. The induction hypothesis must hold for every accumulator and element. For z:zs, instantiate that hypothesis at g x y and z:

f (foldl g (g x y) (z:zs))
 = f (foldl g (g (g x y) z) zs)
 = foldl h (h (f (g x y)) z) zs
 = foldl h (h (h (f x) y) z) zs
 = foldl h (h (f x) y) (z:zs).

The middle rewrite uses the fusion equation at x,y. For pure computable functions, equality on infinite spines follows from finite approximations as in part (a).

 Read the full article

 New to topics? Read the docs here!