Content deleted Content added
Undid revision 1294830678 by 103.58.110.6 (talk): looks pretty much the same; *all* occurrences should have the same source code |
No edit summary |
||
| (6 intermediate revisions by 5 users not shown) | |||
Line 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 35 ⟶ 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 108 ⟶ 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 129 ⟶ 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 189 ⟶ 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 272 ⟶ 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 351 ⟶ 360:
== References ==
*{{cite book
| last1 = Boolos
| first1 = George
| author-link = George Boolos
| last2 = Burgess
| first2 = John
| author2-link = John P. Burgess
|
| first3 = Richard C.
| author3-link = Richard Jeffrey
| title = Computability and Logic
| publisher = Cambridge University Press
| edition = 4th
|
| isbn = 9780521007580
*{{cite book
|
| first1 = W.S.
|
| first2 = L.H.
|
| title = Theory of Computation
|
| isbn = 0471095850
}}
*{{cite journal
| last =
| 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
Line 410 ⟶ 412:
| 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}}
| |||