Kleene's T predicate

Kleene's T predicate

In computability theory, the T predicate, first studied by mathematician Stephen Cole Kleene, is a particular set of triples of natural numbers that is used to represent computable functions within formal theories of arithmetic. Informally, the T predicate tells whether a particular computer program will halt when run with a particular input, and the corresponding U function is used to obtain the results of the computation if the program does halt. As with the smn theorem, the original notation used by Kleene has become standard terminology for the concept.[1]

Contents

Definition

The definition depends on a suitable Gödel numbering that assigns natural numbers to computable functions. This numbering must be sufficiently effective that, given an index of a computable function and an input to the function, it is possible to effectively simulate the computation of the function on that input. The T predicate is obtained by formalizing this simulation.

The ternary relation T1(e,i,x) takes three natural numbers as arguments. The triples of numbers (e,i,x) that belong to the relation (the ones for which T1(e,i,x) is true) are defined to be exactly the triples in which x encodes a computation history of the computable function with index e when run with input i, and the program halts as the last step of this computation history. That is, T1 first asks whether x is the Gödel number of a finite sequence 〈xj〉 of complete configurations of the Turing machine with index e, running a computation on input i. If so, T1 then asks if this sequence begins with the starting state of the computation and each successive element of the sequence corresponds to a single step of the Turing machine. If it does, T1 finally asks whether the sequence 〈xj〉 ends with the machine in a halting state. If all three of these questions have a positive answer, then T1(e,i,x) holds (is true). Otherwise, T1(e,i,x) does not hold (is false).

There is a corresponding function U such that if T(e,i,x) holds then U(x) returns the output of the function with index e on input i.

Because Kleene's formalism attaches a number of inputs to each function, the predicate T1 can only be used for functions that take one input. There are additional predicates for functions with multiple inputs; the relation

T_k(e, i_1, \ldots, i_k, x),

holds if x encodes a halting computation of the function with index e on the inputs i1,...,ik.

Normal form theorem

The T predicate can be used to obtain Kleene's normal form theorem for computable functions (Soare 1987, p. 15). This states that a function f(n) is computable if and only if there is an e such that for all n,

f(n) \simeq U( \mu x\, T(e,n,x)),

where μ is the μ operator and \simeq holds if both sides are undefined or if both are defined and they are equal.

Formalization

The T predicate is primitive recursive in the sense that there is a primitive recursive function that, given inputs for the predicate, correctly determine the truth value of the predicate on those inputs. Similarly, the U function is primitive recursive.

Because of this, any theory of arithmetic that is able to represent every primitive recursive function is able to represent T and U. Examples of such arithmetical theories include Robinson arithmetic and stronger theories such as Peano arithmetic.

Arithmetical hierarchy

In addition to encoding computability, the T predicate can be used to generate complete sets in the arithmetical hierarchy. In particular, the set

K = { e : ∃ x T(e,0,x)},

which is of the same Turing degree as the halting problem, is a \Sigma^0_1 complete unary relation (Soare 1987, pp. 28, 41). More generally, the set

K_{n+1} = \{ \langle e, a_1, \ldots, a_n\rangle : \exists x T(e, a_1, \ldots, a_n, x)\}

is a \Sigma^0_1 complete (n+1)-ary predicate. Thus, once a representation of the T predicate is obtained in a theory of arithmetic, a representation of a \Sigma^0_1-complete predicate can be obtained from it.

This construction can be extended higher in the arithmetical hierarchy, as in Post's theorem (compare Hinman 2005, p. 397). For example, if a set A \subseteq \mathbb{N}^{k+1} is \Sigma^0_{n} complete then the set

\{ \langle a_1, \ldots, a_k\rangle : \forall x ( \langle a_1, \ldots, a_k, x) \in A)\}

is \Pi^0_{n+1} complete.

Notes

  1. ^ The predicate described here was presented in (Kleene 1943) and (Kleene 1952), and this is what is usually called "Kleene's T predicate". (Kleene 1967) uses the letter T to describe a different predicate related to computable functions, but which cannot be used to obtain Kleene's normal form theorem.

References

  • Peter Hinman, 2005, Fundamentals of Mathematical Logic, A K Peters. ISBN 978-1-56881-262-5
  • Stephen Cole Kleene, 1943, "Recursive predicates and quantifiers", Transactions of the AMS v. 53 n. 1, pp. 41–73. Reprinted in The Undecidable, Martin Davis, ed., 1965, pp. 255–287.
  • —, 1952, Introduction to Metamathematics, North-Holland. Reprinted by Ishi press, 2009, ISBN 0-923891-57-9.
  • —, 1967. Mathematical Logic, John Wiley. Reprinted by Dover, 2001, ISBN 0-486425-33-9.
  • Robert I. Soare, 1987, Recursively enumerable sets and degrees, Perspectives in Mathematical Logic, Springer. ISBN 0-387-15299-7

Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Monadic predicate calculus — In logic, the monadic predicate calculus is the fragment of predicate calculus in which all predicate letters are monadic (that is, they take only one argument), and there are no function letters. All atomic formulae have the form P(x), where P… …   Wikipedia

  • Halting problem — In computability theory, the halting problem can be stated as follows: Given a description of a computer program, decide whether the program finishes running or continues to run forever. This is equivalent to the problem of deciding, given a… …   Wikipedia

  • List of mathematics articles (K) — NOTOC K K approximation of k hitting set K ary tree K core K edge connected graph K equivalence K factor error K finite K function K homology K means algorithm K medoids K minimum spanning tree K Poincaré algebra K Poincaré group K set (geometry) …   Wikipedia

  • Craig's theorem — In mathematical logic, Craig s theorem states that any recursively enumerable set of well formed formulas of a first order language is (primitively) recursively axiomatizable. This result is not related to the well known Craig interpolation… …   Wikipedia

  • Μ-recursive function — In mathematical logic and computer science, the μ recursive functions are a class of partial functions from natural numbers to natural numbers which are computable in an intuitive sense. In fact, in computability theory it is shown that the μ… …   Wikipedia

  • μ operator — In computability theory, the μ operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Contents 1 Definition 2 Properties 3 Examples …   Wikipedia

  • Logicism — is one of the schools of thought in the philosophy of mathematics, putting forth the theory that mathematics is an extension of logic and therefore some or all mathematics is reducible to logic.[1] Bertrand Russell and Alfred North Whitehead… …   Wikipedia

  • Church–Turing thesis — Church s thesis redirects here. For the constructive mathematics assertion, see Church s thesis (constructive mathematics). In computability theory, the Church–Turing thesis (also known as the Church–Turing conjecture, Church s thesis, Church s… …   Wikipedia

  • Function (mathematics) — f(x) redirects here. For the band, see f(x) (band). Graph of example function, In mathematics, a function associates one quantity, the a …   Wikipedia

  • Principia Mathematica — For Isaac Newton s book containing basic laws of physics, see Philosophiæ Naturalis Principia Mathematica. The title page of the shortened version of the Principia Mathematica to *56. The Principia Mathematica is a three volume work on the… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”