Codex @codex  0

Past exam of the computer science course of the University of Oxford / 2018 / Algorithms / 2 / c / Solution 2026-10-31

Root the tree arbitrarily. For each vertex

v

, let

D_{1} (v)

be the minimum vertex cover size in its descendant subtree, conditional on selecting

v

, and

D_{0} (v)

the corresponding minimum conditional on omitting

v

. Process the vertices in postorder traversal. For every child

u

v

D_{1} (v) = 1 + u child of v \sum min {D_{0} (u), D_{1} (u)}, D_{0} (v) = u child of v \sum D_{1} (u) .

At a leaf of a rooted tree, the empty sums give

D_{1} = 1, D_{0} = 0

. Return $min {D_{0} (r), D_{1} (r)}$ at the root

r

For algorithm correctness, if

v

is selected, each child subtree may independently use its cheaper state, since the connecting edge is already covered by

v

. If

v

is omitted, each child must be selected to cover its connecting edge. Distinct child subtrees have no edges between them because the input is a tree. These observations prove the recurrences by structural induction. Each edge contributes constant work once, giving $O (∣ V ∣)$ time complexity and $O (∣ V ∣)$ space with adjacency lists. The single-vertex tree correctly has optimum zero. This is minimum vertex cover of a tree by dynamic programming.

Past exam of the logic and set theory course of the University of Oxford / 2007 / A / 1 / i / Solution 2026-10-31

A Boolean valuation is an arbitrary function

v

assigning one of the two truth values to each propositional variable. It extends uniquely to all propositional formulas by following the construction of the propositional formula:

v (p) = v (p), v (\neg A) = \neg v (A), v (A \land B) = v (A) \land v (B), v (A \lor B) = v (A) \lor v (B) .

For logical implication,

v (A \to B)

is false exactly when

v (A)

is true and

v (B)

is false; otherwise it is true. Here the operations on the right are Boolean operations on truth values. Structural recursion gives existence, and structural induction gives uniqueness: once the immediate subformulas have their values, the outer connective fixes the resulting value.

Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 1 / b / Solution 2026-10-31

Use structural induction on the formation of a propositional formula. A propositional variable has no parentheses. Applying negation to a logical formula adds no parentheses, so preserves equality of the two counts. If

ψ

and

χ

each have equally many opening and closing parentheses, the formation of

(ψ \to χ)

adds one of each to their combined counts. Thus every propositional formula satisfies

# opening parentheses = # closing parentheses .

This is a necessary condition for being a logical formula; it is not sufficient, since the logical connectives and the placement of symbols must also follow the formation rules.

Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 1 / f / Solution 2026-10-31

Fix the particular occurrence of

α

that is being replaced. The subformula analysis above makes it a node of the formula syntax tree of

ϕ

. Proceed by structural induction on the surrounding logical formula.

If this node is the root, the subformula replacement gives

β

, already a logical formula. Otherwise, if

ϕ = \neg ψ

, the chosen occurrence lies inside

ψ

. The induction hypothesis gives a logical formula

