Primitive recursive function - Revision history

2A02:8108:2C2F:900:8966:3881:401D:564E: /* Predicate "Is zero" */

2025-06-28T08:08:44Z

Predicate "Is zero"

← Previous revision		Revision as of 08:08, 28 June 2025
Line 138:		Line 138:

	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		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(0) = 1</math> and e.g. <math>IsZero(8) = \rho(C_1^0,C_0^2)(S(7)) = C_0^2(7,IsZero(7)) = 0</math>.		<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() = 1</math> and e.g. <math>IsZero(8) = \rho(C_1^0,C_0^2)(S(7)) = C_0^2(7,IsZero(7)) = 0</math>.

	=== Predicate "Less or equal" ===		=== Predicate "Less or equal" ===

Guhhhh: /* Definition */ \(f\) was missing the \(y'\) argument -- that's what makes it loop downward in the first place.

2025-06-15T12:16:56Z

Definition: \(f\) was missing the \(y'\) argument -- that's what makes it loop downward in the first place.

← Previous revision		Revision as of 12:16, 15 June 2025
Line 31:		Line 31:
	f(y, x_1, \dots, x_k) &= \begin{cases}		f(y, x_1, \dots, x_k) &= \begin{cases}
	g(x_1, \dots, x_k) & \text{if } y=0 \\		g(x_1, \dots, x_k) & \text{if } y=0 \\
	h(y', f(x_1, \dots, x_k) ,x_1, \dots, x_k) & \text{if } y=S(y') \text{ for a } y' \in \mathbb{N} \\		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{cases}
	\end{align}</math>		\end{align}</math>

Noises From Afar: /* Definition */ Changed definition of the function returned by the ρ operator to use the cases environment

2025-06-13T22:49:40Z

Definition: Changed definition of the function returned by the ρ operator to use the cases environment

← Previous revision		Revision as of 22:49, 13 June 2025
Line 26:		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.		\| 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 (''k~~'' ~~+~~ ~~2)-ary function <math>h(y,z,x_1,\ldots,x_k)\,</math>:<math display="block">\begin{align}		\| 5=''Primitive recursion operator'' <math>\rho</math>: Given the ''k''-ary function <math>g(x_1,\ldots,x_k)\,</math> and the <math>(k+2)</math>-ary function <math>h(y,z,x_1,\ldots,x_k)\,</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}\\		\rho(g, h) &\ \stackrel{\mathrm{def}}{=}\ f, \quad\text{where the }(k+1)\text{-ary function } f \text{ is defined by}\\
	f(0,x_1,\~~ldots~~,x_k) &= ~~g(x_1,\ldots,x_k) \~~\		f(y, x_1, \dots, x_k) &= \begin{cases}
			g(x_1, \dots, x_k) & \text{if } y=0 \\
	f(S(y),x_1,\ldots,x_k) &= h(y,f(y,x_1,\ldots,x_k),x_1,\ldots,x_k).\end{align}</math>
			h(y', f(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:''		''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>.		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>.

Jochen Burghardt: Undid revision 1294830678 by 103.58.110.6 (talk): looks pretty much the same; all occurrences should have the same source code

2025-06-10T19:08:11Z

Undid revision 1294830678 by 103.58.110.6 (talk): looks pretty much the same; *all* occurrences should have the same source code

← Previous revision		Revision as of 19:08, 10 June 2025
Line 138:		Line 138:
	=== Predicate "Less or equal" ===		=== Predicate "Less or equal" ===

	Using the property <math>x \leq y \iff x \~~mathbin{\overset~~.-} y = 0</math>, the 2-ary function <math>Leq</math> can be defined by <math>Leq = IsZero \circ Sub</math>. Then <math>Leq(x,y) = 1</math> if <math>x \leq y</math>, and <math>Leq(x,y) = 0</math>, otherwise. As a computation example,		Using the property <math>x \leq y \iff x \stackrel.- y = 0</math>, the 2-ary function <math>Leq</math> can be defined by <math>Leq = IsZero \circ Sub</math>. Then <math>Leq(x,y) = 1</math> if <math>x \leq y</math>, and <math>Leq(x,y) = 0</math>, otherwise. As a computation example,
	:<math>\begin{array}{lll}		:<math>\begin{array}{lll}
	& Leq(8,3) \\		& Leq(8,3) \\

103.58.110.6: Correct spacing around binary operator /* Predicate "Less or equal" */

2025-06-10T02:01:37Z

Correct spacing around binary operator Predicate "Less or equal"

← Previous revision		Revision as of 02:01, 10 June 2025
Line 138:		Line 138:
	=== Predicate "Less or equal" ===		=== Predicate "Less or equal" ===

	Using the property <math>x \leq y \iff x \~~stackrel~~.- y = 0</math>, the 2-ary function <math>Leq</math> can be defined by <math>Leq = IsZero \circ Sub</math>. Then <math>Leq(x,y) = 1</math> if <math>x \leq y</math>, and <math>Leq(x,y) = 0</math>, otherwise. As a computation example,		Using the property <math>x \leq y \iff x \mathbin{\overset.-} y = 0</math>, the 2-ary function <math>Leq</math> can be defined by <math>Leq = IsZero \circ Sub</math>. Then <math>Leq(x,y) = 1</math> if <math>x \leq y</math>, and <math>Leq(x,y) = 0</math>, otherwise. As a computation example,
	:<math>\begin{array}{lll}		:<math>\begin{array}{lll}
	& Leq(8,3) \\		& Leq(8,3) \\

Wws: /* Some common primitive recursive functions */ Correct Kleene page number (reL 1971 editionn on archive.org)

2025-04-27T17:30:38Z

Some common primitive recursive functions: Correct Kleene page number (reL 1971 editionn on archive.org)

← Previous revision		Revision as of 17:30, 27 April 2025
Line 189:		Line 189:

	=== Some common primitive recursive functions ===		=== Some common primitive recursive functions ===
	The following examples and definitions are from {{harvtxt\|Kleene\|1952\|pp=~~223–231~~}}. Many appear with proofs. Most also appear with similar names, either as proofs or as examples, in {{harvtxt\|Boolos\|Burgess\|Jeffrey\|2002\|pp=63–70}} they add the logarithm lo(x, y) or lg(x, y) depending on the exact derivation.		The following examples and definitions are from {{harvtxt\|Kleene\|1952\|pp=222–231}}. Many appear with proofs. Most also appear with similar names, either as proofs or as examples, in {{harvtxt\|Boolos\|Burgess\|Jeffrey\|2002\|pp=63–70}} they add the logarithm lo(x, y) or lg(x, y) depending on the exact derivation.

	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.		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.

Citation bot: Altered pages. Add: issue, jstor, pages. Formatted dashes. | Use this bot. Report bugs. | Suggested by Dominic3203 | Linked from User:Mathbot/Most_linked_math_articles | #UCB_webform_linked 1796/1913

2025-02-25T07:36:56Z

Altered pages. Add: issue, jstor, pages. Formatted dashes. | Use this bot. Report bugs. | Suggested by Dominic3203 | Linked from User:Mathbot/Most_linked_math_articles | #UCB_webform_linked 1796/1913

← Previous revision		Revision as of 07:36, 25 February 2025
Line 315:		Line 315:
	\| title=ACM '67: Proceedings of the 1967 22nd national conference		\| title=ACM '67: Proceedings of the 1967 22nd national conference
	\| year=1967		\| year=1967
			\| pages=465–469
	\| doi-access=free		\| 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.		}}</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 351:		Line 352:
	== References ==		== References ==
	* {{citation\|last1=Brainerd \|first1=W.S. \|last2=Landweber \|first2=L.H. \|year=1974 \|title=Theory of Computation \|publisher=Wiley \|isbn=0471095850}}		* {{citation\|last1=Brainerd \|first1=W.S. \|last2=Landweber \|first2=L.H. \|year=1974 \|title=Theory of Computation \|publisher=Wiley \|isbn=0471095850}}
	* {{citation\|last=Hartmanis \|first=Juris \|author-link=Juris Hartmanis \|year=1989\|chapter=Overview of Computational Complexity Theory \|title=Computational Complexity Theory \|publisher=American Mathematical Society\|pp=~~1-17~~ \|isbn=978-0-8218-0131-4 \|series=Proceedings of Symposia in Applied Mathematics \|volume=38 \|mr=1020807}}		* {{citation\|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}}
	* [[Robert I. Soare]], ''Recursively Enumerable Sets and Degrees'', Springer-Verlag, 1987. {{isbn\|0-387-15299-7}}		* [[Robert I. Soare]], ''Recursively Enumerable Sets and Degrees'', Springer-Verlag, 1987. {{isbn\|0-387-15299-7}}
	* {{citation \|last=Kleene \|first=Stephen Cole \|author-link=Stephen Cole Kleene \|year=1952\|title=Introduction to Metamathematics \|edition=7th [1974] reprint; 2nd \|publisher=[[North-Holland Publishing Company]] \|oclc=3757798 \|isbn=0444100881}} Chapter XI. General Recursive Functions §57		* {{citation \|last=Kleene \|first=Stephen Cole \|author-link=Stephen Cole Kleene \|year=1952\|title=Introduction to Metamathematics \|edition=7th [1974] reprint; 2nd \|publisher=[[North-Holland Publishing Company]] \|oclc=3757798 \|isbn=0444100881}} Chapter XI. General Recursive Functions §57
