Past exam of the year 1 of the computer science course of the University of Oxford / 2005 / Calculus, linear algebra, discrete mathematics, logic and proof, and models of computation / 10

A Turing machine has a finite control, an unbounded tape divided into cells over a finite tape alphabet including a blank symbol, and a head that reads one cell at a time. For a deterministic Turing machine, the current state and scanned symbol determine the replacement symbol, a head move one cell left or right, and the next state. The input occupies finitely many cells initially; all other cells are blank. Distinguished halting states report acceptance or rejection.

A formal language is a decidable language if some Turing machine halts on every input string, accepting exactly the members and rejecting all nonmembers:Halting on the nonmembers is part of the requirement; a machine that merely runs forever on some nonmembers need not decide the formal language.

Cancel one unary symbol from each block at each round. Mark the first, middle and last delimiters by $L,C,E$, respectively; use $X$ for a cancelled symbol in the left block and $Y$ for one in the right block. These are extra tape symbols of the Turing machine, all distinct from $0,1$ and blank. No numerical counter is needed in the finite control.

Starting on the first zero, replace it by $L$, scan right through the first block of ones to replace the next zero by $C$, then scan right through the second block and replace its terminal zero by $E$. Move left to $C$. If the initial head is on a blank immediately before the first zero, first move right to that zero. The cancellation loop always starts with the head at $C$:

After $k$ completed rounds, the invariant isIt holds initially with $k=0$, and each completed round changes exactly one remaining $1$ in each block into the corresponding marker. This proves the cancellation count and preserves the locations of all delimiters.

For successful cleanup, the right block is entirely $Y$ symbols. From $C$, sweep right, erasing all $Y$ symbols and finally $E$, then move left across the erased blanks back to the still-present $C$. Erase $C$ and continue left, erasing each $X$, until reaching either the last surviving $1$ or $L$. Move one cell right and write the new terminal zero there. Move left through the surviving ones to $L$, replace $L$ by $0$, and halt. The remaining nonblank tape is exactlyFor example, $0111110110$ represents $m=5,n=2$ and becomes $01110$, representing three.

For zero-result cleanup, the head has reached $L$. Sweep right, erasing everything through $E$ while retaining $L$; after erasing $E$, move left across the blanks to $L$. Replace $L$ by $0$, write a second zero in the next cell, and halt. Thus if $m<n$ the machine returns $00$. If $m=n$, successful cleanup also leaves $00$. With this explicit choice of behaviour,Each sweep seeks a retained delimiter or an end marker a finite distance away. Each completed round removes one right-block $1$; after at most $n$ completed rounds either cleanup or left-block exhaustion occurs. The stated scans, writes and single-cell moves are implementable by finitely many states, so this is an implementation-level Turing machine construction. The output $00$ represents zero; a negative integer cannot be represented in the unsigned unary numeral system specified here.

The halting problem asks, given the encoding $⟨M,w⟩$ of a Turing machine and an input string, whether that machine eventually halts on that input. Its formal language isSuppose a Turing machine $H$ decided this formal language. Construct another Turing machine $D$ that, on an input encoding $⟨M⟩$, runs $H$ on $⟨M,⟨M⟩⟩$. If $H$ answers that $M$ halts on its own encoding, $D$ enters an infinite loop. If $H$ answers that $M$ does not halt, $D$ halts. Handling malformed encodings by immediate rejection makes $D$ well-defined on arbitrary strings.

Now run $D$ on its own encoding. If $H$ says that $D$ halts, the construction makes $D$ loop; if $H$ says that $D$ does not halt, the construction makes $D$ halt. Either answer contradicts the assumed correctness of $H$. ThereforeThe contradiction concerns a decider that must give a correct terminating answer for every encoded machine and input. Simulating $M$ does detect a halt when one occurs, but cannot in general certify that a running computation will continue forever.