Kleene's T predicate

Last updated

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

Example call of T1. The 1st argument gives the source code (in C rather than as a Godel number e) of a computable function, viz. the Collatz function f. The 2nd argument gives the natural number i to which f is to be applied. The 3rd argument gives a sequence x of computation steps simulating the evaluation of f on i (as an equation chain rather than a Godel sequence number). The predicate call evaluates to true since x is actually the correct computation sequence for the call f(5), and ends with an expression not involving f anymore. Function U, applied to the sequence x, will return its final expression, viz. 1. KleeneT collatz5.gif
Example call of T1. The 1st argument gives the source code (in C rather than as a Gödel number e) of a computable function, viz. the Collatz function f. The 2nd argument gives the natural number i to which f is to be applied. The 3rd argument gives a sequence x of computation steps simulating the evaluation of f on i (as an equation chain rather than a Gödel sequence number). The predicate call evaluates to true since x is actually the correct computation sequence for the call f(5), and ends with an expression not involving f anymore. Function U, applied to the sequence x, will return its final expression, viz. 1.

The definition depends on a suitable Gödel numbering that assigns natural numbers to computable functions (given as Turing machines). 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 predicate is obtained by formalizing this simulation.

The ternary relation takes three natural numbers as arguments. is true if encodes a computation history of the computable function with index when run with input , and the program halts as the last step of this computation history. That is,

If all three of these questions have a positive answer, then is true, otherwise, it is false.

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

There is a corresponding primitive recursive function such that if is true then returns the output of the function with index on input .

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

is true if encodes a halting computation of the function with index on the inputs .

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

Normal form theorem

The predicates can be used to obtain Kleene's normal form theorem for computable functions (Soare 1987, p. 15; Kleene 1943, p. 5253). This states there exists a fixed primitive recursive function such that a function is computable if and only if there is a number such that for all one has

,

where μ is the μ operator ( is the smallest natural number for which is true) and is true if both sides are undefined or if both are defined and they are equal. By the theorem, the definition of every general recursive function f can be rewritten into a normal form such that the μ operator is used only once, viz. immediately below the topmost , which is independent of the computable function .

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

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

is a -complete (n+1)-ary predicate. Thus, once a representation of the Tn predicate is obtained in a theory of arithmetic, a representation of a -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 is complete then the set

is 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.

Related Research Articles

In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops. Primitive recursive functions form a strict subset of those general recursive functions that are also total functions.

In computability theory, Rice's theorem states that all non-trivial semantic properties of programs are undecidable. A semantic property is one about the program's behavior, unlike a syntactic property. A property is non-trivial if it is neither true for every partial computable function, nor false for every partial computable function.

In mathematical logic and computer science, a general recursive function, partial recursive function, or μ-recursive function is a partial function from natural numbers to natural numbers that is "computable" in an intuitive sense – as well as in a formal one. If the function is total, it is also called a total recursive function. In computability theory, it is shown that the μ-recursive functions are precisely the functions that can be computed by Turing machines. The μ-recursive functions are closely related to primitive recursive functions, and their inductive definition (below) builds upon that of the primitive recursive functions. However, not every total recursive function is a primitive recursive function—the most famous example is the Ackermann function.

In computability theory, Kleene's recursion theorems are a pair of fundamental results about the application of computable functions to their own descriptions. The theorems were first proved by Stephen Kleene in 1938 and appear in his 1952 book Introduction to Metamathematics. A related theorem, which constructs fixed points of a computable function, is known as Rogers's theorem and is due to Hartley Rogers, Jr.

Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since expanded to include the study of generalized computability and definability. In these areas, computability theory overlaps with proof theory and effective descriptive set theory.

<span class="mw-page-title-main">Arithmetical hierarchy</span> Hierarchy of complexity classes for formulas defining sets

In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy classifies certain sets based on the complexity of formulas that define them. Any set that receives a classification is called arithmetical.

In computability theory, a set S of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if:

In computational complexity theory, the polynomial hierarchy is a hierarchy of complexity classes that generalize the classes NP and co-NP. Each class in the hierarchy is contained within PSPACE. The hierarchy can be defined using oracle machines or alternating Turing machines. It is a resource-bounded counterpart to the arithmetical hierarchy and analytical hierarchy from mathematical logic. The union of the classes in the hierarchy is denoted PH.

In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the primitive recursive functions makes it possible to define all computable functions.

In mathematics and computer algebra, automatic differentiation, also called algorithmic differentiation, computational differentiation, is a set of techniques to evaluate the partial derivative of a function specified by a computer program.

Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithms, in the sense that a function is computable if there exists an algorithm that can do the job of the function, i.e. given an input of the function domain it can return the corresponding output. Computable functions are used to discuss computability without referring to any concrete model of computation such as Turing machines or register machines. Any definition, however, must make reference to some specific model of computation but all valid definitions yield the same class of functions. Particular models of computability that give rise to the set of computable functions are the Turing-computable functions and the general recursive functions.

In computability theory, a Turing reduction from a decision problem to a decision problem is an oracle machine which decides problem given an oracle for . It can be understood as an algorithm that could be used to solve if it had available to it a subroutine for solving B. The concept can be analogously applied to function problems.

In computability theory, a decider is a Turing machine that halts for every input. A decider is also called a total Turing machine as it represents a total function.

In computability theory, the Turing jump or Turing jump operator, named for Alan Turing, is an operation that assigns to each decision problem X a successively harder decision problem X with the property that X is not decidable by an oracle machine with an oracle for X.

In computability theory the S m
n
 
theorem
, is a basic result about programming languages. It was first proved by Stephen Cole Kleene (1943). The name S m
n
 
comes from the occurrence of an S with subscript n and superscript m in the original formulation of the theorem.

In computability theory, course-of-values recursion is a technique for defining number-theoretic functions by recursion. In a definition of a function f by course-of-values recursion, the value of f(n) is computed from the sequence .

Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

Algorithm characterizations are attempts to formalize the word algorithm. Algorithm does not have a generally accepted formal definition. Researchers are actively working on this problem. This article will present some of the "characterizations" of the notion of "algorithm" in more detail.

In mathematics, the effective topos introduced by Martin Hyland (1982) captures the mathematical idea of effectivity within the category theoretical framework.

In computability theory and computational complexity theory, enumeration reducibility is a method of reduction that determines if there is some effective procedure for determining enumerability between sets of natural numbers. An enumeration in the context of e-reducibility is a listing of the elements in a particular set, or collection of items, though not necessarily ordered or complete.

References