Kleene's Recursion Theorem
   HOME

TheInfoList



OR:

In
computability theory 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 e ...
, Kleene's recursion theorems are a pair of fundamental results about the application of
computable function 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 ...
s to their own descriptions. The theorems were first proved by
Stephen Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
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. Hartley Rogers Jr. (July 6, 1926 – July 17, 2015) was a mathematician who worked in computability theory, and was a professor in the Mathematics Department of the Massachusetts Institute of Technology. Biography Born in 1926 in Buffalo, New York ...
The recursion theorems can be applied to construct fixed points of certain operations on
computable function 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 ...
s, to generate quines, and to construct functions defined via
recursive definition In mathematics and computer science, a recursive definition, or inductive definition, is used to define the elements in a set in terms of other elements in the set ( Aczel 1977:740ff). Some examples of recursively-definable objects include facto ...
s.


Notation

The statement of the theorems refers to an
admissible numbering In computability theory, admissible numberings are enumerations (Numbering (computability theory), numberings) of the set of partial computable functions that can be converted ''to and from'' the standard numbering. These numberings are also called ...
\varphi of the
partial recursive 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 i ...
s, such that the function corresponding to index e is \varphi_e. If F and G are
partial function In mathematics, a partial function from a set to a set is a function from a subset of (possibly itself) to . The subset , that is, the domain of viewed as a function, is called the domain of definition of . If equals , that is, if is de ...
s on the natural numbers, the notation F \simeq G indicates that, for each ''n'', either F(n) and G(n) are both defined and are equal, or else F(n) and G(n) are both undefined.


Rogers's fixed-point theorem

Given a function F, a fixed point of F is an index e such that \varphi_e \simeq \varphi_. Rogers describes the following result as "a simpler version" of Kleene's (second) recursion theorem.


Proof of the fixed-point theorem

The proof uses a particular total computable function h, defined as follows. Given a natural number x, the function h outputs the index of the partial computable function that performs the following computation: :Given an input y, first attempt to compute \varphi_(x). If that computation returns an output e, then compute \varphi_e(y) and return its value, if any. Thus, for all indices x of partial computable functions, if \varphi_x(x) is defined, then \varphi_ \simeq \varphi_. If \varphi_x(x) is not defined, then \varphi_ is a function that is nowhere defined. The function h can be constructed from the partial computable function g(x,y) described above and the s-m-n theorem: for each x, h(x) is the index of a program which computes the function y \mapsto g(x,y). To complete the proof, let F be any total computable function, and construct h as above. Let e be an index of the composition F \circ h, which is a total computable function. Then \varphi_ \simeq \varphi_ by the definition of h. But, because e is an index of F \circ h, \varphi_e(e) = (F \circ h)(e), and thus \varphi_ \simeq \varphi_. By the transitivity of \simeq, this means \varphi_ \simeq \varphi_. Hence \varphi_n \simeq \varphi_ for n = h(e). This proof is a construction of a
partial recursive 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 i ...
which implements the
Y combinator Y Combinator (YC) is an American technology startup accelerator launched in March 2005. It has been used to launch more than 3,000 companies, including Airbnb, Coinbase, Cruise, DoorDash, Dropbox, Instacart, Quora, PagerDuty, Reddit, St ...
.


Fixed-point-free functions

A function F such that \varphi_e \not \simeq \varphi_ for all e is called fixed-point free. The fixed-point theorem shows that no total 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 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: *There is an algorithm such that the ...
Turing degree In computer science and mathematical logic the Turing degree (named after Alan Turing) or degree of unsolvability of a set of natural numbers measures the level of algorithmic unsolvability of the set. Overview The concept of Turing degree is fund ...
that computes a fixed-point-free function is 0′, the degree of the
halting problem 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. Alan Turing proved in 1936 that a g ...
.


Kleene's second recursion theorem

The second recursion theorem is a generalization of Rogers's theorem with a second input in the function. One informal interpretation of the second recursion theorem is that it is possible to construct self-referential programs; see "Application to quines" below. :The second recursion theorem. For any partial recursive function Q(x,y) there is an index p such that \varphi_p \simeq \lambda y.Q(p,y). The theorem can be proved from Rogers's theorem by letting F(p) be a function such that \varphi_(y) = Q(p,y) (a construction described by the S-m-n theorem). One can then verify that a fixed-point of this F is an index p as required. The theorem is constructive in the sense that a fixed computable function maps an index for ''Q'' into the index ''p''.


Comparison to Rogers's theorem

Kleene's second recursion theorem and Rogers's theorem can both be proved, rather simply, from each other. However, a direct proof of Kleene's theorem does not make use of a universal program, which means that the theorem holds for certain subrecursive programming systems that do not have a universal program.


Application to quines

A classic example using the second recursion theorem 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. When expressed as computer programs, such indices are known as quines. The following example in
Lisp A lisp is a speech impairment in which a person misarticulates sibilants (, , , , , , , ). These misarticulations often result in unclear speech. Types * A frontal lisp occurs when the tongue is placed anterior to the target. Interdental lisping ...
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. 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. \varphi p(nil) (eval (list p nil)) Q(p, nil) (eval (list Q p nil))


Application to elimination of recursion

