Past exam of the mathematics course of the University of Cambridge / 2025 / iii / Paper 120 / 2

The Church-Rosser theorem states that if $M{\twoheadrightarrow }_{\beta }{N}_1$ and $M{\twoheadrightarrow }_{\beta }{N}_2$, then there is a term $P$ with $N_1{\twoheadrightarrow }_{\beta }P$ and $N_2{\twoheadrightarrow }_{\beta }P$. Equivalently, beta reduction is confluent.

Solved by gpt-5.6-sol high.

The Weak normalization theorem for simply typed lambda calculus says that every term typable in the implicational simply typed lambda calculus has a beta-normal form. Define reducibility by induction on types: a term of atomic type is reducible when it is weakly normalizing, and $M:A\to B$ is reducible when $MN$ is reducible at $B$ for every reducible $N:A$. Induction on types shows that every reducible term is weakly normalizing and that variables are reducible.

The fundamental substitution lemma is proved by induction on a typing derivation: if $\Gamma ⊢M:A$ and each variable in $\Gamma$ is replaced by a reducible term of its declared type, then the resulting term is reducible at $A$. The application case is the definition at arrow type; in the abstraction case, applying the abstraction to any reducible argument makes one beta step to the substituted body, which is reducible by induction. Substituting each free variable by itself makes every well-typed term reducible, hence weakly normalizing.

Solved by gpt-5.6-sol high.

A lambda term $F$ lambda-defines $f:{\mathbb{N}}^k\to \mathbb{N}$ when, for all $n_1,\dots ,n_k$,where $c_n$ is the Church numeral for $n$.

Solved by gpt-5.6-sol high.

No. Let $c_0=\lambda f.\lambda x.x$ and setBoth terms send every Church numeral to $c_0$, so both define the constant-zero function. They are distinct beta-normal forms, however, and the Church-Rosser theorem implies that distinct beta-normal forms cannot be beta-equivalent.

Solved by gpt-5.6-sol high.

TakeIf $L$ is a fixed-point combinator, then $Lf{\equiv }_{\beta }f(Lf)$, so eta-conversion givesConversely, if $L{\equiv }_{\beta \eta }\delta L$, application to an arbitrary $f$ gives $Lf{\equiv }_{\beta \eta }f(Lf)$, which is precisely the fixed-point-combinator property.

Solved by gpt-5.6-sol high.