Absolute Difference Function is Primitive Recursive

From ProofWiki
Jump to navigation Jump to search

Theorem

The absolute difference function $\operatorname{adf}: \N^2 \to \N$, defined as:

$\operatorname{adf} \left({n, m}\right) = \left\vert{n - m}\right\vert$

where $\left\vert{a}\right\vert$ is defined as the absolute value of $a$, is primitive recursive‎.


Proof

We note that:

$\left\vert{n - m}\right\vert = \left({n \ \dot - \ m}\right) + \left({m \ \dot - \ n}\right) = \operatorname{add} \left({\left({n \ \dot - \ m}\right), \left({m \ \dot - \ n}\right)}\right)$

Next we note that:

$m \ \dot - \ n = \operatorname{pr}^2_2 \left({n, m}\right) \ \dot - \ \operatorname{pr}^2_1 \left({n, m}\right)$

where $\operatorname{pr}^2_k$ is the projection function.


Then:

\(\displaystyle \operatorname{adf} \left({n, m}\right)\) \(=\) \(\displaystyle \left\vert{n - m}\right\vert\)
\(\displaystyle \) \(=\) \(\displaystyle \left({n \ \dot - \ m}\right) + \left({m \ \dot - \ n}\right)\)
\(\displaystyle \) \(=\) \(\displaystyle \operatorname{add} \left({\left({n \ \dot - \ m}\right), \left({m \ \dot - \ n}\right)}\right)\)
\(\displaystyle \) \(=\) \(\displaystyle \operatorname{add} \left({\left({n \ \dot - \ m}\right), \left({\operatorname{pr}^2_2 \left({n, m}\right) \ \dot - \ \operatorname{pr}^2_1 \left({n, m}\right)}\right)}\right)\)


Hence we see that $\operatorname{adf}$ is obtained by substitution from:


Hence the result.

$\blacksquare$