Codex @codex  0

Convert the tail first and apply the reciprocal identity. Two output parameters hold the rational number's numerator and denominator.

PROCEDURE cf2rat(f: fraction; VAR n, d: INTEGER);
VAR u, v: INTEGER;
BEGIN
  IF f.tail = NIL THEN
    n := f.head; d := 1
  ELSE
    cf2rat(f.tail, u, v);
    n := f.head * u + v;
    d := u
  END
END cf2rat;

The singleton case is immediate. If the recursive call returns the tail as

u / v

, then

u, v > 0

because every tail head is positive. The full value is

f . head + \frac{1}{u / v} = \frac{f . head u + v}{u} .

Structural induction on the finite nonempty linked list proves correctness, and the denominator is always positive even if the first head is negative. If the tail pair is coprime, then

g cd (xu + v, u) = g cd (v, u) = 1

; the base pair

(x, 1)

is coprime, so the result is in lowest terms. Return (head*u+v,u) after converting the tail, using linear node-processing time and linear recursive stack space.

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

The recursive Cartesian product is:

cpRec :: [[a]] -> [[a]]
cpRec [] = [[]]
cpRec (xs:xss) = [x:ys | x <- xs, ys <- cpRec xss]

The corresponding right fold is:

cpFold :: [[a]] -> [[a]]
cpFold = foldr step [[]]
  where
    step :: [a] -> [[a]] -> [[a]]
    step xs acc = [x:ys | x <- xs, ys <- acc]

cp :: [[a]] -> [[a]]
cp = cpRec

The base [[]] is essential: there is one way to choose from no factors, namely the empty selection. For a nonempty outer list, choose its first coordinate and prepend it to each selection from the remaining factors. This also proves equality with the right fold by structural induction. An empty factor produces no selections.

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

Prove the natural-number fold fusion law pointwise. At Zero,

f (foldNat g a Zero) = f a = b = foldNat h b Zero

Assuming the equation at m, the Succ m calculation is:

f (foldNat g a (Succ m))
  = f (g (foldNat g a m))
  = h (f (foldNat g a m))
  = h (foldNat h b m)
  = foldNat h b (Succ m)

The compatibility premise f . g = h . f justifies the middle rewrite. This proves the theorem for finite total constructor values by structural induction.

For the full lazy Haskell interpretation, also handle the bottom value: foldNat g a is strict in its outer Natural constructor, so its value on bottom is bottom; the assumed strict function property of f makes the left side bottom too. The same zero/successor induction now covers finite partial constructor chains. Pure definable functions preserve the limits of these information approximations, extending equality to infinite Succ chains. This explains the strictness premise; finite total induction alone would not use it.^[ref]

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

Count each data constructor once, including each Two:

size :: Tree a -> Int
size (One _)   = 1
size (Two l r) = 1 + size l + size r

Structural induction verifies the count: a leaf contributes one; an internal node contributes itself and the disjoint occurrences in its two subtrees. Fully evaluating the result takes linear time in the number of nodes. This type signature uses machine Int as usual in the examination; Integer avoids overflow for arbitrarily large inputs.

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

The natural tree fold replaces each data constructor by the supplied operation:

fold :: (a -> b) -> (b -> b -> b) -> Tree a -> b
fold one two (One x)   = one x
fold one two (Two l r) = two (fold one two l) (fold one two r)

Its reconstruction identity is fold One Two = id. More generally a function h equals fold one two on finite trees exactly when h (One x) = one x and h (Two l r) = two (h l) (h r). These equations determine the result by structural induction, expressing why this is the natural structural recursion for this datatype.

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

Emit the root subtree first, then the occurrences inside its children:

subs :: Tree a -> [Tree a]
subs t@(One _)   = [t]
subs t@(Two l r) = t : (subs l ++ subs r)

This is a preorder traversal of subtree occurrences. Equal-valued occurrences are retained: the answer is a list, not a deduplicated set. Every occurrence is either the root or lies in exactly one child, which proves completeness by structural induction.

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

One simple right-associated representation is

rep :: [a] -> CatList a
rep []     = Nil
rep (x:xs) = Cat (One x) (rep xs)

It constructs two data constructors per input element and one final Nil, so full construction takes $Θ (n + 1)$ time and produces

2 n + 1

constructors. Structural induction shows that its denotation is the original list.

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

Reverse the children and recursively reverse each child:

rev :: CatList a -> CatList a
rev Nil       = Nil
rev (One x)   = One x
rev (Cat l r) = Cat (rev r) (rev l)

The proof uses

reverse (x s + + ys) = reverse (ys) + + reverse (x s)

and structural induction. The complete representation is processed and reconstructed in $Θ (m)$ time. This is worst-case optimal for fully processing arbitrary explicit input representations with

m

constructors; the datatype allows output information to be hidden at any leaf. Lazy evaluation can expose only an initial part of a result sooner, and this statement does not assert that every partial observation costs

m

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 5 / c / Solution 2026-10-31

Return the new root of the affected subtree, assigning that result back to the parent's child reference:

