Remainder is Primitive Recursive

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $m, n \in \N$ be natural numbers.

Let us define the function $\operatorname{rem}: \N^2 \to \N$:

$\map \rem {n, m} = \begin{cases}

\text{the remainder when } n \text{ is divided by } m & : m \ne 0 \\ 0 & : m = 0 \end{cases}$

where the $\text{remainder}$ is as defined in the Division Theorem:

If $n = m q + r$, where $0 \le r < m$, then $r$ is the remainder.


Then $\rem$ is primitive recursive.


Proof

Let $\map \rem {n, m} = r$.

We see that as $n$ increases by $1$, then so does $r$, except when $n = m-1$ in which case increasing $n$ by $1$ makes $r$ go to $0$.

We also take into account the case where $m = 0$:

So we can define $\rem$ by cases:

$\map \rem {n, m} = \begin{cases}

0 & : \map \rem {n - 1, m} = m - 1 \text { or } m = 0 \text { or } n = 0\\ \map \rem {n - 1, m} + 1 & : \text {otherwise} \\ \end{cases}$


We remind ourselves of the following primitive recursive functions:


We have:

  • $\map \sgn m = 1 \iff m \ne 0$
  • $\map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} } = 1 \iff \map \rem {n, m} \ne m \, \dot - \, 1$.

So:

$\map \sgn m \, \map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} } = 1 \iff m > 0 \land \map \rem {n, m} \ne m \, \dot - \, 1$.


So we see that:

$\map \rem {n + 1, m} = \paren {\map \rem {n, m} + 1} \, \map \sgn m \, \map {\overline \sgn} {\map {\chi_{\operatorname{eq} } } {\map \rem {n, m}, m \, \dot - \, 1} }$


So $\rem$ is obtained by primitive recursion (over the first variable, which is allowed by Permutation of Variables of Primitive Recursive Function) from the primitive recursive functions:

Thus we can use Definition by Cases is Primitive Recursive and it follows that $\rem$ is primitive recursive.

$\blacksquare$