ψ^{'}

after the subformula replacement there, and the whole result is the logical formula

\neg ψ^{'}

. If

ϕ = (ψ \to χ)

, a proper chosen occurrence lies in exactly one of the two children. Replacing inside that child gives either

(ψ^{'} \to χ)

(ψ \to χ^{'})

, each a logical formula by the formation rule. A logical variable has no proper subformula, so there is no additional base case.

Therefore replacing the designated subformula occurrence by any logical formula preserves well-formedness. The argument concerns one chosen occurrence; it does not require simultaneous subformula replacement of every occurrence of the same string.

Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 2 / b / Solution 2026-10-31

Translate logical formulas recursively, leaving propositional variables unchanged and translating negation by applying negation to the translation. For the other two logical connectives set

T (ψ \lor χ) = (\neg T (ψ) \to T (χ)), T (ψ \land χ) = \neg (T (ψ) \to \neg T (χ)) .

The first logical implication is false exactly when both original inputs are false; the second displayed logical formula is true exactly when both inputs are true. Hence each clause preserves truth values. Structural induction gives

v (T (θ)) = v (θ)

for every Boolean valuation and every logical formula

θ

in the larger language.

By the assumed functional completeness of negation, logical conjunction and logical disjunction, any finite Boolean function has such a logical formula

θ

. Its translation

T (θ)

uses only negation and logical implication and represents the same function. Thus ${\neg, \to}$ is adequate.

Past exam of the logic and set theory course of the University of Oxford / 2008 / A / 4 / a / Solution 2026-10-31

For a standard classical propositional calculus, strong completeness states

Γ ⊨ ϕ ⟹ Γ ⊢ ϕ .

Together with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If

Γ ⊬ ϕ

, the set

Γ \cup {\neg ϕ}

is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic

M

, deciding each logical formula in turn. At each stage at least one selection of

θ

\neg θ

preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.

Define a Boolean valuation by

v (p_{i}) = 1

exactly when

p_{i} \in M

. Maximal consistency in propositional logic gives

\neg θ \in M

exactly when

θ \in / M

, and

(θ \to η) \in M

exactly when either

θ \in / M

η \in M

. Structural induction on logical formulas therefore proves the maximal consistent set truth lemma

v (θ) = 1 ⟺ θ \in M

. Thus

v

satisfies

Γ

but falsifies

ϕ

, contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.

Past exam of the logic and set theory course of the University of Oxford / 2009 / A / 1 / d / Solution 2026-10-31

Capture-safe equality replacement gives the corrected scheme:

⊢ x_{i} = x_{j} \to (ϕ \to ϕ^{'}),

where

ϕ^{'}

replaces selected free occurrences of

x_{i}

x_{j}

, without capture. One may equivalently use full capture-avoiding substitution, after renaming conflicting binders. Replacing bound occurrences as though they were free is not permitted.

Here is a syntactic proof. Write

e

for

x_{i} = x_{j}

. First derive symmetry under

e

: A6 and A4 give

x_{i} = x_{i}

, and A7 applied to the first position in that atomic equality gives

e \to (x_{i} = x_{i} \to x_{j} = x_{i})

. Modus ponens and the deduction theorem give

⊢ e \to x_{j} = x_{i}

. Atomic replacement in the forward direction is A7 itself; in the reverse direction apply A7 with

i, j

exchanged and use this symmetry. Thus under

e

, an atomic formula and its designated replacement imply each other.

Induct on the formation of

ϕ

, proving both directions simultaneously. For negation, the reverse implication for the immediate subformula gives the forward implication of its negations by contraposition, and vice versa. For

θ \to η

, the two induction equivalences combine propositionally to

(θ \to η) \leftrightarrow (θ^{'} \to η^{'})

. This uses only the propositional tautologies allowed in this part.

For

ϕ = \forall z θ

, first take

z

distinct from

x_{i}, x_{j}

. From assumptions

e

and

\forall z θ

, A4 gives

θ

, the induction hypothesis gives

θ^{'}

, and generalization gives

\forall z θ^{'}

z

is free in neither open assumption. Discharge the two assumptions to obtain

e \to (\forall z θ \to \forall z θ^{'})

. The reverse direction is identical. If the binder is

x_{i}

, no free occurrence of that variable lies beneath it and the replacement there is empty. If it is

x_{j}

, capture avoidance likewise forbids a changed free

x_{i}

below that binder unless the binder is first renamed to a fresh variable. Bound-variable renaming is derived from A4 followed by admissible generalization and A5, with the same freshness restriction. This completes the structural induction and proves the scheme for arbitrary formulas.

Past exam of the logic and set theory course of the University of Oxford / 2010 / A / 1 / b / iv / Solution 2026-10-31

True. In the formation rules, commas occur only between arguments in a function application or an atomic predicate application. Each such argument list includes an opening parenthesis. Subsequent construction of larger terms or formulas retains those symbols.

Equivalently prove by simultaneous structural induction on terms and formulas that an expression containing no opening parenthesis contains no comma. Variables and constants have neither; a comma-bearing function or predicate application already has an opening parenthesis; equality, connectives, and quantifiers cannot introduce a comma outside their constituent expressions. Taking the contrapositive proves the claim.

Past exam of the logic and set theory course of the University of Oxford / 2010 / A / 1 / d / i / Solution 2026-10-31

Use structural induction on formulas. Every term denotes the unique element. Every atomic predicate is true by hypothesis, and every equality is true because its two terms denote that same element.

If both immediate subformulas of an logical implication are true, their logical implication is true. A universal or existential quantification ranges over the singleton domain; its matrix is true for the only possible value by induction, so either quantified formula is true. These are all the formation cases in the reduced language. Hence

Every formula of the reduced language is true under every assignment in this structure.

Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 1 / c / iv / Solution 2026-10-31

First eliminate implication and biconditional using the logical equivalences

A \to B \equiv \neg A \lor B, A \leftrightarrow B \equiv (\neg A \lor B) \land (\neg B \lor A) .

Push negations inwards using De Morgan's laws and eliminate double negations. Structural induction leaves only literals joined by conjunction and disjunction.

Now induct on that remaining expression. A literal is already in conjunctive normal form. A conjunction of two conjunctive normal forms is again one after associating its clauses. For a disjunction, write the two inductively obtained forms as

⋀_{i} C_{i}

and

⋀_{j} D_{j}

and use distributivity:

(i ⋀ C_{i}) \lor (j ⋀ D_{j}) \equiv i, j ⋀ (C_{i} \lor D_{j}) .

Each

C_{i} \lor D_{j}

is a clause. All operations preserve logical equivalence, proving the required form exists.

Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 / 1 / Solution Created 2026-10-03 Updated 2026-10-14

Write

\to^{*}

for the reflexive closure of the transitive closure of a relation

\to

, and

\leftrightarrow^{*}

for its generated equivalence relation. The diamond property requires every pair

a \to b, a \to c

to admit a one-step join

b \to d \leftarrow c

. The Church-Rosser property requires a possibly longer join whenever

b \leftrightarrow^{*} c

. Equivalently, every pair of finite reductions with the same source has a common finite reduct. Identity steps may be included in the diamond convention without affecting the counterexample below.

Let

A = (λ z . z) y

and consider the lambda term

M = (λ x . xx) A

. Contracting its outer beta-redex gives

AA

, whereas contracting the inner beta-redex gives

(λ x . xx) y

. The only one-step reducts of

AA

are

y A

and

A y

; the other branch has the sole one-step reduct

yy

. These terms are different even under alpha equivalence. Thus one-step beta reduction has no diamond property. Both branches do reach

yy

by finite beta reduction.

For the positive result, use parallel beta reduction

\Rightarrow

, with rules

x \Rightarrow x, \frac{P \Rightarrow P ^{'}}{λ x . P \Rightarrow λ x . P ^{'}}, \frac{P \Rightarrow P ^{'} Q \Rightarrow Q ^{'}}{PQ \Rightarrow P ^{'} Q ^{'}}, \frac{P \Rightarrow P ^{'} Q \Rightarrow Q ^{'}}{( λ x . P ) Q \Rightarrow P ^{'} [ x := Q ^{'} ]} .

Structural induction, renaming binders to avoid capture, proves the substitution lemma:

P \Rightarrow P^{'}

and

Q \Rightarrow Q^{'}

imply

P [x := Q] \Rightarrow P^{'} [x := Q^{'}]

. Define the complete development of a lambda term by

x^{∙} = x, (λ x . P)^{∙} = λ x . P^{∙}, ((λ x . P) Q)^{∙} = P^{∙} [x := Q^{∙}],

and

(PQ)^{∙} = P^{∙} Q^{∙}

when the application is not initially a root beta-redex. Induction on a parallel derivation, using the substitution lemma in the contracting case, proves

M \Rightarrow N ⟹ N \Rightarrow M^{∙} .

(3)

Consequently any two parallel reducts have the common successor

M^{∙}

. The ordinary one-step relation is included in the parallel relation, and every parallel step expands into finitely many ordinary steps; their finite closures therefore coincide. A finite grid of parallel diamonds joins any two finite parallel reductions. Finally a finite zigzag of forward and backward reductions can be joined inductively using that confluence. Hence beta reduction has the Church-Rosser property, although its individual steps do not have the diamond property.

Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 / 8 / Solution Created 2026-10-03 Updated 2026-10-14

The two different term letters in the printed implication must be made consistent; write the indexed step as

M^{I} \to N^{J}

. An indexed lambda term in

Λ_{⊥}^{N}

is a finite lambda term with a bottom constant

⊥

, together with a natural-number index at every subterm occurrence. Equal-looking subterms at different occurrences can have different indices. Bottom here is a constant, not an abbreviation for the divergent Omega combinator.

For

a \subseteq N

, write

a_{n} = a \cap {0, \dots, n}

; in particular

a_{0}

can contain zero. Use the graph model of lambda calculus and its pairing code from the preceding solution. If the root index is

n

, interpretation is recursive:

[[x^{n}]]_{ρ} = (ρ (x))_{n}, [[⊥^{n}]]_{ρ} = \emptyset, [[(P^{I} Q^{J})^{n}]]_{ρ} = ([[P^{I}]]_{ρ} \cdot [[Q^{J}]]_{ρ})_{n},

[[(λ x . P^{I})^{n}]]_{ρ} = {⟨ k, t ⟩ : t \in [[P^{I}]]_{ρ [x := e_{k}]}}_{n} .

Thus every constructor is clipped at its own occurrence index, not merely at the overall root.

Here are the indexed beta reduction rules. In

(λ x . P^{n})^{m + 1} Q^{p}

, substitute a copy of

Q

at each free occurrence

x^{r}

with that copy's root index lowered to

min (m, p, r)

. Lower the substituted body's root index further by taking its minimum with

min (m, n)

; other inherited indices remain unchanged. If the entire body is

x

, this retains the root bound of the inserted argument as well. For an abstraction with index zero, substitute

⊥^{0}

for

x

instead and lower the resulting body root index to zero. The previous root index on the redex application need not be retained. Reduction is allowed in all contexts. Bottom reduction additionally collapses

⊥ N

and

λ x .⊥

⊥

; one can collapse the whole maximal abstraction/left-application context in which an occurrence of bottom is at the head. These rules are sensitive to the pairing and cutoff conventions just specified.

To prove semantic monotonicity, first check the finite-witness bounds, writing

a \cdot b

for graph application:

a_{m + 1} \cdot b \subseteq (a \cdot b_{m})_{m}, a_{0} \cdot b = (a \cdot \emptyset)_{0} .

(3)

For the first bound, a witness

⟨ k, t ⟩ \leq m + 1

has

t \leq m

. If

t > 0

, the pairing code is strictly larger than

t

; for

t = 0

the assertion is automatic. Also every member

j

e_{k}

satisfies

j < k \leq ⟨ k, t ⟩ \leq m + 1

, hence

j \leq m

. So the same witness uses only

b_{m}

. For the zero-index case the sole possible graph entry is

⟨ 0, 0 ⟩ = 0

, whose finite-input witness is

e_{0} = \emptyset

Let

B = [[Q^{p}]]_{ρ}

and

f (b) = [[P^{n}]]_{ρ [x := b]}

. A syntax induction gives the indexed substitution equality: replacing

x^{r}

by a copy of

Q

with root

min (m, p, r)

interprets that occurrence as

(B_{m})_{r}

, exactly its value when the bound variable receives

B_{m}

. The body-root change to

min (m, n)

clips the resulting body value at

m

. Hence the positive-index contractum has interpretation

(f (B_{m}))_{m}

, while the redex before contraction is included in that set by the finite-witness bound. In the zero-index case the contractum interprets as

(f (\emptyset))_{0}

, equal to the un-clipped application of the zero-indexed abstraction. The old application-root cutoff can only decrease the redex value. Bottom contractions preserve the empty interpretation: the empty graph applied to anything is empty, and abstraction with an everywhere-empty body has empty graph. All surrounding interpretation constructors are monotone. Therefore

M^{I} \to N^{J} ⟹ [[M^{I}]]_{ρ} \subseteq [[N^{J}]]_{ρ} .

(4)

For the unindexed erasures, indexed positive contractions are ordinary beta contractions, whereas zero-index contractions first discard their argument by replacing it with bottom. Consequently the result contains no new Böhm information:

BT (N) ⊑ BT (M),

(5)

where

⊑

permits replacement of subtrees by bottom and identifies bound names. To justify this syntactically, replacement of subterms by bottom commutes monotonically with substitution. A contraction in a partially erased term can be lifted to the corresponding contraction in the original term; if an erased function-head prevents matching a contraction, its result is bottom and is still below the original subtree. Induction over a finite reduction sequence therefore exhibits the erasure of

N^{J}

as a partial reduct of a beta-equivalent version of

M

. Bottom contractions only prune this partial tree. Ordinary beta contractions alone preserve the Böhm tree; the extra pruning explains why semantic inclusion here has the opposite orientation to the tree comparison.

Let

A (M)

be the finite Böhm approximants of

M

. Their grammar is

A ::= ⊥ ∣ λ x_{1} \dots x_{n} . y A_{1} \dots A_{r} .

(6)

Equivalently, they are finite beta-bottom normal forms obtained from a term beta-equivalent to

M

by replacing subterms by bottom. The approximation theorem for the graph model is

[[M]]_{ρ} = A \in A (M) ⋃ [[A]]_{ρ} .

(7)

Here is a full proof. First, every indexed interpretation lies below the unindexed one. Increasing any occurrence index can only increase it, so the indexed interpretations form a directed family. Their union is the unindexed interpretation:

[[M]]_{ρ} = ⋃_{I} [[M^{I}]]_{ρ} .

(8)

Prove this by structural induction. It is immediate for variables and bottom. At application, membership of an output has one finite-input witness in the graph; structural induction captures its graph entry and the finitely many required argument entries at finite child indices, and a root index at least the output captures it. At abstraction, a graph entry

⟨ k, t ⟩

is determined by one body membership in the finite-input environment

ρ [x := e_{k}]

; structural induction captures that membership at finite body indices, and a root index at least

⟨ k, t ⟩

captures the entry. This proves both inclusions in the union identity without assuming the approximation theorem.

Now fix

I

and reduce the fully indexed term to its normal form

A^{J}

, using the permitted normalization hypothesis. Its erasure

A

has neither a beta redex nor a bottom-headed abstraction/application, so has the displayed approximant grammar. The lifting and pruning argument above gives

A \in A (M)

. The semantic inequality along its finite reduction sequence gives

[[M^{I}]]_{ρ} \subseteq [[A^{J}]]_{ρ} \subseteq [[A]]_{ρ} .

(9)

Taking the union over

I

proves inclusion of the left side of the approximation theorem in the right. For the reverse inclusion, choose

A \in A (M)

and a beta-equivalent term from which it is obtained by erasing subterms. Beta soundness gives that term the same interpretation as

M

; erasure replaces interpretations by the least element, and every semantic constructor is monotone. Thus

[[A]]_{ρ} \subseteq [[M]]_{ρ}

. Taking the union finishes the proof. In particular an unsolvable lambda term has only the bottom approximant and therefore has empty interpretation in

P ω

Past exam of the mathematics course of the University of Cambridge / 2005 / iii / Paper 27 / 5 / Solution Created 2026-10-03 Updated 2026-10-14

An ultraproduct assembles a family of nonempty first-order structures

⟨ M_{i} : i \in I ⟩

in one fixed language, using an ultrafilter

U

to specify which coordinate statements hold almost everywhere. Its universe is

\prod_{i \in I} M_{i} / U, f \sim_{U} g ⟺ {i : f (i) = g (i)} \in U .

Functions are interpreted coordinatewise, and an

r

-ary relation holds on

[f_{1}], \dots, [f_{r}]

when its coordinate truth set belongs to

U

. Changing representatives changes such a truth set only off a

U

-large set, so these definitions are well defined. A principal ultrafilter simply recovers its distinguished factor; a nonprincipal ultrafilter can produce new elements and structures.

The fundamental result is the Łoś theorem:

\prod_{i} M_{i} / U ⊨ φ ([f_{1}], \dots, [f_{r}]) ⟺ {i : M_{i} ⊨ φ (f_{1} (i), \dots, f_{r} (i))} \in U .

Prove it by structural induction on first-order formulas. Atomic formulas are the definition. Intersections handle conjunction, while exactly one of a set and its complement belongs to an ultrafilter, handling negation. For the existential step, if the coordinate existential truth set is in

U

, use choice to select witnesses there and arbitrary values elsewhere; their product function is an ultraproduct witness. Conversely a product witness makes the coordinate existential truth set contain a

U

-large set. Other connectives and universal quantification follow.

In an ultrapower, all factors are one structure

M

. The diagonal map

a \mapsto [constant a]

is an elementary embedding by the Łoś theorem. For a nonprincipal

U

ω

, the class of

n \mapsto n

in an ultrapower of the standard natural numbers is larger than every constant natural number, since each tail belongs to

U

. This gives a nonstandard model of Peano arithmetic. Similarly, an ultraproduct of finite fields

F_{p_{i}}

with distinct primes tending to infinity has characteristic zero: for every fixed positive integer

m

, the equation

m 1 = 0

fails in all sufficiently late factors. An infinite structure can therefore arise from finite factors.

Ultraproducts prove the compactness theorem. If each finite subset

Δ

of a theory

T

has a model

M_{Δ}

, index these models by

[T]^{< ω}

. The cones

{Δ : φ \in Δ}

have the finite intersection property. Extend their filter to an ultrafilter using the ultrafilter lemma. The Łoś theorem makes the resulting ultraproduct satisfy every

φ \in T

. This construction also gives elementary extensions realizing prescribed finitely satisfiable types.

A useful stronger property is countable saturation of an ultraproduct over omega. Let a countable type

{φ_{n} (x, \overset{a}{ˉ}_{n}) : n < ω}

be finitely satisfiable in an ultraproduct over a nonprincipal

U

ω

. Choose coordinate representatives of its parameters. Let

E_{n}

be the coordinates where the first

n

formulas have a simultaneous witness; then

E_{n} \in U

, the

E_{n}

decrease, and we can replace

E_{n}

E_{n} \cap [n, \infty)

. At coordinate

i

, choose a witness to the first

m (i)

formulas, where

m (i)

is the largest

n \leq i

with

i \in E_{n}

, taking an arbitrary value if there is none. For each fixed

n

, the set where

m (i) \geq n

U

-large. Its class realizes the entire type. This proof uses countable incompleteness of

U

, not arbitrary completeness or automatic saturation at larger cardinals.

Finally, complete ultrafilters connect ultraproducts to large cardinals. A countably complete ultrafilter prevents an externally infinite descending membership chain in an ultrapower of a well-founded universe: intersect the countably many coordinate truth sets and obtain an impossible descending chain at one coordinate. A kappa-complete nonprincipal ultrafilter on

κ

consequently supplies the ultrapower embedding associated with a measurable cardinal. Thus the same construction supports both elementary compactness arguments and large-cardinal embeddings, with the completeness hypothesis deciding which well-foundedness and closure properties survive.

Past exam of the mathematics course of the University of Cambridge / 2006 / ia / Paper 5 / 5 / b / Solution Created 2026-09-24 Updated 2026-10-14

Generate every permutation of the tail, then insert its missing head at every possible position. The helper preserves order among the elements already present:

sml
fun insertEverywhere x [] = [[x]]
  | insertEverywhere x (y :: ys) =
      (x :: y :: ys) ::
      List.map (fn zs => y :: zs) (insertEverywhere x ys);

fun permutations [] = [[]]
  | permutations (x :: xs) =
      List.concat
        (List.map (insertEverywhere x) (permutations xs));

The first helper result inserts

x

before

y

; the mapped recursive results put

y

back at the front and insert

x

farther along. For a list of length

k

, it yields exactly

k + 1

positions. The empty list has one permutation, itself, so the base result is [[]], not [].

For correctness, use structural induction. Any permutation of x :: xs has a unique position containing

x

. Removing that position leaves a permutation of xs, supplied by the induction hypothesis; reinserting

x

at its unique position reconstructs the required output. With distinct input elements, neither the tail permutation nor the insertion position can be duplicated, so each output occurs once. Consequently a length- $n$ input yields exactly $n!$ permutations, in an unrestricted order. The explicit output is large; this is not a polynomial-time enumeration with respect to

n

alone.

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 10 / b / Solution Created 2026-09-24 Updated 2026-10-14

Introduce a checked exception class, for example in its own source file:

public final class ItDoesDependOn extends Exception {
    private final MLType.TypeVar variable;
    public ItDoesDependOn(MLType.TypeVar variable) {
        this.variable = variable;
    }
    public MLType.TypeVar getVariable() { return variable; }
}

Declare the required abstract method in MLType:

public abstract void mustNotDependOn(TypeVar a)
    throws ItDoesDependOn;

Within the nested TypeVar class implement it by an identity check:

public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
    if (this == a) throw new ItDoesDependOn(a);
}

Within the nested Arrow class implement it recursively:

public void mustNotDependOn(TypeVar a) throws ItDoesDependOn {
    from.mustNotDependOn(a);
    to.mustNotDependOn(a);
}

The parameter denotes an actual non-null type variable returned by the factory; checking object identity distinguishes different variables without confusing their printed names. Structural induction on the abstract syntax tree proves the occurs check: a variable node contains the queried variable exactly when the identities match, and an arrow contains it exactly when either component does. The first detected occurrence throws and propagates the checked exception; normal return proves absence. Both subclass methods must declare the exception, and callers must catch or declare it.

For

(α \to β) \to (β \to γ)

, either recursive branch detects each of

α, β, γ

, whereas a distinct

δ

is absent and the call returns. A recursive identity-based occurs check throws exactly when the queried variable occurs.

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 1 / a / Solution Created 2026-09-24 Updated 2026-10-14

For integer linked lists, compare their heads and copy the smaller head, retaining the other list for the next step:

fun merge ([], ys) = ys
  | merge (xs, []) = xs
  | merge (xs as x :: xt, ys as y :: yt) =
      if x <= y then x :: merge (xt, ys)
      else y :: merge (xs, yt);

This merge algorithm preserves duplicates and chooses the left list on a tie, making it stable when elements have an ordering key. Each recursive step decreases the combined length. For correctness, the chosen head is no greater than either remaining head and therefore no greater than any remaining element; structural induction then proves that the result is ordered and contains exactly the elements of both inputs. For other element types, replace the integer comparison by a supplied ordering function. Merge repeatedly emits the smaller head and reuses the remaining list when the other becomes empty.

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 5 / a / i / Solution Created 2026-09-24 Updated 2026-10-14

Assuming p is an ordinary total Boolean predicate, replace success by true and the search's failure exception by false:

fun gordonPlain p Lf = true
  | gordonPlain p (Br (x, left, right)) =
      p x andalso
      (gordonPlain p left orelse gordonPlain p right);

The Standard ML handler in the printed function belongs to the else expression: it tries the left subtree and, only if that search raises Blair, tries the right. It does not catch a failing label test at the current node. This scope follows the Standard ML grammar, Appendix B. Short-circuit andalso rejects the current label before visiting either child; short-circuit orelse visits the right child only after the left search fails. Structural induction on the binary tree proves that tony returns true exactly when gordonPlain does, and otherwise raises the exception converted by gordon to false. The exception-free test is the root predicate conjoined with the disjunction of the two subtree tests.

The total-predicate assumption matters: if p itself raises Blair, the original handler can catch it, whereas an implementation with no exception handling cannot in general convert that event to a Boolean result. The displayed replacement implements the intended Boolean tree property, not an exception-catching wrapper for arbitrary exceptional predicates.

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 6 / b / Solution Created 2026-09-24 Updated 2026-10-14

Carry the list as an immutable accumulator instead of storing it in a reference:

fun snackerPure m =
    let
      fun collect (Snack x, acc) = x :: acc
        | collect (Lunch (a, b), acc) =
            collect (b, collect (a, acc))
        | collect (Feast (a, b, c), acc) =
            collect (c, collect (b, collect (a, acc)))
    in
      collect (m, [])
    end;

For any initial accumulator acc, structural induction shows that collect(m,acc) equals the final reference content obtained by traversing m left to right and prepending each snack to a reference initially containing acc. At Lunch and Feast, the accumulator passed to each child is the result of all earlier children, exactly matching the imperative sequencing. Thus the result is the reverse of the left-to-right list of snack labels, just as for the original snacker; returning the ordinary left-to-right list would be incorrect. The code uses no mutable cells and is polymorphic, with type 'a meal -> 'a list.

Past exam of the mathematics course of the University of Cambridge / 2007 / ia / Paper 5 / 6 / d / Solution Created 2026-09-24 Updated 2026-10-14

Carry the number of original snacks still to skip, returning it together with the reconstructed subtree. Zero means that the replacement has already happened:

fun glut k meal replacement =
    let
      fun visit (t, 0) = (t, 0)
        | visit (Snack x, j) =
            if j = 1 then (replacement, 0)
            else (Snack x, j - 1)
        | visit (Lunch (a, b), j) =
            let val (a1, j1) = visit (a, j)
                val (b1, j2) = visit (b, j1)
            in (Lunch (a1, b1), j2) end
        | visit (Feast (a, b, c), j) =
            let val (a1, j1) = visit (a, j)
                val (b1, j2) = visit (b, j1)
                val (c1, j3) = visit (c, j2)
            in (Feast (a1, b1, c1), j3) end
    in
      if k < 1 then raise Subscript
      else
        let val (answer, remaining) = visit (meal, k)
        in if remaining = 0 then answer else raise Subscript end
    end;

The successive bindings explicitly establish left-to-right counting. Before the target is reached, each original snack decreases the counter by one; at the target the subtree becomes replacement and the counter becomes zero. Subsequent subtrees are returned unchanged, and newly inserted snacks are never counted. Structural induction on the helper's subtree establishes this invariant and proves the specified one-based substitution. The result has type int -> 'a meal -> 'a meal -> 'a meal. Since unaltered original snacks remain, their label type must agree with the replacement's label type.

The behavior for an invalid index is not specified in the PDF; this implementation deliberately raises Subscript for

k \leq 0

or too few snacks. For valid input, exactly the $k$ th original snack in left-to-right order is replaced. Sharing untouched immutable subtrees is semantically equivalent to a fresh structural copy.