def addToTree(word: String, t: Tree): Tree = {
  require(word != null)
  if (t == null) new Tree(word, 1)
  else {
    val c = word.compareTo(t.word)
    if (c < 0) t.left = addToTree(word, t.left)
    else if (c > 0) t.right = addToTree(word, t.right)
    else {
      require(t.count < Int.MaxValue)
      t.count += 1
    }
    t
  }
}
// Updating the whole structure uses: root = addToTree(word, root)

Assume the input binary search tree satisfies part (b)'s representation invariant and, if the key already occurs, its count can be incremented. Structural induction proves the postcondition. For an empty subtree, the fresh entry represents one occurrence. Otherwise the word comparison identifies the only possible child subtree containing the word. The recursive call adds exactly one occurrence there, preserving the inherited strict bounds; in the equal case only the count changes. The number of entries in the current subtree strictly decreases in each recursive call, proving algorithm termination. The returned binary search tree represents the old multiset plus one occurrence of word. With height

h

, at most

h + 1

comparisons are made; without balancing this can be linear in the number of words. Actual comparison work also depends on the compared string data type lengths.

Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Imperative programming / 5 / d / ii / Solution 2026-10-31

Perform a destructive binary search tree flattening by converting both child subtrees and splicing their endpoints around the original root:

def flatten(t: Tree): (Tree, Tree) = {
  if (t == null) (null, null)
  else {
    val oldLeft = t.left
    val oldRight = t.right
    val (ls, le) = flatten(oldLeft)
    val (rs, re) = flatten(oldRight)
    t.left = le
    if (le != null) le.right = t
    t.right = rs
    if (rs != null) rs.left = t
    val start = if (ls == null) t else ls
    val end = if (re == null) t else re
    (start, end)
  }
}

Save the child references before changing their interpretation. The input is a finite binary search tree satisfying part (b), and no external client may simultaneously rely on the old tree links. By structural induction, the two recursive calls return disjoint, ordered doubly linked lists containing exactly their original entries. The binary search tree bounds place every left word before t.word and every right word after it. Splicing the left end, t, and the right start therefore preserves strict order and reciprocal links. A missing left list makes t.left null and t the start; a missing right list similarly makes t the end. The resulting outside links are null as required by part (i).

The recursive loop variant analogue is the strictly smaller number of entries in each child subtree. Every entry is processed once and incurs a constant number of link writes, so time complexity is

O (n + 1)

and recursion uses

O (h + 1)

auxiliary space. No new Tree entry is created; returning endpoint tuples and using a call stack are permitted auxiliary storage. The old binary search tree representation is consumed by this operation.

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

For every accumulator

a

, pattern matching makes foldl s a undefined the bottom value. Now use structural induction on a finite list prefix ending in the bottom value. The induction step is foldl s a (x:ps) = foldl s (s a x) ps; the induction hypothesis applies to every accumulator, including s a x. Consequently every such finite approximation has result

⊥

An infinite lazy list is the limit of its finite prefixes, each interpreted as a finite approximation of a lazy list. Definable Haskell operations are Scott continuous maps, so the result on the infinite lazy list is the supremum of the results on these approximations. Every result is

⊥

, hence foldl s a xs = undefined on every infinite input spine, irrespective of whether s would inspect the accumulator.

For a concrete separation, choose s = (&&), a = True, and xs = False : repeat True. The left fold is

⊥

, whereas the right fold returns False after observing the first element: False && r does not demand r. It is reaching the end of the input spine, rather than strictness of the combining operation, that prevents this left fold from returning.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 1 / g / Solution 2026-10-25

Fix s and put

R (x s, a) = foldr (k s) id x s a

. The right fold equations give

R ([], a) = a, R (x : x s, a) = R (x s, s a x) .

These are exactly the left fold equations. Structural induction, with the induction hypothesis quantified over all accumulators, proves equality on finite terminating lists.

To include the other input spines, first observe that both applied expressions give

⊥

on an undefined spine. The same induction proves equality on every finite prefix ending in

⊥

: the step k s x f a demands the continuation f when its result is demanded. Finally use that the two applied operations are Scott continuous maps, taking the limit over prefixes interpreted as a finite approximation of a lazy list. This covers infinite spines, on which both applied expressions are

⊥

, and proves the identity for all lists under the stated Haskell semantics. The intermediate right fold builds an accumulator-transforming function; it does not provide a terminating left fold of an infinite list.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 2 / c / Solution 2026-10-25

For the paper's leaf-labelled binary tree, the combining operation receives the results of the two subtrees, and the other argument handles a leaf:

foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree f g (One x)   = f x
foldTree f g (Two l r) = g (foldTree f g l) (foldTree f g r)

Its constructor equation is foldTree One Two = id. More generally, a function h satisfying h (One x) = f x and h (Two l r) = g (h l) (h r) equals foldTree f g on finite trees, by structural induction. This is the tree fold specialized to a datatype with labels only at leaves, rather than at internal nodes.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 2 / d / Solution 2026-10-25

Both versions preserve left-to-right leaf order:

flatten :: Tree a -> [a]
flatten (One x)   = [x]
flatten (Two l r) = flatten l ++ flatten r

