Signum (Primitive Recursion)

Definition

Signum ( Primitive Recursion)

The natural-number signum is primitive-recursive and satisfies

The base returns ; every step returns , independently of the previous result. Thus

Here, supplies the initial value, while the constant function ignores both the previous index and previous result . Equivalently, signum is the indicator function of the positive natural numbers: .

Construction

There are no unchanged parameters, so the base takes no arguments. The step takes two arguments, and , but need not use them. The constant- function is constructed from the zero function and successor function:

Example

Recording whether a number is positive