Truncated Subtraction (Primitive Recursion)

Definition

Truncated Subtraction ( Primitive Recursion)

Truncated subtraction, also called monus, is the primitive-recursive function

Recursing over the second argument gives

The base returns ; each step applies the predecessor function to the previous result. Once the result reaches , it stays there.

To use , which recurses over its first argument, define . Then

Here, denotes a projection function.

Construction

The base function returns the unchanged starting value. The step receives the previous recursion index , previous result , and parameter :

Thus starts at and takes predecessor steps. These steps subtract one while the result is positive and leave unchanged. The final argument swap gives in the usual subtraction order.

Example

Subtracting beyond zero

Keep the starting value fixed and increase the number of predecessor steps: