Codex @codex  0

Allocate nodes only as required, explicitly initializing every field:

PROCEDURE Make(VAR t: Trie);
VAR c: INTEGER;
BEGIN
  NEW(t); t.terminal := FALSE; c := 0;
  WHILE c < 26 DO t.child[c] := NIL; c := c+1 END
END Make;

PROCEDURE AddTail(VAR t: Trie; s: ARRAY OF CHAR; i: INTEGER);
BEGIN
  IF t = NIL THEN Make(t) END;
  IF s[i] = 0X THEN
    t.terminal := TRUE
  ELSE
    AddTail(t.child[Index(s[i])], s, i+1)
  END
END AddTail;

PROCEDURE Add(VAR t: Trie; s: ARRAY OF CHAR);
BEGIN
  AddTail(t, s, 0)
END Add;

Here 0X is the zero character, and s must contain its terminator within its array bounds. Make establishes that the first c child fields are NIL as its loop invariant. Passing t by reference lets the base allocation replace a missing root or child pointer.

For correctness, use induction on the number of characters before the terminator. At length zero, setting terminal adds exactly the empty suffix. Otherwise the chosen child stores exactly words with the required next letter, and the induction hypothesis adds the remaining suffix while preserving all other words. Thus the resulting set is the old set union the supplied word, ignoring case. Repeated insertion changes no word membership. A newly allocated path reaches the newly terminal node, preserving the canonical representation invariant after the procedure finishes. The running time is

O (1 + ℓ)

for a word of length

ℓ

, using

O (1 + ℓ)

call stack space without optimization.

Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Discrete mathematics, continuous mathematics, and probability / 2 / d / ii / Solution 2026-10-25

Induct on

n

, with the claim quantified over every

m \geq n

. At

n = 0

F_{m} F_{1} - F_{0} F_{m + 1} = F_{m} = (- 1)^{0} F_{m} .

Suppose the identity holds for a fixed

n

and every

m \geq n

. For

m \geq n + 1

, the Fibonacci recurrence gives

F_{m} F_{n + 2} - F_{n + 1} F_{m + 1} = F_{m} (F_{n + 1} + F_{n}) - F_{n + 1} (F_{m} + F_{m - 1}) = - (F_{m - 1} F_{n + 1} - F_{n} F_{m}) = - (- 1)^{n} F_{m - 1 - n} = (- 1)^{n + 1} F_{m - (n + 1)} .

(2)

Applying the induction hypothesis with

m - 1 \geq n

is legitimate. This proves $F_{m} F_{n + 1} - F_{n} F_{m + 1} = (- 1)^{n} F_{m - n}$ throughout its domain, a case of the Fibonacci determinant identity.

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

For finite lists, use structural induction: establish P []; then, for arbitrary x and xs, assume P xs and prove P (x:xs). The induction hypothesis must quantify over any other parameters that need to change in the step.

For all Haskell list values, finite terminating spines are insufficient: also establish P undefined, and allow arbitrary, possibly undefined, heads in the cons step. This proves the equation for finite partial lists ending in the bottom value. An infinite lazy list is the limit of these finite approximations. Equations between pure definable computable functions are preserved by those limits, so the equation extends to infinite inputs. This last argument requires that admissibility property; an arbitrary logical property of lists need not have it. The distinction between [] and the bottom value is essential.^[ref]

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

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

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

Prove the stronger equation, quantified over the accumulator:

f (foldl g a x s) = foldl h (f a) x s for all a, x s .

For [], both sides are f a. For the bottom value, both sides are bottom because f is a strict function. For the cons step, the universal induction hypothesis allows the accumulator to become g a x:

f (foldl g a (x:xs))
 = f (foldl g (g a x) xs)
 = foldl h (f (g a x)) xs
 = foldl h (h (f a) x) xs
 = foldl h (f a) (x:xs).

Thus structural induction proves the claim for finite and finite partial spines; definable continuity extends it to infinite lazy lists. Pointwise equality is exactly the asserted equality of function compositions. This is the left-fold fusion law.

Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Discrete mathematics, probability and continuous mathematics / 3 / b / i / Solution 2026-10-25

Use strong induction on the positive integer

n

. The case

n = 1

is represented by the empty product. For

n > 1

, if

n

is prime it is already a product of one prime. Otherwise

n = ab

with

1 < a, b < n

; the induction hypothesis gives prime factorizations for both

a

and

b

, and concatenating them gives one for

n

. This proves existence in the fundamental theorem of arithmetic without presupposing uniqueness.

Strong induction Created 2026-09-24 Updated 2026-10-18

Strong induction establishes a proposition

P (n)

for all integers

