|
== Elimination of parameters ==
{{expert needed|computer science|section|reason=properly explain the purpose of removing parameters (the text only explains *how* it is used, not *what for* - I guess in some Gödelian (un)computability proof)|date=November 2021}}
The primitive recursion schema as given may be replaced by one which makes use of fewer parameters. Let <math>w</math> be an elementary pairing function, and <math>\pi_1,\pi_2</math> be its projection functions for inversion.
Theorem: Any function constructible via the clauses of primitive recursion using the standard primitive recursion schema is constructible when the schema is replaced with the following.
*<math>f'(x,0) = g'(x)</math>
*<math>f'(x,y+1) = h'(f'(x,y))</math>
This is proven by providing two intermediate schemata for primitive recursion, starting with a function defined via the standard schema, and translating the definition into terms of each intermediate schema and finally into terms of the above schema. The first intermediate schemata is as follows:
*<math>f_1(x,0) = g_1(x)</math>
*<math>f_1(x,y+1) = h_1(x,y,f_1(x,y))</math>
Translation of the standard definition of a primitive recursive function to the intermediate schema is done inductively, where an elementary pairing function <math>w</math> is used to reinterpret the definition of a <math>k+1</math>-ary primitive recursive function into a <math>k</math>-ary primitive recursive function, terminating the induction at <math>k=1</math>.
The second intermediate schema is as follows, with the <math>x</math> parameter eliminated.
*<math>f_2(x,0)=g_2(x)</math>
*<math>f_2(x,y+1)=h_2(y,f_2(x,y))</math>
Translation to it is accomplished by pairing <math>x</math> and <math>f_1(x,y)</math> together to use one parameter for handling both, namely by setting <math>g_2(x)=w(x,g_1(x))</math>, <math>h_2(x,z)=w(\pi_1 z,h_1(\pi_1 z, x, \pi_2 z))</math>, and recovering <math>f_1(x,y)</math> from these paired images by taking <math>\pi_2(f_2(x,y))</math>.
Finally, translation of the intermediate schema into the parameter-eliminated schema is done with a similar pairing and unpairing of <math>y</math> and <math>f_2(x,y)</math>. Composing these three translations gives a definition in the original parameter-free schema.<ref>H. E. Rose, ''Subrecursive Functions and Hierarchies'' (1984), pp.33--34. Oxford Logic Guides: 9, Oxford University Press, ISBN 0-19-853189-3.</ref>
This allows primitive recursion to be formalized in Peano arithmetic, due to its lack of extra ''n''-ary function symbols.{{citation needed|date=May 2023}}
== Relationship to recursive functions ==
| 