Absolute Difference Function is Primitive Recursive

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 \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \operatorname{adf} \left({n, m}\right)\)	\(=\)	\(\displaystyle \left\vert{n - m}\right\vert\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(=\)	\(\displaystyle \left({n \ \dot - \ m}\right) + \left({m \ \dot - \ n}\right)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(=\)	\(\displaystyle \operatorname{add} \left({\left({n \ \dot - \ m}\right), \left({m \ \dot - \ n}\right)}\right)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)
	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)	\(\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)\)	\(\displaystyle \)	\(\displaystyle \)	\(\displaystyle \)

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

• the primitive recursive function $n \ \dot - \ m$
• the primitive recursive function $\operatorname{add} \left({n, m}\right)$
• the projection function.

Hence the result.

$\blacksquare$