Content deleted Content added
No edit summary |
Recursuve -> primitive recursive |
||
Line 8:
Take as axioms the axioms of the [[primitive recursive function]]s, but extend the definitions so as to allow for [[partial function]]s. Add one further operator, the ''least search'' or ''unbounded search'' operator, defined as follows:
:If ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) is a partial function on the [[natural numbers]] with ''n''+1 arguments ''x'', ''z''<sub>1</sub>,...,''z''<sub>''n''</sub>, then the function μ''x'' ''f'' is the partial function with arguments ''z''<sub>1</sub>,...,''z''<sub>''n''</sub> that returns the least ''x'' such that ''f''(0,''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>), ''f''(1,''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>), ..., ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) are all defined and ''f''(''x'',''z''<sub>1</sub>,''z''<sub>2</sub>,...,''z''<sub>''n''</sub>) = 0, if such an ''x'' exists; if no such ''x'' exists, then μ''x'' ''f'' is not defined for the particular arguments ''z''<sub>1</sub>,...,''z''<sub>''n''</sub>.
It is easy to see that this least search axiom (along with the simple primitive recursion axioms) implies the bounded search axiom of primitive resursion.
The set of ''partial recursive functions'' is defined as the smallest set of partial functions of any [[arity]] from natural numbers to natural numbers which contains the zero, successor, and projection functions, and which is closed under composition, primitive recursion, and unbounded search.
| |||