General recursive function

From Esolang
Jump to navigation Jump to search

General recursive functions are a model of computability based upon partial functions from natural numbers to natural numbers. A partial function is general recursive when it can be expressed as the composite of several primitive functions; intuitively, these primitive functions correspond to basic operations on natural numbers like addition as well as basic computational structures like bounded loops and searches.

Definition

A general recursive function is constructed by composition of basic functions which operate on natural numbers. The following traditional basis, known as Kleene's basis or the µ-recursive basis, is often used, but there are others.

Basic functions

  • Zero: Z(x) = 0
  • Successor: S(x) = x+1
  • Projection: Pin(x1, ..., xn) = xi

Operators

  • Composition
f(x1, ..., xn) = g(h1(x1, ..., xn), ..., hm(x1, ..., xn))
  • Primitive recursion
f(x1, ..., xn, 0) = g(x1, ..., xn)
f(x1, ..., xn, y+1) = h(x1, ..., xn, y, f(x1, ..., xn, y))
  • Minimization
f(x1, ..., xn) = y if g(x1, ..., xn, y) = 0 and g(x1, ..., xn, z) > 0 for any z < y

Relation to other models

Any function on natural numbers which can be computed by a Turing machine is a general recursive function. Additionally, any general recursive function can be implemented on a Turing machine. This leads to:

Theorem (Turing-completeness). General recursive functions are equivalent to Turing machines. (Turing, 1937)

General recursion can be used to compute formulae over natural numbers, given a suitable choice of axioms. This allows humans to use computing machines to automatically derive truths about natural numbers. For example, Heyting arithmetic is a system for proving facts about natural numbers, and:

Theorem (Realizability). Every formula of Heyting arithmetic can be realized by a general recursive function. (Kleene, 1945)

However, Peano arithmetic is not so fortunate, and there is no automatic computation for its formulae:

Theorem (Gödel's first incompleteness). For any particular Gödel encoding of any axioms equivalent to Peano arithmetic, there is a formula of those axioms which captures a truth about the natural numbers and is not realizable. (Gödel 1931, Rosser 1936)

The main difference between Peano arithmetic and Heyting arithmetic is the principle of excluded middle, which is an axiom of Peano arithmetic but not of Heyting arithmetic. This is easiest to understand by omission; in Peano arithmetic, statements are either true or false, but in Heyting arithmetic they can also be not false, a state of not necessarily being true but definitely refuting falsehood. Similarly, the partial nature of general recursion provides for a state of not finished, a state of not necessarily having reached a result but definitely refuting stuckness.

Another important limitation of general recursion is that it is not complete for the class of partial functions on the natural numbers. It's not even complete for total functions:

Theorem (Busy Beaver function). There is a well-defined total function on the natural numbers not expressed by any Turing machine. (Radó, 1961)[1]

In this sense, any invocation of Rice's theorem creates an incompleteness where general recursion provably cannot compute certain otherwise-innocuous statements about natural numbers.

Topos theory

This is all well-grounded using topos theory. A topos is a formalization of mathematical logic. While most classical mathematics is done with respect to a topos that has the principle of excluded middle, topos theory does not require it; a topos is Boolean if it has excluded middle, and some topoi are non-Boolean.

Over several decades, it was established that every Grothendieck topos is a Heyting category; that is, every logic built from a natural analysis of topological spaces has logical axioms corresponding to Heyting arithmetic. This generalizes set theory, which is the analysis of the topological space with a single point.

Eventually, a topos was constructed that explains general recursion without excluded middle:

Construction (Effective topos). There is a non-Boolean topos whose arrows are general recursive functions over Kleene's basis. (Hyland, 1982)

Examples

The following languages have general recursive functions:

Primitive recursive function

Without the minimization operator, the functions that can be constructed are primitive recursive functions. Primitive recursive functions are total functions.

Not every computable total function is primitive recursive, e.g. the Ackermann function. However, the Ackermann function is higher-order primitive recursive, also known as primitive recursive functional: it can be expressed by primitive recursion if higher-order functions are added to the domain. Higher-order primitive recursion is also total.

The following languages have higher-order primitive recursive functions:

External resources

References

  1. ↑ T. Radó, "On non-computable functions," in The Bell System Technical Journal, vol. 41, no. 3, pp. 877-884, May 1962, doi: 10.1002/j.1538-7305.1962.tb00480.x. https://gwern.net/doc/cs/computable/1962-rado.pdf
Retrieved from "https://esolangs.org/w/index.php?title=General_recursive_function&oldid=158949"