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:

$\map {\operatorname {adf} } {n, m} = \size {n - m}$

where $\size a$ is defined as the absolute value of $a$, is primitive recursiveā€Ž.


Proof

We note that:

$\size {n - m} = \paren {n \mathop {\dot -} m} + \paren {m \mathop {\dot -} n} = \map {\operatorname {add} } {\paren {n \mathop {\dot -} m}, \paren {m \mathop {\dot -} n} }$

Next we note that:

$m \mathop {\dot -} n = \map {\pr^2_2} {n, m} \mathop {\dot -} \map {\pr^2_1} {n, m}$

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


Then:

\(\ds \map {\operatorname {adf} } {n, m}\) \(=\) \(\ds \size {n - m}\)
\(\ds \) \(=\) \(\ds \paren {n \mathop {\dot -} m} + \paren {m \mathop {\dot -} n}\)
\(\ds \) \(=\) \(\ds \map {\operatorname {add} } {\paren {n \mathop {\dot -} m}, \paren {m \mathop {\dot -} n} }\)
\(\ds \) \(=\) \(\ds \map {\operatorname {add} } {\paren {n \mathop {\dot -} m}, \paren {\map {\pr^2_2} {n, m} \mathop {\dot -} \map {\pr^2_1} {n, m} } }\)


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

the primitive recursive function $n \mathop {\dot -} m$
the primitive recursive function $\map {\operatorname {add} } {n, m}$
the projection function.


Hence the result.

$\blacksquare$