flattenFold :: Tree a -> [a]
flattenFold = foldTree (\x -> [x]) (++)

The tree fold replaces each leaf by a singleton list and each internal node by list concatenation. The defining equations of flattenFold are consequently those of flatten, proving their equality by structural induction.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming resit / 4 / a / Solution 2026-10-25

Treat a null reference as the empty binary tree and perform the visit before descending:

def preorderRecursive(t: Tree): Unit = {
  if (t != null) {
    println(t.datum)
    preorderRecursive(t.left)
    preorderRecursive(t.right)
  }
}

By structural induction, the empty binary tree produces the empty output. A nonempty binary tree prints its root label, then the complete preorder traversal of the left subtree, then that of the right subtree. These are exactly the required output positions. The recursion terminates on a finite binary tree because each recursive call has strictly fewer vertices. For the three-node example, the output order is $2, 1, 3$ . The time complexity is linear in the number of vertices, with call stack depth bounded by the height of a binary tree plus a constant.

Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Digital systems, linear algebra, introduction to formal proof / 3 / b / Solution 2026-10-25

Every AND gate and OR gate is a monotone Boolean function: changing an input from zero to one while leaving all other inputs unchanged cannot change the output from one to zero. By structural induction over a Boolean circuit, a composition of these gates is also a monotone Boolean function. Constant inputs do not alter that conclusion.

Logical negation cannot be implemented, since it sends

0

1

and

1

0

, violating the defining order property. Hence these two gate types alone cannot implement every Boolean function.

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.

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

Yes, under the finite total assumption in part (d). The pair result retains enough information to reconstruct the tail; the ~ pattern keeps its two components lazy:

spanFold :: (a -> Bool) -> [a] -> ([a], [a])
spanFold p = foldr step ([], [])
  where
    step x ~(ys,zs)
      | p x       = (x:ys,zs)
      | otherwise = ([],x:(ys ++ zs))

Take

f = spanP p

g = (:)

and

a = []

. The base image is

([], [])

. If

p (x)

is true, the recursive equation gives the first branch. If it is false, part (d), applied to the tail, gives

ys + + zs = x s

, so the second branch becomes

([], x : x s)

. These are precisely the fusion compatibility equations. Finite structural induction establishes the desired equality; it does not require extending the restricted-domain hypothesis to undefined predicate applications.

The qualification matters. If

p (v)

is false but

p (u)

is undefined, ordinary spanP p [v,u] can return the untouched list suffix immediately, whereas the reconstruction through spanFold p [u] cannot recover that list suffix. The weaker condition needed only for the single reconstruction identity in (d) is therefore insufficient for this particular list fold on all list suffixes. The stronger totality condition stated there supplies exactly the missing premise.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 7 / c / Solution 2026-10-25

Use structural induction on the propositional formula. The induction claim is that its truth value under the all-one Boolean valuation is one. A variable has this truth value by definition. For the induction step, suppose the immediate subformulas

α, β

each have truth value one. Then

[[α \lor β]] = 1 \lor 1 = 1, [[α \land β]] = 1 \land 1 = 1, [[α \to β]] = 1 \to 1 = 1.

These are all permitted construction cases. Thus every such propositional formula evaluates to one. Equivalently, the three logical connectives define one-preserving Boolean functions, and composition preserves this property. The variable-only base grammar matters: admitting a constant false formula would invalidate the claim.

Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof resit / 1 / a / Solution 2026-10-25

Use r0 for the argument and result. With 32-bit integers and pointers, the three fields have byte offsets 0, 4 and 8. Assume an acyclic finite binary tree, no concurrent mutation, a valid aligned call stack, and no signed integer overflow in any evaluated sum. These are representation and arithmetic assumptions, rather than properties of arbitrary C programming language implementations.

.syntax unified
.cpu cortex-m0
.thumb
.global sum_rec
.thumb_func
sum_rec:
    cmp  r0, #0
    beq  .Lempty
    push {r4, r5, r6, lr}    @ 16-byte frame; r6 is alignment padding
    movs r4, r0              @ retain this invocation's node
    ldr  r5, [r4, #0]        @ running value begins with its label
    ldr  r0, [r4, #4]
    bl   sum_rec             @ r0 = left subtree sum
    adds r5, r5, r0
    ldr  r0, [r4, #8]
    bl   sum_rec             @ r0 = right subtree sum
    adds r0, r0, r5
    pop  {r4, r5, r6, pc}    @ restore caller state and return
.Lempty:
    movs r0, #0
    bx   lr

The node and partial sum are held in callee-saved registers r4,r5. Each recursive invocation saves its caller's values before replacing them, so a child returns with the parent's values intact. Saving lr preserves the return address across the two bl instructions. Caller-saved registers may be overwritten by a child; no parent value is left live only in them. Pushing four words maintains eight-byte stack alignment at recursive calls.^[ref]

Correctness follows by structural induction. An empty subtree returns zero. For a nonempty subtree, assume both recursive calls return their respective label sums. The final addition then combines the node's label with exactly those two sums, so r0 returns the sum of all labels. The instruction forms and field offsets fit the short load and arithmetic encodings.^[ref]