Course-of-values Recursion - Equivalence To Primitive Recursion

Equivalence To Primitive Recursion

In order to convert a definition by course-of-values recursion into a primitive recursion, an auxiliary (helper) function is used. Suppose that one wants to have

.

To define f using primitive recursion, first define the auxiliary course-of-values function that should satisfy

Thus encodes the first n values of f. The function can be defined by primitive recursion because is obtained by appending to the new element :

,

where append(n,s,x) computes, whenever s encodes a sequence of length n, a new sequence t of length n + 1 such that t = x and t = s for all i < n (again this is a primitive recursive function, under the assumption of an appropriate Gödel numbering).

Given, the original function f can be defined by, which shows that it is also a primitive recursive function.