Turing's Halting Theorem

 
 Editor
Salto, Francisco
 Incorporated contributions
Salto (12/2009)
 Usage domain
Logic, computability
 Type
theorem, concept
 French
Indecibilité de l'arrêt
 German Turings Unentscheidbarkeit

Contents

1. Basic idea
2. Concepts
3. Proofs


1. Basic idea

Many problems around us in ordinary life do not seem to have a computational solution. More interestingly, some precisely formulated theoretical and scientific problems are also seemingly insoluble in computational terms. By “computable” we shall understand here computable in its standard sense, that is, able to be solved by the finite, precise and recursive means of any Turing Machine.

However, it is indeed surprising and theoretically highly interesting that certain arithmetically formulated problems are insoluble by any standard computation. Imagine we introduce arbitrary finite sequences in a system under the following rules: (1) answer “yes” if the sequence codes a program which terminates, (2) answer “no” if it doesn't (does not codify a programm or does not terminate).This is Turing's Halting problem, for which he proofed the inexistence of any algorithmical decision procedure. The interest of this undecidability result lies in the purely logical reasons supporting it and exporting its uncomputability results to any procedure able to answer it. Moreover, Rice generalizes and extends Turing's results for any non-trivial property of partial functions.

It is important to notice that this and other limitative results from logic, such as incompleteness, do not teach us that we are able to proof results that are beyond any computer. We can, but this is not surprising, belief them.

2. Concepts

The general notion of computation is usually made precise by means of the concept of recursion. Church's Thesis states that all computable functions are recursive. Under this asumption, all computable funcions are definable in a fragment of the language of formal arithmetic, or, equivalently, by means of Turing's Machine Algorithms.

In this way, to each program or computation M corresponds a natural number n which is its code or index Mn. The result of introducing an input k in the machine M, gives as a result a sequence M(k). Since computation languages are themselves sequences, they apply to themselves, just as a calculation can be applied over its own code (Mm(m)). This is the source ot may fruitful applications and also of some crucial limitations of computability.

A set is recursively enumerable whenever it is definable in the language  RE of formal first order Arithmetic (basicly the standard language of formal arithmetic without negation and with  bounded cuantificación). Equivalently, we call a language recursively enumerable if it contains all finite sequences codifying a Turing machine and an input, so that the machine stops at that input. A set (or a problem, or a language) is recursive if and only if both itself and its complement are recursively enumerable.

For example, consider the problem TERMINATES, posing the task of  determining, given a program with code m and an input n for it, if the program terminates or not at n. The problem TERMINATES(m,n) is recursively enumerable, since there is a program accepting TERMINATES, that is, a program terminating whenever its input is in TERMINATES, and not doing it in any contrary case. A program computing TERMINATES terminates at some input n.

Let us now consider the complement NONTERMINATES of the problem TERMINATES. If there is a program for it, it will terminate if its input is in NONTERMINATES, and in any contrary case it won’t terminate. As we shall see, NONTERMINATES is not recursively enumerable, and hence  TERMINATES is not recursive.  This is, informally summarized, the course of the following argument.

3. Proofs

Enumeration Theorem. There is a dyadic relation T(x,y) which is recursively enumerable and recursively enumerates all recursive enumerable sets. That is, for any recursively anumerable set C there is a code e such that C={n:T(e,n)}.

Proof: Let Re be the set {x:T(e,x)}. Te is recursively enumerable, since both T and e are definable in the language RE. Now, C being by hypothesis also enumerable recursive, it is defined by a formula in a free variable x. Let e be the code or Gödel number of such formula. Hence,  C=Te.

Certain “diagonal” theorem. The diagonal relation is not computable (recursive).

Proof: Let K be the set {x:T(x,x)}. K is recursively enumerable, but its complement –K it's not. If it were, -K=Te for some e. But for all x, by the definition of complement, x belongs to –K if and only if x does not belong to Tx. In the particular case of e, we have e belongs to –K if and only if e does not belong to Te, that is, e does not belong to –K, which is a classical contradiction.

Halting Theorem. TERMINATES is not computable (recursive).

Proof: Suppose for reductio that the two argument function t (m,n) were computable being t(m,n)=1 or =0 depending on whether the machine m with n as input terminates or not. Under this assumption, the diagonal function t(n,n)=t’(n) is also computable, which is impossible by the previous diagonal theorem.
 
References
  • BOOLOS, G., BURGUESS, J. & JEFFREY, R. (2003). Computability and Logic. Cambridge: University Press.
  • COPELAND, J. (2009). The Turing Archive. [on line] http://www.alanturing.net/turing_archive/  [visited: 20/12/2009]
  • FITTING, M. (2000). Notes on Incompleteness and Undecidability. New York: CUNY.
  • KRIPKE, S. (1995). Elementary Recursion Theory and its applications to formal Systems. Princeton, MS.
  • PAPADIMITRIOU (1995). Computacional Complexity. Reading (Mass.): Addison Wesley.
  • SALTO, F. (2006). “Verdad y Recursividad”, in J. Méndez (ed.) Artículos de segunda Mano, Salamanca: Varona. pp. 51-156
  • SMULLYAN, R. (1994). Diagonalization and Self-reference. Oxford: Clarendon Press.
  • TURING, A. (1937). “Computability and l-Definability”. Journal of Symbolic Logic, 2, 153-163. 
Entries
New entry. Before doing a new entry, please, copy this line and the following ones and paste them at the column bottom. Next fill out the fields: 'name', 'date' and 'text', and delete this upper blue paragraph.
Name (date)
 
[Entry text]



Incorporated entries
Francisco Salto (12/2009)
 
[Entry directly edited by the author and editor of the article in the left column.]
Comments