Past exam of the mathematics course of the University of Cambridge / 2002 / iii / Paper 76 / 5

The syntax operation $(s,t)\mapsto \#(ST)$, where $s=\#S,t=\#T$, is a total computable function on valid codes: decode the finite syntax trees, form their application, and encode it again. Extend it arbitrarily on invalid codes if necessary. Similarly $n\mapsto \#(c_n)$ is total computable because the finite numeral syntax can be generated effectively from $n$. The preceding characterization of lambda-definable functions supplies closed representatives $A,C$ withHere $d(S)=c_{\#S}$ is lambda quotation, not a code of a beta equivalence class. In particular $C$ quotes the syntax of the numeral itself; it is not simply successor or an identity operation.

Choose $x$ fresh for $F$ and put $H=\lambda x.F(Ax(Cx))$, $Q=Hd(H)$. The preceding coding equations giveConsequentlyThis self-quoting fixed point is valid even if $F$ has free variables, since the effective Gödel numbering codes open lambda terms too. Freshness of $x$ prevents variable capture.

For the Church numeral system already used, the discriminatorhas $D{c}_{0}UV{\to }_{\beta }^{\ast }U$ and $D{c}_{1}UV{\to }_{\beta }^{\ast }V$ by the Church numeral zero test. More generally it chooses $V$ at every positive numeral. Only its values at zero and one are needed.

There is an argument-order defect in the printed flip context: the discriminator constructed above takes its numeral first. Fix $U\in \mathcal{U},V\in \mathcal{V}$ and useEquivalently, define $E=\lambda uvn.Dnuv$ and write the context as $\lambda x.EUV(Gx)$. This is an explicit permutation of the discriminator arguments, not an assumption that $DUV(Gx)$ has the required behavior.

Let $Q{\equiv }_{\beta }Fd(Q)$ be the self-quoting fixed point. There are exactly two cases. If $Gd(Q){\equiv }_{\beta }{c}_0$, then $Q{\equiv }_{\beta }U$, so closure under beta equivalence puts $Q$ in $\mathcal{U}$ and forces $Gd(Q){\equiv }_{\beta }{c}_1$. If $Gd(Q){\equiv }_{\beta }{c}_1$, then $Q{\equiv }_{\beta }V\in \mathcal{V}$, forcing $Gd(Q){\equiv }_{\beta }{c}_0$. Both contradict the distinct beta-normal Church numerals $c_0,c_1$. Hence no such total binary lambda classifier exists.

If beta equivalence were decidable, its decision algorithm would give a total computable function that outputs one exactly on codes of terms beta-equivalent to $I$, and zero on all other codes. Its numeral representation would be such a $G$, taking $\mathcal{U}$ to be the class of $I$ and $\mathcal{V}$ its complement. Both are nonempty: $K$ has a different beta-normal form from $I$. The contradiction proves beta equality is undecidable. It is nevertheless semidecidable, since finite conversion proofs can be effectively enumerated.