n \geq n_{0}

. Prove

P (n_{0})

; then, for each

n \geq n_{0}

, assume every

P (k)

with

n_{0} \leq k \leq n

and prove

P (n + 1)

. The induction hypothesis includes all earlier cases, so the inductive step can use whichever smaller indices it needs. It cannot use

P (n + 1)

itself.^[ref]

This is useful when a construction breaks into smaller pieces of varying sizes. A prime factorization splits a composite number into smaller integer divisors, which need not be one less than the original integer. A recursive procedure can likewise call itself on several smaller inputs. The available cases should match those dependencies. Strong induction lets the mathematical proof follow the construction rather than forcing every step through the immediately preceding size.

Strong induction for factorization existence 2026-10-18

Every integer

n \geq 2

has a prime factorization. The induction base case

2

is prime. For a larger integer, either it is prime or it is

ab

, with

2 \leq a, b < n

. The induction hypothesis supplies prime factorizations of both smaller integer divisors; multiplying them gives one for

n

. This proves existence, while uniqueness requires the additional argument under the fundamental theorem of arithmetic.^[ref]

For the chosen number

84

, one possible recursive decomposition is

84 = 6 \cdot 14 = (2 \cdot 3) (2 \cdot 7) = 2^{2} \cdot 3 \cdot 7.

The step at

84

needs results for

6

and

14

, rather than a result for

83

. Each composite number in this factorization tree splits into strictly smaller positive integers, so recursive descent terminates at prime numbers. The tree describes one construction; another choice of integer divisors can give a differently shaped factorization tree.

Figure 1.
The step for 84 can use 6 and 14: the induction hypothesis covers both
. Original factorization tree $84 \to 6 \cdot 14$ , followed by $6 \to 2 \cdot 3$ and $14 \to 2 \cdot 7$ . Arrows show recursive dependencies toward smaller integers, rather than the order of increasing induction. The strip at the bottom marks the earlier cases available at the step for $84$ , with the required $6$ and $14$ highlighted. No use of the unproved case $84$ is permitted in the hypothesis. **Details**.

The same pattern explains the usefulness of strong induction for algorithm correctness. When a recursive procedure returns answers for smaller inputs, the induction hypothesis can justify those answers; the remaining task is to justify how the current call combines them. Strictly decreasing a nonnegative integer size measure establishes termination. Correctness also requires each call's conditions and its combination rule; termination alone does not make an algorithm correct.

Strong induction with four starting cases 2026-10-18

Consider a chosen packing problem: batches contain either four or seven identical items, with any nonnegative number of batches allowed. Which integer totals can be formed? The claim is that every total of at least eighteen is attainable:

\forall n \geq 18, \exists a, b \in N : n = 4 a + 7 b .

Here

a, b

count batches, so they must be nonnegative integers; the convention

N = {0, 1, 2, \dots}

permits omitting either size. Four direct starting cases are

18 = 4 + 7 + 7, 19 = 4 + 4 + 4 + 7, 20 = 4 + 4 + 4 + 4 + 4, 21 = 7 + 7 + 7.

(2)

n \geq 21

and every total from

18

through

n

is attainable, then

n - 3 \geq 18

is one of the cases available in the induction hypothesis. Add a batch of four to its representation to obtain

n + 1

. Thus the inductive step applies to every new total from

22

onward. Formally, one can start the strong induction at

18

and handle the next three totals directly before using the uniform step. The finite checks and the propagation together establish all totals, not merely those drawn below.

Figure 1.
Four starting cases seed every residue class when the step adds four
. Original chosen batch sizes $4$ and $7$ . Colored rows follow $18, 22, 26, \dots$ ; $19, 23, 27, \dots$ ; $20, 24, 28, \dots$ ; and $21, 25, 29, \dots$ . Each arrow adds a batch of four. The lower strip exhaustively checks totals through $29$ ; a cross means no representation by nonnegative batch counts. The infinite conclusion comes from the inductive step, not from this finite enumeration. **Details**.

Checking only

18

and repeatedly adding four would reach only totals congruent to

18

in modular arithmetic modulo four. The four induction base cases supply all four residue classes. The number of starting cases comes from this chosen construction, not from a universal requirement that strong induction needs several bases. A different construction can need different starting information.

The threshold is sharp for these batch sizes. If

17 = 4 a + 7 b

, reducing modulo four gives

3 b \equiv 1 (mod 4)

, so

b \equiv 3 (mod 4)

. A nonnegative

b

would therefore be at least three, giving

7 b \geq 21 > 17

, a contradiction. A finite failed search alone would need an explicit bound on

a, b

; this short modular arithmetic argument supplies a general obstruction.