Suppose that g and h are total computable functions that are used in a recursive definition for a function f: :f(0,y) \simeq g(y), :f(x+1,y) \simeq h(f(x,y),x,y), The second recursion theorem can be used to show that such equations define a computable function, where the notion of computability does not have to allow, prima facie, for recursive definitions (for example, it may be defined by μ-recursion, or by
Turing machine A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
s). This recursive definition can be converted into a computable function \varphi_(e,x,y) that assumes e is an index to itself, to simulate recursion: :\varphi_(e,0,y) \simeq g(y), :\varphi_(e,x+1,y) \simeq h(\varphi_e(x,y),x,y). The recursion theorem establishes the existence of a computable function \varphi_f such that \varphi_f(x,y) \simeq \varphi_(f,x,y). Thus f satisfies the given recursive definition.


Reflexive programming

Reflexive, or
reflective Reflection is the change in direction of a wavefront at an interface between two different media so that the wavefront returns into the medium from which it originated. Common examples include the reflection of light, sound and water waves. The ' ...
, programming refers to the usage of self-reference in programs. Jones presents a view of the second recursion theorem based on a reflexive language. It is shown that the reflexive language defined is not stronger than a language without reflection (because an interpreter for the reflexive language can be implemented without using reflection); then, it is shown that the recursion theorem is almost trivial in the reflexive language.


The first recursion theorem

While the second recursion theorem is about fixed points of computable functions, 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 In communications and information processing, code is a system of rules to convert information—such as a letter, word, sound, image, or gesture—into another form, sometimes shortened or secret, for communication through a communication ...
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 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 ...
. Each enumeration operator Φ determines a function from sets of naturals to sets of naturals given by :\Phi(X) = \. 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. :# 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. :# 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 In mathematics, the factorial of a non-negative denoted is the product of all positive integers less than or equal The factorial also equals the product of n with the next smaller factorial: \begin n! &= n \times (n-1) \times (n-2) \t ...
function ''f'': \begin &f(0) = 1 \\ &f(n+1) = (n + 1) \cdot f(n) \end 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 ( \varnothing, (0, 1)). 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 ( \, (n+1, (n+1)\cdot m)). This indicates that, if ''f''(''n'') is ''m'', then is , so that the pair is in the graph of ''f''. Unlike the base case , the recursive operator requires some information about ''f''(''n'') before it defines a value of . The first recursion theorem (in particular, part 1) states that there is a set ''F'' such that . 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: \begin &g(0) = 1\\ &g(n + 1) = 1\\ &g(2n) = 0 \end There is no function ''g'' satisfying these equations, because they imply ''g''(2) = 1 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 ''F''''k'' is constructed, for k = 0, 1, \ldots. Let ''F''0 be the empty set. Proceeding inductively, for each ''k'', let ''F''''k'' + 1 be F_k \cup \Phi(F_k). Finally, ''F'' is taken to be \bigcup F_k. The remainder of the proof consists of a verification that ''F'' is recursively enumerable and is the least fixed point of Φ. The sequence ''F''''k'' used in this proof corresponds to the Kleene chain in the proof of the
Kleene fixed-point theorem In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following: :Kleene Fixed-Point Theorem. Suppose (L, \sqsubseteq) is a directed-complete pa ...
. 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 ''F''''k'' 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 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 In the mathematical areas of order and lattice theory, the Kleene fixed-point theorem, named after American mathematician Stephen Cole Kleene, states the following: :Kleene Fixed-Point Theorem. Suppose (L, \sqsubseteq) is a directed-complete pa ...
of
order theory Order theory is a branch of mathematics that investigates the 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 intr ...
. The second recursion theorem can be applied to any total recursive function.


Generalized theorem

In the context of his theory of numberings, Ershov showed that Kleene's recursion theorem holds for any
precomplete numbering In computability theory complete numberings are generalizations of Gödel numbering first introduced by A.I. Mal'tsev in 1963. They are studied because several important results like the Kleene's recursion theorem and Rice's theorem, which were o ...
. 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.See for a survey in English. Given a precomplete numbering \nu, then for any partial computable function f with two parameters there exists a total computable function t with one parameter such that :\forall n \in \mathbb : \nu \circ f(n,t(n)) = \nu \circ t(n).


See also

*
Denotational semantics In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called ''denotations'' ...
, where another least fixed point theorem is used for the same purpose as the first recursion theorem. *
Fixed-point combinator In mathematics and computer science in general, a '' fixed point'' of a function is a value that is mapped to itself by the function. In combinatory logic for computer science, a fixed-point combinator (or fixpoint combinator) is a higher-order ...
s, which are used in
lambda calculus Lambda calculus (also written as ''λ''-calculus) is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation ...
for the same purpose as the first recursion theorem. *
Diagonal lemma In mathematical logic, the diagonal lemma (also known as diagonalization lemma, self-reference lemma or fixed point theorem) establishes the existence of self-referential sentences in certain formal theories of the natural numbers—specificall ...
a closely related result in mathematical logic


References

* * * * Footnotes


Further reading

*


External links

* {{SEP, recursive-functions, Recursive Functions,
Piergiorgio Odifreddi Piergiorgio Odifreddi (born 13 July 1950, in Cuneo) is an Italian mathematician, logician, aficionado of the history of science, and popular science writer and essayist, especially on philosophical atheism as a member of the Italian Union of R ...
, 2012. Computability theory Theorems in the foundations of mathematics