Line 365:		Line 366:
	\| url = https://scholar.archive.org/work/ruvjr6nkyre4nfxjdme2refpwe		\| url = https://scholar.archive.org/work/ruvjr6nkyre4nfxjdme2refpwe
	\| volume = 2		\| volume = 2
	\| year = 1996}}		\| year = 1996\| jstor = 420992
			}}
	*{{citation		*{{citation
	\| last = Severin \| first = Daniel E.		\| last = Severin \| first = Daniel E.
Line 386:		Line 388:
	\| title = Primitive recursive functions		\| title = Primitive recursive functions
	\| volume = 53		\| volume = 53
	\| year = 1947\| doi-access = free		\| year = 1947\| issue = 10
			\| doi-access = free
	}}		}}
	*{{citation		*{{citation
Line 396:		Line 399:
	\| title = A reduction of the recursion scheme		\| title = A reduction of the recursion scheme
	\| volume = 32		\| volume = 32
	\| year = 1967}}		\| year = 1967\| issue = 4
			\| jstor = 2270177
			}}
	*{{citation		*{{citation
	\| last = Gladstone \| first = M. D.		\| last = Gladstone \| first = M. D.
Line 405:		Line 410:
	\| title = Simplifications of the recursion scheme		\| title = Simplifications of the recursion scheme
	\| volume = 36		\| volume = 36
	\| year = 1971}}		\| year = 1971\| issue = 4
			\| jstor = 2272468
			}}

	{{Mathematical logic}}		{{Mathematical logic}}

