Admissible numbering

Last updated

In computability theory, admissible numberings are enumerations (numberings) of the set of partial computable functions that can be converted to and from the standard numbering. These numberings are also called acceptable numberings and acceptable programming systems.

Contents

Rogers' equivalence theorem shows that all acceptable programming systems are equivalent to each other in the formal sense of numbering theory.

Definition

The formalization of computability theory by Kleene led to a particular universal partial computable function Ψ(e, x) defined using the T predicate. This function is universal in the sense that it is partial computable, and for any partial computable function f there is an e such that, for all x, f(x) = Ψ(e,x), where the equality means that either both sides are undefined or both are defined and are equal. It is common to write ψe(x) for Ψ(e,x); thus the sequence ψ0, ψ1, ... is an enumeration of all partial computable functions. Such enumerations are formally called computable numberings of the partial computable functions.

An arbitrary numbering η of partial functions is defined to be an admissible numbering if:

Here, the first bullet requires the numbering to be computable; the second requires that any index for the numbering η can be converted effectively to an index to the numbering ψ; and the third requires that any index for the numbering ψ can be effectively converted to an index for the numbering η.

Equivalent Definition

The following equivalent characterization of admissibility has the advantage of being "internal to η", in that it makes no direct reference to a standard numbering (only indirectly through the definition of Turing universality). A numbering η of partial functions is admissible in the above sense if and only if:

The proof is as follows:

The fact that admissible numberings in the above sense have all these properties follows from the fact that the standard numbering does, and Rogers's Equivalence Theorem
In the other direction, suppose η has the properties in the equivalent characterization.
Since the evaluation function H(e,x)=ηe(x) is partial computable, there exists v such that ψv=H. Thus, by the Parameter Theorem for the standard numbering, there is a total computable function d such that ψd(v,e)(x)=H(e,x) for all x. The total function f(e) = d(v,e) then satisfies the second part of the above definition.
Next, since the evaluation function E(e,x)=ψe(x) for the standard numbering is partial computable, by the assumption of Turing universality there exists u such that ηu(e,x)=ψe(x) for all e,x.
Let c(x,e) be the computable currying function for η. Then ηc(u,e)e for all e, so g(e) = c(u,e) satisfies the third part of the first definition above.

Rogers' equivalence theorem

Hartley Rogers, Jr. showed that a numbering η of the partial computable functions is admissible if and only if there is a total computable bijection p such that, for all e, ηe = ψp(e) (Soare 1987:25).

See also

Related Research Articles

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 program, nor false for every program.

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.

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 computability theory, a set of natural numbers is called computable, recursive, or decidable if there is an algorithm which takes a number as input, terminates after a finite amount of time and correctly decides whether the number belongs to the set or not.

In computer science and mathematical logic the Turing degree or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set.

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 . The concept can be analogously applied to function problems.

In computability theory the S m
n
 
theorem
, written also as "smn-theorem" or "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 a numbering is the assignment of natural numbers to a set of objects such as functions, rational numbers, graphs, or words in some formal language. A numbering can be used to transfer the idea of computability and related concepts, which are originally defined on the natural numbers using computable functions, to these different types of objects.

In computability theory, productive sets and creative sets are types of sets of natural numbers that have important applications in mathematical logic. They are a standard topic in mathematical logic textbooks such as Soare (1987) and Rogers (1987).

In computability theory, the UTM theorem, or universal Turing machine theorem, is a basic result about Gödel numberings of the set of computable functions. It affirms the existence of a computable universal function, which is capable of calculating any other computable function. The universal function is an abstract version of the universal Turing machine, thus the name of the theorem.

In computability theory, a function is called limit computable if it is the limit of a uniformly computable sequence of functions. The terms computable in the limit, limit recursive and recursively approximable are also used. One can think of limit computable functions as those admitting an eventually correct computable guessing procedure at their true value. A set is limit computable just when its characteristic function is limit computable.

In the mathematical discipline of set theory, there are many ways of describing specific countable ordinals. The smallest ones can be usefully and non-circularly expressed in terms of their Cantor normal forms. Beyond that, many ordinals of relevance to proof theory still have computable ordinal notations. However, it is not possible to decide effectively whether a given putative ordinal notation is a notation or not ; various more-concrete ways of defining ordinals that definitely have notations are available.

In recursion theory, α recursion theory is a generalisation of recursion theory to subsets of admissible ordinals . An admissible set is closed under functions, where denotes a rank of Godel's constructible hierarchy. is an admissible ordinal if is a model of Kripke–Platek set theory. In what follows is considered to be fixed.

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.

In constructive mathematics, Church's thesis is the principle stating that all total functions are computable functions.

In computability theory, index sets describe classes of computable functions; specifically, they give all indices of functions in a certain class, according to a fixed Gödel numbering of partial computable functions.

In computability theory, the halting problem is the problem of determining, from a description of an arbitrary computer program and an input, whether the program will finish running, or continue to run forever. The halting problem is undecidable, meaning that no general algorithm exists that solves the halting problem for all possible program–input pairs.

References