Past exam of the mathematics course of the University of Cambridge / 2013 / iii / Paper 20 (Computability and Logic)

Fix a finite alphabet $\Sigma$. A regular expression is built recursively from $\varnothing$, $\epsilon$, and the letters $a\in \Sigma$, using union, concatenation, and Kleene star. Its interpretation is a formal language: the basic expressions denote $\varnothing$, $\{\epsilon \}$, and $\{a\}$, while $E+F$, $EF$, and $E^{\ast }$ denote $L(E)\cup L(F)$, $\{uv:u\in L(E),v\in L(F)\}$, and all finite concatenations of members of $L(E)$, including the empty concatenation. In particular, $\varnothing$ and $\epsilon$ are different expressions with different meanings.

Kleene theorem identifies exactly the languages described by regular expressions with those recognized by finite-state automata. Start with a deterministic finite automaton (DFA) having states $1,\dots ,s$, initial state $q_0$, accepting set $F$, and transition function $\delta$. Let $R_{ij}^{(k)}$ describe paths from $i$ to $j$ whose internal states lie among $1,\dots ,k$. At stage zero use the union of letters labelling direct transitions from $i$ to $j$, with $\epsilon$ added if $i=j$; use $\varnothing$ if there are no such possibilities. Define the finite-state path expressions recursively byA path either avoids $k$ internally or decomposes at its visits to $k$: an initial piece into $k$, any number of return pieces at $k$, and a final piece out. Each piece has no internal occurrence of $k$. This proves the recursion by induction, including paths with $i=k$ or $j=k$, where empty pieces are permitted. Thusis a regular expression for the DFA's accepted formal language. An empty accepting set gives the expression $\varnothing$. This is the path form of state elimination for finite automata.

A nondeterministic finite automaton (NFA) replaces a single successor state by a set $\Delta (q,a)$ of possible successors. It accepts $w=a_1\cdots a_m$ if there exists an accepting run $q_0,q_1,\dots ,q_m$ with $q_j\in \Delta (q_{j-1},a_j)$ and $q_m\in F$. Rejection means that no accepting run exists, rather than that some run rejects. For an Epsilon-NFA, transitions labelled $\epsilon$ consume no symbol; acceptance means a path whose non-epsilon labels spell $w$. In particular, acceptance of the empty word is tested using the epsilon closure of the initial state.

The same Kleene theorem holds for nondeterministic finite automata. For an NFA without epsilon transitions, the powerset construction has state set $\mathcal{P}(Q)$, initial state $\{q_0\}$, transition $S\mapsto {\bigcup }_{q\in S}\Delta (q,a)$ on letter $a$, and accepting subsets meeting $F$. Induction on word length shows that its state is exactly the set of possible current NFA states. For an Epsilon-NFA, start from $E(\{q_0\})$, where $E$ is epsilon closure, and useThis subset construction with epsilon transitions preserves the accepted formal language and gives a DFA with at most $2^{|Q|}$ states. The already proved direction of Kleene theorem therefore gives a regular expression for every NFA language.

For the converse, recursively construct an Epsilon-NFA with a designated initial state and final state for a regular expression. Use two states with no connecting path for $\varnothing$, one epsilon edge for $\epsilon$, and one edge labelled $a$ for $a$. Keep component state sets disjoint. Union uses a fresh initial state with epsilon edges into both components, and epsilon edges from their finals to a fresh final. Concatenation joins the first final to the second initial by an epsilon edge. For Kleene star, use fresh initial and final states, an epsilon edge directly between them for zero iterations, an edge into the old initial, and epsilon edges from the old final both back to the old initial and out to the new final. Each construction has exactly the intended union, concatenation, or iteration semantics. Induction on the regular expression proves correctness; the subset construction with epsilon transitions then gives a DFA. This proves both directions of Kleene theorem.

If $M$ halts on every input, simulate $M$ on input $n$ while counting its steps, and output that count when it halts. The resulting function $t_M(n)$ is a total computable function. Consequently yes: one may take the exact running time,This construction does not promise a simple closed expression or a bound of any particular complexity class; it uses the promised totality of this particular machine.

For a machine computing a partial computable function, its exact halting-time function is still a partial computable function, with the same domain. A finite bound cannot cover a genuinely infinite computation. Even restricting attention to inputs on which $M$ halts, a total computable function bounding all halting times need not exist. In fact the precise characterization is the computable bound on halting time criterion:For the forward implication, compute $f(n)$ and simulate $M(n)$ for that many steps. If it has not halted, the proposed bound ensures that it never will. This decides the domain. Conversely, first decide whether $n$ is in the domain; return zero outside it and the simulated halting time inside it. This defines a total computable function satisfying the bound. The time needed to compute the bound itself is irrelevant to this argument.

