Content deleted Content added
→Variants: The Fischer, Fischer, Beigel paper is complete rubbish. They reprove things known decades earlier, and conjecture things also refuted decades earlier. |
No edit summary |
||
| (14 intermediate revisions by 12 users not shown) | |||
Line 1:
{{Short description|Function computable with bounded loops}}
{{CS1 config|mode=cs2}}
In [[computability theory]], a '''primitive recursive function''' is, roughly speaking, a function that can be computed by a [[computer program]] whose [[loop (programming)|loops]] are all [[For loop|"for" loops]] (that is, an upper bound of the number of iterations of every loop is fixed before entering the loop). Primitive recursive functions form a strict [[subset]] of those [[general recursive function]]s that are also [[total function]]s.
Line 25 ⟶ 26:
| 4=''Composition operator'' <math>\circ\,</math> (also called the ''substitution operator''): Given an ''m''-ary function <math>h(x_1,\ldots,x_m)\,</math> and ''m'' ''k''-ary functions <math>g_1(x_1,\ldots,x_k),\ldots,g_m(x_1,\ldots, x_k)</math>: <math display="block">h \circ (g_1, \ldots, g_m) \ \stackrel{\mathrm{def}}{=}\ f, \quad\text{where}\quad f(x_1,\ldots,x_k) = h(g_1(x_1,\ldots,x_k),\ldots,g_m(x_1,\ldots,x_k)).</math> For <math>m=1</math>, the ordinary [[function composition]] <math>h \circ g_1</math> is obtained.
| 5=''Primitive recursion operator'' <math>\rho</math>: Given the ''k''-ary function <math>g(x_1,\ldots,x_k)\,</math> and the <math>(
:<math display="block">\begin{align} \rho(g, h) &\ \stackrel{\mathrm{def}}{=}\ f, \quad\text{where the }(k+1)\text{-ary function } f \text{ is defined by}\\
g(x_1, \dots, x_k) & \text{if } y=0 \\
h(y', f(y', x_1, \dots, x_k) ,x_1, \dots, x_k) & \text{if } y=S(y') \text{ for a } y' \in \mathbb{N} \\
\end{cases}
\end{align}</math>
''Interpretation:''
The function <math>f</math> acts as a [[for loop|for-loop]] from <math>0</math> up to the value of its first argument. The rest of the arguments for <math>f</math>, denoted here with <math>x_1,\ldots,x_k</math>, are a set of initial conditions for the for-loop which may be used by it during calculations but which are immutable by it. The functions <math>g</math> and <math>h</math> on the right-hand side of the equations that define <math>f</math> represent the body of the loop, which performs calculations. The function <math>g</math> is used only once to perform initial calculations. Calculations for subsequent steps of the loop are performed by <math>h</math>. The first parameter of <math>h</math> is fed the "current" value of the for-loop's index. The second parameter of <math>h</math> is fed the result of the for-loop's previous calculations, from previous steps. The rest of the parameters for <math>h</math> are those immutable initial conditions for the for-loop mentioned earlier. They may be used by <math>h</math> to perform calculations but they will not themselves be altered by <math>h</math>.
Line 34 ⟶ 39:
The '''primitive recursive functions''' are the basic functions and those obtained from the basic functions by applying these operations a finite number of times.
=== Primitive-recursiveness of vector-valued functions ===
A (vector-valued) function <math>f : \mathbb{N}^m \to \mathbb{N}^n</math> is primitive recursive if it can be written as
:<math>f(x_1, \dots, x_m) = (f_1(x_1, \dots, x_m), \dots, f_n(x_1, \dots, x_m))</math>
where each component <math>f_i : \mathbb{N}^m \to \mathbb{N}</math> is a (scalar-valued) primitive recursive function.<ref>{{harvtxt|PlanetMath}}</ref>
== Examples ==
Line 51 ⟶ 61:
|<math>S \circ S</math> is a 1-ary function that adds 2 to its input, <math>(S \circ S)(x) = x+2</math>.
|<math>S \circ C_0^1</math> is a 1-ary function which returns 1 for every input: <math>(S \circ C_0^1)(x) = S(C_0^1(x)) = S(0) = 1</math>. That is, <math>S \circ C_0^1</math> and <math>C_1^1</math> are the same function: <math>S \circ C_0^1 = C_1^1</math>. In a similar way, every <math>C_n^k</math> can be expressed as a composition of appropriately many <math>S</math> and <math>C_0^k</math>. Moreover, <math>C_0^k</math> equals <math>C_0^1 \circ P_1^k</math>, since <math>C_0^k(x_1,\ldots,x_k) = 0 = C_0^1(x_1) = C_0^1(P_1^k(x_1,\ldots,x_k)) = (C_0^1 \circ P_1^k)(x_1,\ldots,x_k)</math>. For these reasons, some authors<ref>E.g.: {{
}}
Line 107 ⟶ 117:
===Truncated subtraction===
The limited subtraction function (also called "[[monus]]", and denoted "<math>\
:<math>\begin{array}{rcll}
y \
y \
\end{array}</math>
Since the recursion runs over the second argument, we begin with a primitive recursive definition of the reversed subtraction, <math>RSub(y,x) = x \
:<math>\begin{array}{lll}
& Sub(8,1) \\
Line 128 ⟶ 138:
=== Converting predicates to numeric functions ===
In some settings it is natural to consider primitive recursive functions that take as inputs tuples that mix numbers with [[truth value]]s (that is <math>t</math> for true and <math>f</math> for false),{{Citation needed|date=January 2025 |reason=Kleene never considers mixed domains - see p. 226 where he lists the 4 types of functions he considers. Using N to represent the naturals, and T to represent the truth values: (a) N to N (b) N to T (c) T oto T (d) T to N}} or that produce truth values as outputs.{{sfn|Kleene|
=== Predicate "Is zero" ===
As an example for a primitive recursive predicate, the 1-ary function <math>IsZero</math> shall be defined such that <math>IsZero(x) = 1</math> if <math>x = 0</math>, and
<math>IsZero(x) = 0</math>, otherwise. This can be achieved by defining <math>IsZero = \rho(C_1^0,C_0^2)</math>. Then, <math>IsZero(0) = \rho(C_1^0,C_0^2)(0) = C_1^0(
=== Predicate "Less or equal" ===
Using the property <math>x \leq y \iff x \
:<math>\begin{array}{lll}
& Leq(8,3) \\
Line 188 ⟶ 198:
=== Some common primitive recursive functions ===
The following examples and definitions are from {{
In the following the mark " ' ", e.g. a', is the primitive mark meaning "the successor of", usually thought of as " +1", e.g. a +1 =<sub>def</sub> a'. The functions 16–20 and #G are of particular interest with respect to converting primitive recursive predicates to, and extracting them from, their "arithmetical" form expressed as [[Gödel number]]s.
Line 271 ⟶ 281:
===Constant functions===
Instead of <math>C_n^k</math>,
alternative definitions use just one 0-ary ''zero function'' <math>C_0^0</math> as a primitive function that always returns zero, and built the constant functions from the zero function, the successor function and the composition operator.{{Citation needed|date=July 2025}}
=== Iterative functions ===
Line 289 ⟶ 299:
:<math>\begin{align} f(0) & = 0,\\
f(S(y)) & = h(f(y)), \end{align}</math>
suffices to generate all [[unary operation|unary]] primitive recursive functions if we extend the set of initial functions with truncated subtraction ''x ∸ y''. We get ''all'' primitive recursive functions if we additionally include + as an initial function.
=== Additional primitive recursive forms ===
Line 303 ⟶ 313:
An example of a primitive recursive programming language is one that contains basic arithmetic operators (e.g. + and −, or ADD and SUBTRACT), conditionals and comparison (IF-THEN, EQUALS, LESS-THAN), and bounded loops, such as the basic [[for loop]], where there is a known or calculable upper bound to all loops (FOR i FROM 1 TO n, with neither i nor n modifiable by the loop body). No control structures of greater generality, such as [[while loop]]s or IF-THEN plus [[GOTO]], are admitted in a primitive recursive language.
The [[LOOP (programming language)|LOOP language]], introduced in a 1967 paper by [[Albert R. Meyer]] and [[Dennis M. Ritchie]],<ref>{{
| doi=10.1145/800196.806014
|
| last1=Meyer
| first1=Albert R.
Line 312 ⟶ 322:
| first2=Dennis M.
| authorlink2=Dennis Ritchie
|
| year=1967
| pages=465–469
| doi-access=free
}}</ref> is such a language. Its computing power coincides with the primitive recursive functions. A variant of the LOOP language is [[Douglas Hofstadter]]'s [[BlooP and FlooP|BlooP]] in ''[[Gödel, Escher, Bach]]''. Adding unbounded loops (WHILE, GOTO) makes the language [[general recursive function|general recursive]] and [[Turing completeness|Turing-complete]], as are all real-world computer programming languages.
Line 330 ⟶ 341:
== History ==
[[Recursive definition]]s had been used more or less formally in mathematics before, but the construction of primitive recursion is traced back to [[Richard Dedekind]]'s theorem 126 of his ''Was sind und was sollen die Zahlen?'' (1888). This work was the first to give a proof that a certain recursive construction defines a unique function.<ref name="Smith2013">{{
[[Primitive recursive arithmetic]] was first proposed by [[Thoralf Skolem]]<ref>[[Thoralf Skolem]] (1923) "The foundations of elementary arithmetic" in [[Jean van Heijenoort]], translator and ed. (1967) ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard Univ. Press: 302-33.</ref> in 1923.
Line 349 ⟶ 360:
== References ==
*{{cite book
| last1 = Boolos
| first1 = George
| author-link = George Boolos
| last2 = Burgess
| first2 = John
| author2-link = John P. Burgess
| last3 = Jeffrey
| first3 = Richard C.
| author3-link = Richard Jeffrey
| title = Computability and Logic
| publisher = Cambridge University Press
| edition = 4th
| date = 2002
| isbn = 9780521007580
}}
*{{cite book
| last1 = Brainerd
| first1 = W.S.
| last2 = Landweber
| first2 = L.H.
| year = 1974
| title = Theory of Computation
| publisher = Wiley
| isbn = 0471095850
}}
*{{cite journal
| last = Gladstone
| first = M. D.
| doi = 10.2307/2270177
| journal = [[The Journal of Symbolic Logic]]
| mr = 224460
| pages = 505–508
| title = A reduction of the recursion scheme
| volume = 32
| year = 1967
| issue = 4
| jstor = 2270177
}}
*{{cite journal
| last = Gladstone
| first = M. D.
| doi = 10.2307/2272468
| journal = The Journal of Symbolic Logic
| mr = 305993
| pages = 653–665
| title = Simplifications of the recursion scheme
| volume = 36
| year = 1971
| issue = 4
| jstor = 2272468
}}
*{{cite book
| last = Hartmanis
| first = Juris
| author-link = Juris Hartmanis
| year = 1989
| chapter = Overview of Computational Complexity Theory
| title = Computational Complexity Theory
| publisher = American Mathematical Society
| pages = 1–17
| isbn = 978-0-8218-0131-4
| series = Proceedings of Symposia in Applied Mathematics
| volume = 38
| mr = 1020807
}}
*{{cite book
| last = Kleene
| first = Stephen Cole
| author-link = Stephen Cole Kleene
| year = 1974
| orig-year = 1952
| title = Introduction to Metamathematics
| chapter = Chapter XI. General Recursive Functions §57
| edition = 7th reprint; 2nd
| publisher = [[North-Holland Publishing Company]]
| oclc = 3757798
| isbn = 0444100881
}}
*{{cite web
| author = PlanetMath
| title = primitive recursive vector-valued function
| url = https://planetmath.org/primitiverecursivevectorvaluedfunction
| access-date = 2025-07-04
}}
*{{cite book
| last = Rogers
| first = Hartley Jr.
| title = Theory of Recursive Functions and Effective Computability
| publisher = [[MIT Press]]
| year = 1987
| orig-year = 1967
| edition = Reprint
| isbn = 9780262680523
}}
*{{cite journal
| last = Robinson
| first = Raphael M.
| doi = 10.1090/S0002-9904-1947-08911-4
| journal = [[Bulletin of the American Mathematical Society]]
| mr = 22536
| pages = 925–942
| title = Primitive recursive functions
| volume = 53
| year = 1947
| issue = 10
| doi-access = free
}}
*{{cite journal
| last = Severin
| first = Daniel E.
| arxiv = cs/0603063
| doi = 10.2178/jsl/1230396909
| issue = 4
| journal = The Journal of Symbolic Logic
| jstor = 275903221
| mr = 2467207
| pages = 1122–1138
| title = Unary primitive recursive functions
| volume = 73
| year = 2008
}}
*{{cite book
| last = Soare
| first = Robert I.
| author-link = Robert I. Soare
| isbn = 0-387-15299-7
| title = Recursively Enumerable Sets and Degrees
| publisher = Springer-Verlag
| year = 1987
}}
*{{cite journal
| last = Soare
| first = Robert I.
| author-link = Robert I. Soare
| doi = 10.2307/420992
| volume = 2
| issue = 3
| journal = The Bulletin of Symbolic Logic
| mr = 1416870
| pages = 284–321
| title = Computability and recursion
| url = https://scholar.archive.org/work/ruvjr6nkyre4nfxjdme2refpwe
| year = 1996
| jstor = 420992
}}
{{Mathematical logic}}
| |||