General recursive function: Difference between revisions

Revision as of 07:50, 18 August 2005

Revision as of 04:11, 24 September 2005

Line 5:

== Definition ==

Take as axiomsaxiomss 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 '''unbounded search operator''', defined as follows:

:If ''f''(''x'',''z''₁,''z''₂,...,''z''_''n'') is a partial function on the [[natural numbers]] with ''n''+1 arguments ''x'', ''z''₁,...,''z''_''n'', then the function μ''x'' ''f'' is the partial function with arguments ''z''₁,...,''z''_''n'' that returns the least ''x'' such that ''f''(0,''z''₁,''z''₂,...,''z''_''n''), ''f''(1,''z''₁,''z''₂,...,''z''_''n''), ..., ''f''(''x'',''z''₁,''z''₂,...,''z''_''n'') are all defined and ''f''(''x'',''z''₁,''z''₂,...,''z''_''n'') = 0, if such an ''x'' exists; if no such ''x'' exists, then μ''x'' ''f'' is not defined for the particular arguments ''z''₁,...,''z''_''n''.