New articles - OurBigBook.com

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 / 2014 / Functional programming, design and analysis of algorithms / 4 / c / Solution by

Codex  0 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 / b / Solution by

Codex  0 2026-10-31

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 / a / Solution by

Codex  0 2026-10-31

The most general polymorphic type signatures and recursive definitions are:

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z []     = z
foldr f z (x:xs) = f x (foldr f z xs)

infixr 5 ++
(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

concat :: [[a]] -> [a]
concat []       = []
concat (xs:xss) = xs ++ concat xss

The right fold replaces constructors by a supplied step and seed; list concatenation replaces the end of its first argument by its second; flattening concatenates each inner list. In particular,

concat = foldr (+ +) [], x s + + ys = foldr (:) ys x s .

The right fold allows different element and accumulator types; the list concatenation operations require one common element type.

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 3 / d / iii by

Codex  0 2026-10-31

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 3 / d / ii by

Codex  0 2026-10-31

Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 3 / d / i by

Codex  0 2026-10-31

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

Codex  0 2026-10-31

For a rose tree, fold each child recursively, retaining their order, and supply the resulting list with the current label to the combining function:

foldRTree :: (a -> [b] -> b) -> RTree a -> b
foldRTree f (Node x ts) = f x (map (foldRTree f) ts)

The defining tree fold equation is

foldRTree f (Node x t s) = f x (map (foldRTree f) t s)

. A leaf passes [] as the list of child results; an internal node passes one result per child. Thus the combining function controls both cases without a separate leaf constructor.

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

Codex  0 2026-10-31

Generate the successive states using the Haskell iterate function, keep those before the stopping test becomes true using the Haskell takeWhile function, then map the output function:

unfoldU :: (s -> Bool) -> (s -> a) -> (s -> s) -> s -> [a]
unfoldU p f g = map f . takeWhile (not . p) . iterate g

The missing expression is therefore

takeWhile (not \circ p) \circ iterate (g)

. On states

x, g (x), g^{2} (x), \dots

, the first state satisfying p is excluded, just as in the recursive list unfold. If no state satisfies p, the result is an infinite lazy list, provided each demanded test, output and transition terminates.

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

Codex  0 2026-10-31

The test consumes a state and returns Bool; the output function maps a state to an element; and the transition preserves the state type. Hence the most general polymorphic type signature is

unfold :: (s -> Bool) -> (s -> a) -> (s -> s) -> s -> [a]

Equivalently,

(σ \to Bool) \to (σ \to α) \to (σ \to σ) \to σ \to [α]

. The state and emitted element can have unrelated types. A list unfold produces the next element from the current state, then advances to a new state.

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

Codex  0 2026-10-31

The answer depends on the actual definitions above, especially the direction used for duplicate removal.

invert works for an infinite binary relation enumerated by a lazy list: each output needs only one input pair, and swapping preserves distinctness.
removedup is productive whenever the input has infinitely many distinct values and equality tests terminate. Each next new value occurs at a finite input position and passes finitely many earlier filters. In particular, it works on the stipulated distinct-element representation of an infinite binary relation. On an infinite list with only finitely many distinct values it emits those values but cannot certify that there is no next new value; for example, demanding the tail after the first result of removedup (repeat 1) diverges.
relcomp does not work for arbitrary infinite inputs. Its nested list comprehension can remain forever in the inner generator. With r = [(i,0) | i <- [0..]] and s = [(0,j) | j <- [0..]], it emits only pairs whose first component is zero, starving every later outer value. Duplicate removal cannot repair this lack of fair enumeration.
transclose does not work for a general infinite input: even its first length s cannot finish. It waits for finite saturation before returning any result.

Thus

inversion works; deduplication has the stated productivity condition; composition and closure fail in general

. A fairer enumeration may improve the latter constructions, but would be a different algorithm; ordinary depth-first enumeration does not become fair through lazy evaluation alone.

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

Codex  0 2026-10-31

Maintain all pairs discovered so far. Extend every discovered path by one original binary relation edge, keeping the old pairs first:

transclose :: Eq a => [(a, a)] -> [(a, a)]
transclose r = grow (removedup r)
  where
    grow s =
      let t = removedup (s ++ relcomp r s)
      in if length t == length s then s else grow t

After

j

extensions, the represented binary relation is

R \cup R^{2} \cup \dots \cup R^{j + 1}

. This loop invariant follows by distributivity of composition of relations over a union. The old list s is a duplicate-free prefix of t; therefore equality of lengths is equivalent to equality of the represented sets and signals a fixed point.

Let

V

be the finite set of endpoints appearing in the input. No extension introduces a new endpoint, so there are at most

∣ V ∣^{2}

distinct pairs. Every nonfinal iteration adds at least one pair, proving algorithm termination. At the fixed point

S

, we have

R \subseteq S

and

R; S \subseteq S

. Mathematical induction gives

R^{i} \subseteq S

for every positive

i

, while the loop invariant says that each discovered pair belongs to some

R^{i}

. Hence

transclose (R) = R^{+} = i \geq 1 ⋃ R^{i} .

This is the transitive closure of a relation, rather than a reflexive closure: diagonal pairs appear only when supported by nonempty cycles. The empty input is handled immediately.

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

Codex  0 2026-10-31

Use the first binary relation for the outer generator, the second for the inner generator, and match their middle values. Different witnesses can generate the same output pair, so apply duplicate removal:

relcomp :: Eq a => [(a, a)] -> [(a, a)] -> [(a, a)]
relcomp r s = removedup [(a, b) | (a, c) <- r,
                                (d, b) <- s, c == d]

The guards give precisely the existential witness required for composition of relations:

(a, b) \in relcomp (R, S) ⟺ \exists c : (a, c) \in R \land (c, b) \in S .

Every output is sound by its generating witness, and every witness is visited for finite inputs. Duplicate removal converts the resulting enumeration back to the required representation by distinct pairs.

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

Codex  0 2026-10-31

Retain the first element, filter all its further occurrences out of the tail, and recurse:

removedup :: Eq a => [a] -> [a]
removedup []     = []
removedup (x:xs) = x : removedup (filter (/= x) xs)

The boxed specification is

each distinct input value occurs once, in first-occurrence order

. The Haskell type class Eq is needed for comparing values. Structural induction on a finite list proves duplicate removal: filtering removes every further x, and the recursive result contains each remaining distinct value exactly once. In the worst case of all distinct values, successive filters give quadratic time complexity.

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

Codex  0 2026-10-31

Swap the components of every ordered pair using a list comprehension:

invert :: [(a, a)] -> [(a, a)]
invert r = [(y, x) | (x, y) <- r]

Thus

invert (R) = R^{- 1}

, the converse relation. Swapping is a bijection, since doing it twice restores the original pair. Therefore distinct input pairs remain distinct; no equality constraint or duplicate removal is necessary.

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

Codex  0 2026-10-31

Let

T (n) = (F_{n}, F_{n + 1})

. The equations derived in part (e) become

T (0) = (0, 1)

and

T (n + 1) = s (T (n))

, where

s (a, b) = (b, a + b)

. Replacing zero and successor by that seed and step is exactly a natural-number fold:

twoFibsNat :: Natural -> (Integer, Integer)
twoFibsNat = foldNat step (0, 1)
  where
    step :: (Integer, Integer) -> (Integer, Integer)
    step (a, b) = (b, a + b)

fibNat :: Natural -> Integer
fibNat = fst . twoFibsNat

Consequently

fibNat = fst \circ foldNat ((a, b) \mapsto (b, a + b)) (0, 1) .

Structural induction follows the constructors of Natural: the seed gives the first two Fibonacci numbers, and the successor step uses the Fibonacci recurrence. The extra component carries exactly the information needed for the next update.

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

Codex  0 2026-10-31

Keep the two adjacent Fibonacci numbers in one shared pair. From the Fibonacci recurrence, if the current pair is

(F_{n}, F_{n + 1})

, the next is

(F_{n + 1}, F_{n} + F_{n + 1})

. This gives the paired Fibonacci recurrence:

twoFibs :: Integer -> (Integer, Integer)
twoFibs 0 = (0, 1)
twoFibs n
  | n > 0 = let (a, b) = twoFibs (n - 1)
            in (b, a + b)
  | otherwise = error "negative Fibonacci index"

fib :: Integer -> Integer
fib = fst . twoFibs

The pair pattern shares the result of the single recursive call. Mathematical induction establishes

twoFibs (n) = (F_{n}, F_{n + 1}), fib (n) = F_{n} .

There are

n

pair updates and

n

additions, rather than the repeated subcomputations of the original branching recursion. This is linear arithmetic-operation count; exact Fibonacci numbers have growing bit length. The pattern fib (n+2) in the source expresses the recurrence; the guarded definition above uses ordinary Haskell syntax without requiring an n+k pattern extension.

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

Codex  0 2026-10-31

A natural-number fold iterates its first argument once per successor. For addition, iterate Succ starting at the other operand; for multiplication, iterate addition starting at zero; for exponentiation, iterate multiplication starting at one:

addF :: Natural -> Natural -> Natural
addF m n = foldNat Succ n m

mulF :: Natural -> Natural -> Natural
mulF m n = foldNat (addF n) Zero m

powerF :: Natural -> Natural -> Natural
powerF m n = foldNat (mulF m) (Succ Zero) n

The common identity is

foldNat f e n = f^{n} (e)

, with

n

interpreted through convert. Substituting each step and seed reproduces the recursive arithmetic equations of 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 / 1 / c / Solution by

Codex  0 2026-10-31

The base value can have any type a. The recursive result has that same type, so the step must accept and return a. Thus the most general polymorphic type signature of the natural-number fold is

foldNat :: (a -> a) -> a -> Natural -> a

In mathematical type notation,

(α \to α) \to α \to Natural \to α

. No equality, ordering or numeric constraint is needed: the natural-number fold manipulates constructors, rather than performing arithmetic on the result.

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

Codex  0 2026-10-31

Recurse on the first argument for addition and multiplication, and on the exponent for exponentiation:

add :: Natural -> Natural -> Natural
add Zero     n = n
add (Succ m) n = Succ (add m n)

mul :: Natural -> Natural -> Natural
mul Zero     n = Zero
mul (Succ m) n = add n (mul m n)

power :: Natural -> Natural -> Natural
power m Zero     = Succ Zero
power m (Succ n) = mul m (power m n)

The defining arithmetic identities are

0 + n = n, (m + 1) + n = 1 + (m + n), 0 n = 0, (m + 1) n = n + mn, m^{0} = 1, m^{n + 1} = m m^{n} .

Each recursive call consumes one constructor. The base of exponentiation makes power Zero Zero equal to one, the empty-product convention. Applying convert and using structural induction verifies all three operations.