# Absolute Difference Function is Primitive Recursive

## 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:

 $\displaystyle \map {\operatorname {adf} } {n, m}$ $=$ $\displaystyle \size {n - m}$ $\displaystyle$ $=$ $\displaystyle \paren {n \mathop {\dot -} m} + \paren {m \mathop {\dot -} n}$ $\displaystyle$ $=$ $\displaystyle \map {\operatorname {add} } {\paren {n \mathop {\dot -} m}, \paren {m \mathop {\dot -} n} }$ $\displaystyle$ $=$ $\displaystyle \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$