Inverse of Cantor Pairing Function is Primitive Recursive
Theorem
Define $k : \N \to \N$ as:
- $\map k z$ is the largest $k$ such that $T_k \le z$
where $T_k$ is the $k$-th triangular number.
Let $\pi_1 : \N \to \N$ be defined as:
- $\ds \map {\pi_1} z = z - T_{\map k z}$
Let $\pi_2 : \N \to \N$ be defined as:
- $\map {\pi_2} z = \map k z - \map {\pi_1} z$
Then, $\pi_1$ and $\pi_2$ are primitive recursive functions.
Proof
As $n = \map k z$ is the largest $n$ such that:
- $T_n \le z$
holds, it follows that $n = \map k z + 1$ is the smallest $n$ such that:
- $T_n \le z$
fails.
Or, in other words, $n = \map k z$ the smallest $n$ such that:
- $T_{n + 1} > z$
holds.
It follows that we can define $k : \N \to \N$ as:
- $\map k z = \map {\mu n} {T_{n + 1} > z}$
In order for $k$ to be primitive recursive in this way, we need the minimization to be bounded.
We will define:
- $\map k z = \map {\mu n \le z} {T_{n + 1} > z}$
Aiming for a contradiction, suppose for $z \in \N$, every $n \le z$ fails $T_{n + 1} > z$.
Then, in particular, $T_{z + 1} > z$ fails.
But by definition of triangular number:
- $T_{z + 1} = z + 1 + T_z \ge z + 1 > z$
which is a contradiction.
Therefore, for every $z \in \N$:
- $\map {\mu n \le z} {T_{n + 1} > z} = \map {\mu n} {T_{n + 1} > z}$
Define $t : \N \to \N$ as:
- $\map t k = T_k$
which is primitive recursive by Triangular Numbers are Primitive Recursive.
Thus, we have:
- $\map k z = \map {\mu n \le z} {\map t {n + 1} > z}$
which is primitive recursive by:
- Bounded Minimization is Primitive Recursive
- Ordering Relations are Primitive Recursive
- Addition is Primitive Recursive
- Constant Function is Primitive Recursive
$\Box$
By Inverse of Cantor Pairing Function, $\pi_1$ and $\pi_2$ are well-defined.
That is, for every $z$:
- $\map {\pi_1} z \ge 0$
- $\map {\pi_2} z \ge 0$
or:
- $z \ge T_{\map k z}$
- $\map k z \ge \map {\pi_1} z$
Since these always hold, we have:
- $\map {\pi_1} z = z \mathop {\dot -} T_{\map k z}$
- $\map {\pi_2} z = \map k z \mathop {\dot -} \map {\pi_1} z$
where $\dot -$ denotes partial subtraction.
Thus, we have:
- $\map {\pi_1} z = z \mathop {\dot -} \map t {\map k z}$
From Cut-Off Subtraction is Primitive Recursive, this is primitive recursive.
By the same reasoning, $\pi_2$ is primitive recursive as well.
$\blacksquare$