Predecessor Function (Primitive Recursion)

Definition

Predecessor Function ( Primitive Recursion)

The predecessor function returns for and for . It is primitive-recursive, with

The base returns ; each step returns the previous index , ignoring the previous result. Thus

Here, is a constant with no arguments, and is a projection function. This total version is also called the truncated predecessor, since it stops at rather than becoming negative or undefined.

Construction

There are no unchanged parameters, so the base takes no arguments. The step receives the previous index and previous result , selecting the index:

At input , the index is already the required predecessor. No subtraction instruction is needed, and the previous result is unused.

Example

Returning the previous index