Kleene's recursion theorem
Encyclopedia
In computability theory
Computability theory
Computability theory, also called recursion theory, is a branch of mathematical logic that originated in the 1930s with the study of computable functions and Turing degrees. The field has grown to include the study of generalized computability and definability...

, Kleene's recursion theorems are a pair of fundamental results about the application of computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...

s to their own descriptions. The theorems were first proved by Stephen Kleene
Stephen Cole Kleene
Stephen Cole Kleene was an American mathematician who helped lay the foundations for theoretical computer science...

 in 1938.

The two recursion theorems can be applied to construct fixed points
Fixed point (mathematics)
In mathematics, a fixed point of a function is a point that is mapped to itself by the function. A set of fixed points is sometimes called a fixed set...

 of certain operations on computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...

s, to generate quines, and to construct functions defined via recursive definition
Recursive definition
In mathematical logic and computer science, a recursive definition is used to define an object in terms of itself ....

s.

The second recursion theorem

The second recursion theorem is closely related to definitions of computable functions using recursion
Recursion
Recursion is the process of repeating items in a self-similar way. For instance, when the surfaces of two mirrors are exactly parallel with each other the nested images that occur are a form of infinite recursion. The term has a variety of meanings specific to a variety of disciplines ranging from...

. Because it is better known than the first recursion theorem, it is sometimes called just the recursion theorem. Its statement refers to the standard Gödel numbering φ of the partial recursive functions, in which the function corresponding to index e is .
The second recursion theorem. If F is a total computable function
Computable function
Computable functions are the basic objects of study in computability theory. Computable functions are the formalized analogue of the intuitive notion of algorithm. They are used to discuss computability without referring to any concrete model of computation such as Turing machines or register...

 then there is an index e such that .


Here means that, for each n, either both and are defined, and their values are equal, or else both are undefined.

Example

Suppose that g and h are total computable functions that are used in a recursive definition for a function f:



This recursive definition can be converted into a computable function F(e) that takes an index for a program e and returns an index F(e) such that