A universal halting recognizer has undecidable domain by the halting problem, so it has no such total bound. On the other hand, a machine that immediately halts on even inputs and loops on odd inputs computes a nontotal partial computable function but has a constant bound on its halting times. Thus nontotality alone does not decide whether a total bound exists.

A propositional type is a set $\Sigma$ of propositional formulas; a Boolean valuation realizes it if every member is true, and omits it if at least one member is false. A consistent propositional theory $T$ locally omits $\Sigma$ if every formula $\theta$ which implies all members of $\Sigma$ modulo $T$ is refutable modulo $T$. Equivalently, whenever $T\cup \{\theta \}$ is consistent, there is a $\sigma \in \Sigma$ for which $T\cup \{\theta ,\neg \sigma \}$ is consistent. For a consistent propositional type, this says that it is a nonprincipal propositional type.

The extended omitting types theorem for propositional logic says that if a consistent $T$ locally omits each of a countable family ${\Sigma }_0,{\Sigma }_1,\dots$, there is one Boolean valuation satisfying $T$ and omitting them all. It also works inside any prescribed finite condition consistent with $T$.

To prove it, start with such a condition ${\theta }_0$, taking $\top$ when none is prescribed. At stage $i$, choose ${\sigma }_i\in {\Sigma }_i$ such thatSuch a choice exists by local omission. More explicitly, failure would imply $T⊢{\theta }_i\to \sigma$ for every $\sigma \in {\Sigma }_i$, hence $T⊢\neg {\theta }_i$, contradicting the stage invariant. Every finite subset of $T\cup \{{\theta }_0\}\cup \{\neg {\sigma }_i:i\in \mathbb{N}\}$ lies inside a consistent stage. By the propositional compactness theorem and the completeness theorem for propositional logic, it has a Boolean valuation. That Boolean valuation satisfies $T$ and makes the selected member ${\sigma }_i$ of every type false. All types are therefore omitted simultaneously. No effective test for consistency is assumed, and the argument does not require the ambient propositional language to be countable. Only the family of omission requirements is countable.

Interpret the language of ordered rings in the standard natural numbers, with nonlogical symbols $0,1,+,\times ,<$. We give a single first-order formula $F(n,y)$ defining $y=n!$, rather than a separate expression with $n$ multiplication signs. The key is Gödel beta-function sequence coding. The remainder relationuses only the allowed symbols; all variables range over $\mathbb{N}$. With $c>0$, it assigns a unique remainder $r$ at each position $i$.

The factorial graph formula via remainder coding asserts that one code contains the initial value $1$, the final value $y$, and every recurrence step. Here is the fully expanded formula, with no remainder-function or factorial symbol:The first equation represents remainder $1$ at position zero: its omitted explicit remainder bound follows from $c>0$. The second line represents remainder $y$ at position $n$. The universally checked equations represent the adjacent remainders and impose multiplication by $i+1$. Uniqueness of remainders therefore forces them, successively, to be $0!,1!,\dots ,n!$, proving $F(n,y)\Rightarrow y=n!$ by mathematical induction. When $n=0$, the recurrence clause is empty and the two endpoint clauses force $y=1$.

Conversely, choose a positive $c$ larger than every value in the finite sequence $0!,1!,\dots ,n!$ and divisible by each positive integer at most $n$. The moduli $d_i=1+(i+1)c$, $0\le i\le n$, are pairwise coprime. Indeed, for $i<j$, a common divisor of $d_i,d_j$ divides $(j-i)c$ and is coprime to $c$, so divides $j-i$. Since $j-i$ divides $c$, the common divisor must be one. The Chinese remainder theorem gives a nonnegative $b$ with $b\equiv i!(\mathrm{mod}{d}_i)$ for every $i$. The chosen values are smaller than their moduli, so they are the actual remainders; the appropriate quotient witnesses then make $F(n,n!)$ true. ThusThe formula has fixed length, independent of $n$. For example, writing its displayed syntax in plain text with one-character variables, ordinary parentheses, and explicit logical connectives takes fewer than $1000$ characters and fewer than $500$ logical-symbol tokens. Its length is therefore $O(1)$ as a uniform definition of the graph. Numeral names for particular input values, if substituted for the variables, add their own encoding lengths. Over the ordered ring $\mathbb{Z}$, restrict every quantifier to nonnegative integers and require $n,y\ge 0$; this gives the same definition on its nonnegative part. It is the chosen arithmetic structure, not ring axioms alone, that makes the formula define factorial.