OAbot: Open access bot: doi updated in citation with #oabot.

2025-02-03T03:58:53Z

Open access bot: doi updated in citation with #oabot.

← Previous revision		Revision as of 03:58, 3 February 2025
Line 386:		Line 386:
	\| title = Primitive recursive functions		\| title = Primitive recursive functions
	\| volume = 53		\| volume = 53
	\| year = 1947}}		\| year = 1947\| doi-access = free
			}}
	*{{citation		*{{citation
	\| last = Gladstone \| first = M. D.		\| last = Gladstone \| first = M. D.

David Eppstein: first templated citation (in early 2014) was cs2, so standardize on that; templatize more refs to fix harv linking errors

2025-01-27T08:13:47Z

first templated citation (in early 2014) was cs2, so standardize on that; templatize more refs to fix harv linking errors

@@ Line 1: / Line 1: @@
 {{Short description|Function computable with bounded loops}}
 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 51: / Line 52: @@
 |<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.: {{cite book | author=Henk Barendregt | author-link=Henk Barendregt | contribution=Functional Programming and Lambda Calculus | pages=321&ndash;364 | isbn=0-444-88074-7 | editor=Jan van Leeuwen | editor-link=Jan van Leeuwen | title=Formal Models and Semantics | publisher=Elsevier | series=Handbook of Theoretical Computer Science | volume=B | year=1990}} Here: 2.2.6 ''initial functions'', Def.2.2.7 ''primitive recursion'', p.331-332.</ref> define <math>C_n^k</math> only for <math>n = 0</math> and <math>k = 1</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.: {{citation | author=Henk Barendregt | author-link=Henk Barendregt | contribution=Functional Programming and Lambda Calculus | pages=321&ndash;364 | isbn=0-444-88074-7 | editor=Jan van Leeuwen | editor-link=Jan van Leeuwen | title=Formal Models and Semantics | publisher=Elsevier | series=Handbook of Theoretical Computer Science | volume=B | year=1990}} Here: 2.2.6 ''initial functions'', Def.2.2.7 ''primitive recursion'', p.331-332.</ref> define <math>C_n^k</math> only for <math>n = 0</math> and <math>k = 1</math>.
 }}
@@ Line 303: / Line 304: @@
 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>{{cite conference
+The [[LOOP (programming language)|LOOP language]], introduced in a 1967 paper by [[Albert R. Meyer]] and [[Dennis M. Ritchie]],<ref>{{citation
 | doi=10.1145/800196.806014
-| title=The complexity of loop programs
+| contribution=The complexity of loop programs
 | last1=Meyer
 | first1=Albert R.
@@ Line 312: / Line 313: @@
 | first2=Dennis M.
 | authorlink2=Dennis Ritchie
-| conference=ACM '67: Proceedings of the 1967 22nd national conference
+| title=ACM '67: Proceedings of the 1967 22nd national conference
 | year=1967
 | doi-access=free
@@ Line 330: / Line 331: @@
 == 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">{{cite book|author=Peter Smith|title=An Introduction to Gödel's Theorems|year=2013|publisher=Cambridge University Press|isbn=978-1-107-02284-3|pages=98–99|edition=2nd |url=https://www.logicmatters.net/igt/}}</ref><ref name="Tourlakis2003">{{cite book|author=George Tourlakis|title=Lectures in Logic and Set Theory: Volume 1, Mathematical Logic|year=2003|publisher=Cambridge University Press|isbn=978-1-139-43942-8|page=129}}</ref><ref name="Downey2014">{{cite book|editor=Rod Downey|title=Turing's Legacy: Developments from Turing's Ideas in Logic|year=2014|publisher=Cambridge University Press|isbn=978-1-107-04348-0|page=474}}</ref>
+[[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">{{citation|author=Peter Smith|title=An Introduction to Gödel's Theorems|year=2013|publisher=Cambridge University Press|isbn=978-1-107-02284-3|pages=98–99|edition=2nd |url=https://www.logicmatters.net/igt/}}</ref><ref name="Tourlakis2003">{{citation|author=George Tourlakis|title=Lectures in Logic and Set Theory: Volume 1, Mathematical Logic|year=2003|publisher=Cambridge University Press|isbn=978-1-139-43942-8|page=129}}</ref><ref name="Downey2014">{{citation|editor=Rod Downey|title=Turing's Legacy: Developments from Turing's Ideas in Logic|year=2014|publisher=Cambridge University Press|isbn=978-1-107-04348-0|page=474}}</ref>
 [[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: / Line 350: @@
 == References ==
-* {{cite book|last1=Brainerd |first1=W.S. |last2=Landweber |first2=L.H. |year=1974 |title=Theory of Computation |publisher=Wiley |isbn=0471095850}}
+* {{citation|last1=Brainerd |first1=W.S. |last2=Landweber |first2=L.H. |year=1974 |title=Theory of Computation |publisher=Wiley |isbn=0471095850}}
-* {{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|pp=1-17 |isbn=978-0-8218-0131-4 |series=Proceedings of Symposia in Applied Mathematics |volume=38 |mr=1020807}}
+* {{citation|last=Hartmanis |first=Juris |author-link=Juris Hartmanis |year=1989|chapter=Overview of Computational Complexity Theory |title=Computational Complexity Theory |publisher=American Mathematical Society|pp=1-17 |isbn=978-0-8218-0131-4 |series=Proceedings of Symposia in Applied Mathematics |volume=38 |mr=1020807}}
 * [[Robert I. Soare]], ''Recursively Enumerable Sets and Degrees'', Springer-Verlag, 1987.  {{isbn|0-387-15299-7}}
-* {{Cite book |last=Kleene |first=Stephen Cole |author-link=Stephen Cole Kleene |year=1952|title=Introduction to Metamathematics |edition=7th [1974] reprint; 2nd |publisher=[[North-Holland Publishing Company]] |oclc=3757798 |isbn=0444100881}} Chapter XI. General Recursive Functions §57
+* {{citation |last=Kleene |first=Stephen Cole |author-link=Stephen Cole Kleene |year=1952|title=Introduction to Metamathematics |edition=7th [1974] reprint; 2nd |publisher=[[North-Holland Publishing Company]] |oclc=3757798 |isbn=0444100881}} Chapter XI. General Recursive Functions §57
 *{{citation |author-link=George Boolos |first1=George |last1=Boolos |author2-link=John P. Burgess |first2=John |last2=Burgess |author3-link=Richard Jeffrey |first3=Richard |last3=Jeffrey |title=Computability and Logic |publisher=Cambridge University Press |edition=4th |date=2002 |isbn=9780521007580 |pages=70–71}}
 {{Mathematical logic}}

EmilJ: /* Pure recursion */ correction, I misread the statement of Severin's result

2025-01-21T12:10:14Z

Pure recursion: correction, I misread the statement of Severin's result

← Previous revision		Revision as of 12:10, 21 January 2025
Line 289:		Line 289:
	:<math>\begin{align} f(0) & = 0,\\		:<math>\begin{align} f(0) & = 0,\\
	f(S(y)) & = h(f(y)), \end{align}</math>		f(S(y)) & = h(f(y)), \end{align}</math>
	suffices if we extend the set of initial functions with truncated subtraction ''x ∸ y''.		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 ===		=== Additional primitive recursive forms ===