Editing Primitive recursive function (section)

=== Some common primitive recursive functions ===
The following examples and definitions are from {{harvtxt|Kleene|1952|pp=222–231}}. Many appear with proofs. Most also appear with similar names, either as proofs or as examples, in {{harvtxt|Boolos|Burgess|Jeffrey|2002|pp=63–70}} they add the logarithm lo(x, y) or lg(x, y) depending on the exact derivation.

In the following the mark " ' ", e.g. a', is the primitive mark meaning "the successor of", usually thought of as " +1", e.g. a +1 =<sub>def</sub> a'. The functions 16–20 and #G are of particular interest with respect to converting primitive recursive predicates to, and extracting them from, their "arithmetical" form expressed as [[Gödel number]]s.

:# Addition: a+b
:# Multiplication: a×b
:# Exponentiation: a<sup>b</sup>
:# Factorial a! : 0! = 1, a'! = a!×a'
:# pred(a): (Predecessor or decrement): If a > 0 then a−1 else 0
:# Proper subtraction a ∸ b: If a ≥ b then a−b else 0
:# Minimum(a<sub>1</sub>, ... a<sub>n</sub>)
:# Maximum(a<sub>1</sub>, ... a<sub>n</sub>)
:# Absolute difference: | a−b | =<sub>def</sub> (a ∸ b) + (b ∸ a)
:# ~sg(a): NOT[signum(a)]: If a=0 then 1 else 0
:# sg(a): signum(a): If a=0 then 0 else 1
:# a | b: (a divides b): If b=k×a for some k then 0 else 1
:# Remainder(a, b): the leftover if b does not divide a "evenly".  Also called MOD(a, b)
:# a = b: sg | a − b |  (Kleene's convention was to represent ''true'' by 0 and ''false'' by 1; presently, especially in computers, the most common convention is the reverse, namely to represent ''true'' by 1 and ''false'' by 0, which amounts to changing sg into ~sg here and in the next item)
:# a < b: sg( a' ∸ b )
:# Pr(a): a is a prime number Pr(a) =<sub>def</sub>  a>1 & NOT(Exists c)<sub>1<c<a</sub> [ c|a ]
:# p<sub>i</sub>: the i+1th prime number
:# (a)<sub>i</sub>: exponent of p<sub>i</sub> in a: the unique x such that p<sub>i</sub><sup>x</sup>|a & NOT(p<sub>i</sub><sup>x'</sup>|a)
:# lh(a): the "length" or number of non-vanishing exponents in a
:# lo(a, b): (logarithm of a to base b): If a, b > 1 then the greatest x such that b<sup>x</sup> | a else 0

: ''In the following, the abbreviation '''x''' =<sub>def</sub>  x<sub>1</sub>, ... x<sub>n</sub>; subscripts may be applied if the meaning requires.''

* #A:  A function φ definable explicitly from functions Ψ and constants q<sub>1</sub>, ... q<sub>n</sub> is primitive recursive in Ψ.
* #B:  The finite sum Σ<sub>y<z</sub> ψ('''x''', y) and product Π<sub>y<z</sub>ψ('''x''', y) are primitive recursive in ψ.
* #C:  A ''predicate'' P obtained by substituting functions χ<sub>1</sub>,..., χ<sub>m</sub> for the respective variables of a predicate Q is primitive recursive in χ<sub>1</sub>,..., χ<sub>m</sub>, Q.
* #D:  The following ''predicates'' are primitive recursive in Q and R:
::* NOT_Q('''x''') .
::* Q OR R: Q('''x''') V R('''x'''),
::* Q AND R: Q('''x''') & R('''x'''),
::* Q IMPLIES R: Q('''x''') → R('''x''')
::* Q is equivalent to R: Q('''x''') ≡ R('''x''')
* #E:  The following ''predicates'' are primitive recursive in the ''predicate'' R:
::* (Ey)<sub>y<z</sub> R('''x''', y) where (Ey)<sub>y<z</sub> denotes "there exists at least one y that is less than z such that"
::* (y)<sub>y<z</sub> R('''x''', y) where (y)<sub>y<z</sub> denotes "for all y less than z it is true that"
::* μy<sub>y<z</sub> R('''x''', y).  The operator μy<sub>y<z</sub> R('''x''', y) is a ''bounded'' form of the so-called minimization- or [[mu-operator]]: Defined as "the least value of y less than z such that R('''x''', y) is true; or z if there is no such value."
* #F:  Definition by cases: The function defined thus, where Q<sub>1</sub>, ..., Q<sub>m</sub> are mutually exclusive ''predicates'' (or "ψ('''x''') shall have the value given by the first clause that applies), is primitive recursive in φ<sub>1</sub>, ..., Q<sub>1</sub>, ... Q<sub>m</sub>:
::  φ('''x''') =
::* φ<sub>1</sub>('''x''') if Q<sub>1</sub>('''x''') is true,
::* .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .  .
::* φ<sub>m</sub>('''x''') if Q<sub>m</sub>('''x''') is true
::* φ<sub>m+1</sub>('''x''') otherwise
* #G: If φ satisfies the equation:
::  φ(y,'''x''') = χ(y, COURSE-φ(y; x<sub>2</sub>, ... x<sub>n</sub> ), x<sub>2</sub>, ... x<sub>n</sub> then φ is primitive recursive in χ. The value COURSE-φ(y; '''x'''<sub>2 to n</sub> ) of the course-of-values function encodes the sequence of values φ(0,'''x'''<sub>2 to n</sub>), ..., φ(y-1,'''x'''<sub>2 to n</sub>) of the original function.