In the simply typed lambda calculus, types are generated from atomic types by the arrow constructor $A\to B$. A typed lambda term is a lambda term equipped with a derivation of a judgement $\Gamma ⊢t:A$, where the context assigns types to its free variables. The basic typing rules areThe Implicational Curry-Howard correspondence reads atomic types as propositions and $A\to B$ as logical implication. A typed variable is an assumption, abstraction is the implication introduction rule discharging that assumption, and application is the implication elimination rule. Consequently a typed lambda term is a proof in implicational Intuitionistic propositional logic, and a natural deduction proof recursively supplies such a term. For example, $\lambda x.x:A\to A$ expresses implication reflexivity. Products, sums, and the empty type extend the correspondence to conjunction, disjunction, and falsity; pure arrow types give precisely the implicational fragment. Beta reduction removes an introduction followed immediately by its elimination, matching proof simplification.

A Church numeral iswhere $f^{n}x$ means $n$ repetitions of application. At base type $A$, it has type $C_A=(A\to A)\to A\to A$. The following Church numeral arithmetic terms use left-associated application:Their concise conclusions areFor successor, the initial $f$ adds one application. For addition, the inner $nfx$ supplies $n$ applications and $mf$ supplies $m$ more. For multiplication, the repeated operation $nf$ applies $f$ $n$ times, and $m$ repetitions give $mn$. For exponentiation, $\overline{n}$ iterates the operation $\overline{m}$ on $f$: each iteration replaces a function $g$ by its $m$-fold iterate, yielding $f^{m^n}$. Zero iterations give $f$, so this encoding takes $m^0=1$, including $0^0=1$. The explicit outer $f,x$ abstractions make the result the standard Church numeral even at exponent zero, without needing eta equivalence.

Successor, addition, and multiplication operate on the same $C_A$. The displayed exponentiation term has type $C_A\to C_{A\to A}\to C_A$: its exponent iterates an operation on functions. Thus the numeral syntax admits several type instances; one should not force every occurrence into one fixed monomorphic Church type.

The Y combinator is the fixed-point combinatorFor $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, beta reduction gives $Yg{\to }_{\beta }{X}_g{\to }_{\beta }g{X}_g$. Since $X_g{\equiv }_{\beta }Yg$, we obtain $Yg{\equiv }_{\beta }g(Yg)$. This allows a recursive program body to receive a representation of itself.

Here the computation is in the untyped lambda calculus. The self-application $xx$ would require a simple type satisfying $A=A\to B$, impossible for finite simple types. Accordingly $Y$ is not a typed lambda term of the simply typed system. The Strong normalization theorem for simply typed lambda calculus also rules out a universal divergent fixed-point operator there.

To obtain a lambda representation of partial computable functions, encode machine configurations as finite data using Church numerals, Church pairs, and Church Booleans. Initial configuration, one transition, the halting test, and output extraction are primitive recursive functions, represented by lambda terms through the initial functions, composition, and lambda definition of primitive recursion by pair iteration. If these representations are $\mathsf{Init}$, $\mathsf{Next}$, $\mathsf{Halt}$, and $\mathsf{Out}$, defineUse normal-order beta reduction so the Church Boolean halting test selects one branch without evaluating the unused recursive branch. A halting computation follows finitely many transitions and returns the Church numeral of the output. A nonhalting computation forces successive tests forever and has no head normal form; by normal-order normalization theorem, it cannot be beta equivalent to a Church numeral. Thus every partial computable function is represented, with divergence preserved; every total computable function is the halting special case. This explains the role of $Y$ in computational universality while keeping the typed proof interpretation precise.

The equivalence classes of an equivalence relation are nonempty, pairwise disjoint, and partition $\mathbb{N}$. To construct a transversal of a set family for them, choose the least member of each class. Its set isEvery class has a least element by the well-ordering principle for the natural numbers, and that element satisfies the displayed condition. A nonleast element fails it because a smaller equivalent element exists. Therefore $S$ meets every class in exactly one point, not merely infinitely many classes.

