1
$\begingroup$

I (think I) understand the enumeration and then diagonalization proof of the undecidability of the halting problem, but I came cross this proof in SICP below, which does not seem to require the enumeration. Did I miss anything?

(define (run-forever) (run-forever))

(define (try p)
  (if (halts? p p)
      (run-forever)
      'halted))

I suspect this has to do with how a TM is encoded, i.e. the parameter for try. Being able to encode a TM might require enumeration? But I'm still very confused.

$\endgroup$
1
$\begingroup$

No, being able to enumerate Turing machines is not directly relevant.

Let us consider some abstract notion of algorithm. The ingredients for the undecidability are as follows:

  1. The Halting problem makes sense. This means that

    a) Algorithms can "halt" on some inputs, and fail to "halt" on others. Halting allows the algorithm to output something, eg "Yes" and "No".

    b) Algorithms can take algorithms as input.

  2. Algorithms allow if-then-else branching

  3. There is an algorithm that takes an algorithm as input, and simulates how the input-algorithm would act.

The code snippet in the question is essentially how you do it, and the criteria above are essentially saying "this code snippet is valid pseudoc-code for our abstract notion of algorithm".

To see that the fact that TMs can be enumerated really does not factor in, one can look at models of computation such as the BSS-machines. These can have arbitary real numbers as parameters in the code, so there are uncountably many machines. However, they still meet all criteria above, and thus the standard argument shows that BSS-machines cannot decide the BSS-Halting problem.

$\endgroup$
  • $\begingroup$ So if the word "diagonalization" is used in a narrowly Cantorian sense, meaning to flip the diagonal of a natural number enumeration, is it fair to say that the idea of flipping the result of a self reference is somewhat more fundamental than the idea of diagonalization? $\endgroup$ – wlnirvana Jun 23 '18 at 10:48
  • $\begingroup$ @winirvana The classic Cantor diagonalization yields that there is no surjection from a set $X$ to its powerset $2^X$ - again, no need for enumeration of anything. As a trivial (in terms of proof, not of language to express it) we would have the Lawvere fixed point theorem, which one could deem to be the "true meaning of diagonalization". Since the generic proof of undecidability of the Halting problem is not an instance of Lawvere fixed point theorem, one could indeed make an argument towards to your conclusion. $\endgroup$ – Arno Jun 23 '18 at 11:01
0
$\begingroup$

Yes, but it's been proven that Turing machines are enumerable.

All proofs of the Halting Problem depend on the ability for one Turing machine to simulate another. This requires the ability to encode a Turing machine into a string in the tape language of another Turing machine. And since strings are proven to be enumerable, if Turing machines aren't enumerable, then they can't be losslessly converted into strings in this way (since it would provide an enumeration).

However, formally speaking, a Turing machine is simply a 7-tuple of sets, symbols, and functions. All of these are enumerable, and tuples of enumerable types are enumerable. Therefore Turing machines are enumerable.

This is generally considered a good thing, because it means that the encoding into strings is possible, which means we can have universal Turing machines, which means we can have Turing completeness.

$\endgroup$
  • $\begingroup$ But how does this relate to the Scheme example? Is it the idea that code is data and data is code? $\endgroup$ – wlnirvana Jun 23 '18 at 3:54
  • $\begingroup$ I think what is needed is the ability to simulate many Turing machines, and the ability of the Turing machine that does the simulating to be simulated as well. $\endgroup$ – gnasher729 Jun 23 '18 at 11:34

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.