In this context, a fixed point of F is an index e such that ; the function computed by such an e will be a solution to the original recursion equations. The recursion theorem establishes the existence of such a fixed point, assuming that F is computable, and is sometimes called (Kleene's) fixed point theorem for this reason. The theorem does not guarantee that e is an index for the smallest fixed point of the recursion equations; this is the role of the first recursion theorem described below.

Proof of the second recursion theorem

The proof uses a particular total computable function h, defined as follows. Given a natural number x, h outputs the index of the partial computable function that performs the following computation:
Given an input y, first attempt to compute . If that computation returns an output e, then compute and return its value, if any.

Thus, for all x, if halts, then , and if does not halt then does not halt; this is denoted . The function h can be constructed from the partial computable function and the s-m-n theorem
S-m-n theorem
In computability theory the smn theorem, is a basic result about programming languages...

: for each x, is the index of a program which computes the function .

To complete the proof, let F be any total computable function, and construct h as above. Let e be an index of the composition , which is a total computable function. Then by the definition of h.
But, because e is an index of , , and thus . By the transitivity of , this means . Hence for .

Application to quines

One informal interpretation of the second recursion theorem is that any partial computable function can guess an index for itself. This follows from the following corollary of the theorem (Cutland 1980: p. 202).
Corollary. For any partial recursive function Q(x,y) there is an index p such that .


The corollary is proved by letting be a function that gives an index for .

The corollary shows that for any computable function Q of two arguments there is a program that takes one argument and evaluates Q with the index of that very program as the first argument and the given argument as the second. Note that this program is able to generate its index from information built in to the program; it does not require any external resources in order to find the index.

A classic example is the function Q(x,y) = x. The corresponding index p in this case yields a computable function that outputs its own index when applied to any value (Cutland 1980: p. 204). When expressed as computer programs, such indices are known as quines.

The following example in Lisp
Lisp programming language
Lisp is a family of computer programming languages with a long history and a distinctive, fully parenthesized syntax. Originally specified in 1958, Lisp is the second-oldest high-level programming language in widespread use today; only Fortran is older...

 illustrates how the p in the corollary can be effectively produced from the function Q. The function s11 in the code is the function of that name produced by the S-m-n theorem
S-m-n theorem
In computability theory the smn theorem, is a basic result about programming languages...

.


Q can be changed to any two-argument function.
(setq Q '(lambda (x y) x))
(setq s11 '(lambda (f x) (list 'lambda '(y) (list f x 'y))))
(setq n (list 'lambda '(x y) (list Q (list s11 'x 'x) 'y)))
(setq p (eval (list s11 n n)))

The results of the following expressions should be the same.
φ_p(nil)
(eval (list p nil))

Q(p, nil)
(eval (list Q p nil))

Fixed-point free functions

A function F such that for all e is called fixed point free. The recursion theorem shows that no computable function is fixed point free, but there are many non-computable fixed-point free functions. Arslanov's completeness criterion states that the only recursively enumerable Turing degree
Turing degree
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...

 that computes a fixed point free function is 0′, the degree of the halting problem.

The first recursion theorem

The first recursion theorem is related to fixed points determined by enumeration operators, which are a computable analogue of inductive definitions. An enumeration operator is a set of pairs (A,n) where A is a (code
Gödel number
In mathematical logic, a Gödel numbering is a function that assigns to each symbol and well-formed formula of some formal language a unique natural number, called its Gödel number. The concept was famously used by Kurt Gödel for the proof of his incompleteness theorems...

 for a) finite set of numbers and n is a single natural number. Often, n will be viewed as a code for an ordered pair of natural numbers, particularly when functions are defined via enumeration operators. Enumeration operators are of central importance in the study of enumeration reducibility.

Each enumeration operator Φ determines a function from sets of naturals to sets of naturals given by
A recursive operator is an enumeration operator that, when given the graph of a partial recursive function, always returns the graph of a partial recursive function.

A fixed point of an enumeration operator Φ is a set F such that Φ(F) = F. The first enumeration theorem shows that fixed points can be effectively obtained if the enumeration operator itself is computable.
First recursion theorem. The following statements hold.
  1. For any computable enumeration operator Φ there is a recursively enumerable set F such that Φ(F) = F and F is the smallest set with this property.
  2. For any recursive operator Ψ there is a partial computable function φ such that Ψ(φ) = φ and φ is the smallest partial computable function with this property.

Example

Like the second recursion theorem, the first recursion theorem can be used to obtain functions satisfying systems of recursion equations. To apply the first recursion theorem, the recursion equations must first be recast as a recursive operator.

Consider the recursion equations for the factorial
Factorial
In mathematics, the factorial of a non-negative integer n, denoted by n!, is the product of all positive integers less than or equal to n...

 function f:
f(0) = 1,
f(n+1) = (n + 1) · f(n).

The corresponding recursive operator Φ will have information that tells how to get to the next value of f from the previous value. However, the recursive operator will actually define the graph of f. First, Φ will contain the pair . This indicates that f(0) is unequivocally 1, and thus the pair (0,1) is in the graph of f.

Next, for each n and m, Φ will contain the pair . This indicates that, if f(n) is m, then f(n + 1) is (n + 1)m, so that the pair (n + 1, (n + 1)m) is in the graph of f. Unlike the base case f(0) = 1, the recursive operator requires some information about f(n) before it defines a value of f(n + 1).

The first recursion theorem (in particular, part 1) states that there is a set F such that Φ(F) = F. The set F will consist entirely of ordered pairs of natural numbers, and will be the graph of the factorial function f, as desired.

The restriction to recursion equations that can be recast as recursive operators ensures that the recursion equations actually define a least fixed point. For example, consider the set of recursion equations:
g(0) = 1,
g(n + 1) = 1,
g(2n) = 0.

There is no function g satisfying these equations, because they imply g(2) = 2 and also imply g(2) = 0. Thus there is no fixed point g satisfying these recursion equations. It is possible to make an enumeration operator corresponding to these equations, but it will not be a recursive operator.

Proof sketch for the first recursion theorem

The proof of part 1 of the first recursion theorem is obtained by iterating the enumeration operator Φ beginning with the empty set. First, a sequence Fk is constructed, for . Let F0 be the empty set. Proceeding inductively, for each k, let Fk + 1 be . Finally, F is taken to be . The remainder of the proof consists of a verification that F is recursively enumerable and is the least fixed point of Φ. The sequence Fk used in this proof corresponds to the Kleene chain in the proof of the Kleene fixed-point theorem.

The second part of the first recursion theorem follows from the first part. The assumption that Φ is a recursive operator is used to show that the fixed point of Φ is the graph of a partial function. The key point is that if the fixed point F is not the graph of a function, then there is some k such that Fk is not the graph of a function.

Comparison to the second recursion theorem

Compared to the second recursion theorem, the first recursion theorem produces a stronger conclusion but only when narrower hypotheses are satisfied. Rogers [1967] uses the term weak recursion theorem for the first recursion theorem and strong recursion theorem for the second recursion theorem.

One difference between the first and second recursion theorems is that the fixed points obtained by the first recursion theorem are guaranteed to be least fixed points, while those obtained from the second recursion theorem may not be least fixed points.

A second difference is that the first recursion theorem only applies to systems of equations that can be recast as recursive operators. This restriction is similar to the restriction to continuous operators in the Kleene fixed-point theorem of order theory
Order theory
Order theory is a branch of mathematics which investigates our intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article introduces the field and gives some basic definitions...

. The second recursion theorem can be applied to any total recursive function.

Generalized theorem by A.I. Maltsev

Anatoly Maltsev
Anatoly Maltsev
Anatoly Ivanovich Maltsev was born in Misheronsky, near Moscow, and died in Novosibirsk, USSR. He was a mathematician noted for his work on the decidability of various algebraic groups...

 proved a generalized version of the recursion theorem for any set with a precomplete numbering. A Gödel numbering is a precomplete numbering on the set of computable functions so the generalized theorem yields the Kleene recursion theorem as a special case.

Given a precomplete numbering then for any partial computable function with two parameters there exists a total computable function with one parameter such that

See also

  • Denotational semantics
    Denotational semantics
    In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...

    , where another least fixed point theorem is used for the same purpose as the first recursion theorem.
  • Fixed-point combinators, which are used in lambda calculus
    Lambda calculus
    In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...

    for the same purpose as the first recursion theorem.
The source of this article is wikipedia, the free encyclopedia.  The text of this article is licensed under the GFDL.
 
x
OK