The complement of $\sim$ is semidecidable, so for a given $n$ run the finitely many semidecision procedures for $m\nsim n$, $0\le m<n$, in parallel. Accept $n$ once all have accepted. If $n$ is a least representative, all finitely many computations halt; otherwise at least one never accepts. For $n=0$, the empty list of tests succeeds immediately. This proves that $S$ is semidecidable. Equivalently, enumerate inequivalent pairs and output $n$ once all pairs $(m,n)$ with $m<n$ have appeared, dovetailing the requirements over all $n$. This is the semidecidable least-representative transversal of a co-computably enumerable equivalence relation. Infinitely many classes make $S$ infinite, but that hypothesis is unnecessary for the existence and semidecidability of a complete transversal.

A well-quasi-ordering is a reflexive transitive relation such that every infinite sequence $x_0,x_1,\dots$ has $i<j$ with $x_i\le x_j$. An infinite sequence without such a pair is a bad sequence. For a finite rooted tree, let $u\wedge v$ denote the lowest common ancestor of two vertices. A homeomorphic embedding of a rooted tree into another is an injective map $h$ withThus it preserves branching and sends each edge to a nonempty downward path, with different branches separated. The source root may map to a vertex below the target root. Kruskal's tree theorem says that finite rooted trees are well-quasi-ordered under these embeddings.

We first establish the word lemma used in the proof. The Higman lemma says that finite words over a well-quasi-ordering $Q$ are well-quasi-ordered by subsequence embedding with increased letters. Every infinite sequence in $Q$ has an infinite nondecreasing subsequence. To see this, some term must have infinitely many later terms above it: otherwise, repeatedly choosing past all finitely many successors of earlier chosen terms constructs a bad sequence. Apply this observation again inside that infinite upper cone, and repeat.

If the Higman lemma failed, choose a minimal bad sequence of words $w_0,w_1,\dots$, minimizing length at each position among choices admitting a bad continuation. None is empty. Write $w_i=u_i{a}_i$, with last letter $a_i$, and choose indices $i_0<i_1<\cdots$ on which the $a_i$ are nondecreasing. Thenis still a bad sequence. A comparison from the original prefix into some $u_{i_j}$ would give one into $w_{i_j}$. A comparison $u_{i_j}\le u_{i_k}$ would extend by $a_{i_j}\le a_{i_k}$ to $w_{i_j}\le w_{i_k}$. Both contradict the original badness. But the replacement at position $i_0$ is shorter than $w_{i_0}$, contradicting minimality. This proves the Higman lemma.

Now suppose Kruskal's tree theorem fails and choose a minimal bad sequence $T_0,T_1,\dots$, minimizing the number of vertices at each stage. Let $\mathcal{B}$ contain all proper descendant-rooted subtrees of all $T_i$. We claim that $\mathcal{B}$ is well-quasi-ordered by rooted-tree homeomorphic embeddings. Otherwise take a bad sequence $U_0,U_1,\dots$ from it. Each finite set of host trees supplies only finitely many subtrees, so after passing to a subsequence we may arrange that $U_j$ is a proper subtree of $T_{k_j}$ with $k_0<k_1<\cdots$. The sequenceis bad: a comparison from a prefix tree into $U_j$ would compose with its inclusion into $T_{k_j}$ and contradict the original badness; comparisons among the $U_j$ are excluded by construction. Yet $U_0$ is smaller than $T_{k_0}$, contradicting minimality. This proves the claim.

List the immediate-child subtrees of each $T_i$ in any fixed order. These are finite words over $\mathcal{B}$. By the Higman lemma, some earlier child list embeds into a later one with increased letters. The selected child subtrees embed into distinct child branches of the later tree. Map the source root to the target root and use these embeddings in the selected branches. The paths from the target root to the embedded child roots are separated because the target child branches are distinct. The resulting injection preserves lowest common ancestors, giving $T_i⪯T_j$, a contradiction. This proves Kruskal's tree theorem completely. It also gives the root-preserving homeomorphic version: once the weaker relation is well-quasi-ordered on all finite rooted trees, apply the Higman lemma to their child lists to obtain a comparison preserving the root.

For the proposed adjacency-preserving rooted-tree embedding, the answer is no: it is not a well-quasi-ordering. For every $m\ge 1$, form $T_m$ from a stem of $m$ edges starting at the root and then attach two leaves to its terminal vertex. The only vertex with two children is at depth $m$. A root-preserving adjacency injection preserves depths: the unique path of length $d$ from the root maps to a simple path of length $d$ from the target root. The image of a vertex with two children must still have two distinct children. Thus an embedding $T_m\to T_n$ must send the branch vertex at depth $m$ to the unique branch vertex at depth $n$, forcing $m=n$. ThereforeThis is the branching-depth antichain of rooted trees. Homeomorphic embeddings can stretch the stem and hence do not have this obstruction.