|
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>12</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>12</sub>,...,''z''<sub>''n''</sub>), ''f''(1,''z''<sub>1</sub>,''z''<sub>12</sub>,...,''z''<sub>''n''</sub>), ..., ''f''(''x'',''z''<sub>1</sub>,''z''<sub>12</sub>,...,''z''<sub>''n''</sub>) are all defined and ''f''(''x'',''z''<sub>1</sub>,''z''<sub>12</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>.
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.
|
