bounded recursion

In this entry, the following notations are used:

={Fkk}, where for each k, and Fk={ff:k}.

Definition. A functionMathworldPlanetmath fFm+1 is said to be defined by bounded recursion via functions gFm, hFm+2, and kFm+1 if, for any 𝒙m and y,

  1. 1.

    f is defined by primitive recursion via g and h:

    • f(𝒙,0)=g(𝒙),

    • f(𝒙,y+1)=h(𝒙,y,f(𝒙,y));

  2. 2.

    f is bounded from above by k:

    • f(𝒙,y)k(𝒙,y).

Clearly, a function that is defined by bounded recursion is defined by primitive recursion. Conversely, a function is defined by primitive recursion, it is also defined by bounded recursion, since it is bounded by itself. However, the two concepts are not exactly the same. To make this precise, we first define what it means for a set of number-theoretic functions be closed under bounded recursion:

Definition. A set is said to be closed under bounded recursion if, for any f defined by bounded recursion via g,h,k, then f.

It is clear that is closed under both primitive recursion and bounded recursion, and so are 𝒫, the set of all primitive recursive functionsMathworldPlanetmath, as well as , the set of all total recursive functions. However,

Proposition 1.

The set ER of all elementary recursive functions is closed under bounded recursion, but not primitive recursion.

Since the exponential functionDlmfDlmfMathworldPlanetmath, the i-th prime function, and the function (x)y (the exponentMathworldPlanetmath of y in x) are elementary recursive, we have the following corollary:

Corollary 1.

If f is defined by course-of-values recursion via an elementary recursive function h, and f is bounded from above by an elementary recursive function k, then f is elementary recursive.

Title bounded recursion
Canonical name BoundedRecursion
Date of creation 2013-03-22 19:07:01
Last modified on 2013-03-22 19:07:01
Owner CWoo (3771)
Last modified by CWoo (3771)
Numerical id 5
Author CWoo (3771)
Entry type Definition
Classification msc 03D20
Synonym bounded primitive recursion
Related topic ElementaryRecursiveFunction