Sudan function

In the theory of computation, the Sudan function is an example of a function that is recursive, but not recursive function|primitive recursive]. This is also true of the better-known Ackermann function.
In 1926, David Hilbert conjectured that every computable function was primitive recursive. This was refuted by Gabriel Sudan and Wilhelm Ackermann both his students using different functions that were published in quick succession: Sudan in 1927, Ackermann in 1928.
The Sudan function is the earliest published example of a recursive function that is not primitive recursive.

Definition

The last equation can be equivalently written as

These equations can be used as rules of a term rewriting system (TRS).
The generalized function leads to the rewrite rules
At each reduction step the rightmost innermost occurrence of F is rewritten, by application of one of the rules -.
Calude gives an example: compute.
The reduction sequence is

F₀ = x + y

F₁ = 2^y · − y − 2