Past exam of the mathematics course of the University of Cambridge / 2026 / iii / Paper 120 / 3

A partial function $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$ is lambda-definable if there is a lambda term $F$ such thatwhenever the value is defined, while outside the domain the application reduces to no Church numeral.

Solved by gpt-5.6-sol high.

The Strong normalization theorem for simply typed lambda calculus says that every well-typed term has no infinite beta-reduction sequence. In the untyped calculus,reduces to itself and is therefore not strongly normalizing.

Solved by gpt-5.6-sol high.

The nowhere-defined partial function is represented byFor every Church numeral $c_m$, the term $F{c}_m$ reduces to $\Omega$ and hence to no numeral. If $F$ had type $Nat\to Nat$, the strong normalization theorem would make every reduction sequence from $F$ finite, contradicting the visible infinite reduction inside $\Omega$. Thus this partial function is lambda-definable by an untypable term of the required kind.

Solved by gpt-5.6-sol high.

A closed beta-eta-long normal term of type $\sigma \to \sigma \to \sigma$ must have the form $\lambda x:\sigma .\lambda y:\sigma .t$, where the normal term $t:\sigma$ can only be $x$ or $y$: the pure calculus has no constants or other closed source of a value of the atomic type $\sigma$. Hence the only two beta-eta-equivalence classes are the Church Booleans

Solved by gpt-5.6-sol high.

TakeIt has type $Boo{l}_{\sigma }\to Boo{l}_{\sigma }\to Boo{l}_{\sigma }$. If $a{\equiv }_{\beta }\top$, the body selects $x$. If $a{\equiv }_{\beta }\perp$, it reduces to $bxy$, which selects $x$ exactly when $b{\equiv }_{\beta }\top$. Thus it has the stated truth table.

Solved by gpt-5.6-sol high.

For $a\in \{0,1\}$ define a typed transition term $D_a:\sigma \to \sigma$ by a nested Boolean choice:Here a Church Boolean acts as an if-then-else operator. The assumed behavior of $e{q}_{\sigma }$ gives $D_a{q}_i{\equiv }_{\beta }{q}_{\delta (q_i,a)}$.

For $w=a_1\cdots a_k$, putand use $ϵ=\lambda x.x$. Induction on the word length gives

Solved by gpt-5.6-sol high.

Given a finite input word $w$, construct the typed term $\mathbf{w}{q}_0$ effectively and beta-normalize it. The Strong normalization theorem for simply typed lambda calculus guarantees termination, and confluence gives exactly one of the finitely many normal forms $q_i$. Compare that normal form syntactically with the listed accepting states in $F$. This algorithm accepts exactly when ${\delta }^{\ast }(q_0,w)\in F$, so $L$ is recursive. Equivalently, this is the standard theorem that every language recognized by a deterministic finite automaton is a regular language and hence decidable.

Solved by gpt-5.6-sol high.