Definition by Cases is Primitive Recursive

From ProofWiki
Jump to: navigation, search

Theorem

Let $\mathcal R_1, \mathcal R_2, \ldots, \mathcal R_k$ be primitive recursive relations on $\N^l$ such that:

  • $\forall i, j \in \left\{{1, 2, \ldots, k}\right\}: \mathcal R_i \implies \lnot \mathcal R_j$, i.e. all relations are mutually exclusive;
  • $\forall \left({n_1, n_2, \ldots, n_l}\right) \in \N^l: \exists i \in \left\{{1, 2, \ldots, k}\right\}: \mathcal R_i \left({n_1, n_2, \ldots, n_l}\right)$, that is, the set of relations is exhaustive.

Let $\forall i \in \left\{{1, 2, \ldots, k}\right\}: g_i: \N^l \to \N$ be primitive recursive functions.


Then the function $f: \N^l \to \N$ defined as:

$f \left({n_1, n_2, \ldots, n_l}\right) = \begin{cases} g_1 \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_1 \left({n_1, n_2, \ldots, n_l}\right) \\ g_2 \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_2 \left({n_1, n_2, \ldots, n_l}\right) \\ \quad \vdots & \quad \vdots \\ g_k \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_k \left({n_1, n_2, \ldots, n_l}\right) \end{cases}$

is primitive recursive.


Corollary

The definition can be made more flexible by defining $f$ as:

$f \left({n_1, n_2, \ldots, n_l}\right) = \begin{cases} g_1 \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_1 \left({n_1, n_2, \ldots, n_l}\right) \\ g_2 \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_2 \left({n_1, n_2, \ldots, n_l}\right) \\ \quad \vdots & \quad \vdots \\ g_{k-1} \left({n_1, n_2, \ldots, n_l}\right) & : \mathcal R_{k-1} \left({n_1, n_2, \ldots, n_l}\right) \\ g_k \left({n_1, n_2, \ldots, n_l}\right) & : \text {otherwise} \end{cases}$

where "otherwise" can be replaced by:

$\mathcal R_k \left({n_1, n_2, \ldots, n_l}\right) = \lnot \left({\mathcal R_1 \left({n_1, n_2, \ldots, n_l}\right) \lor \mathcal R_2 \left({n_1, n_2, \ldots, n_l}\right) \lor \ldots \lor \mathcal R_{k-1} \left({n_1, n_2, \ldots, n_l}\right)}\right)$

Thus we need to define only $k-1$ mutually exclusive relations as the "otherwise" case takes care of the default case.


Proof

We have:

\(\displaystyle f \left({n_1, n_2, \ldots, n_l}\right)\) \(=\) \(\displaystyle g_1 \left({n_1, n_2, \ldots, n_l}\right) \times \chi_{\mathcal R_1} \left({n_1, n_2, \ldots, n_l}\right)\) $\quad$ $\quad$
\(\displaystyle \) \(+\) \(\displaystyle g_2 \left({n_1, n_2, \ldots, n_l}\right) \times \chi_{\mathcal R_2} \left({n_1, n_2, \ldots, n_l}\right)\) $\quad$ $\quad$
\(\displaystyle \) \(+\) \(\displaystyle \cdots\) $\quad$ $\quad$
\(\displaystyle \) \(+\) \(\displaystyle g_k \left({n_1, n_2, \ldots, n_l}\right) \times \chi_{\mathcal R_k} \left({n_1, n_2, \ldots, n_l}\right)\) $\quad$ $\quad$

because if $\left({n_1, n_2, \ldots, n_l}\right) \in \N^k$, there is a unique $r$ such that $\mathcal R_r \left({n_1, n_2, \ldots, n_l}\right)$.

Then $\chi_{\mathcal R_r} \left({n_1, n_2, \ldots, n_l}\right) = 1$ and $\chi_{\mathcal R_s} \left({n_1, n_2, \ldots, n_l}\right) = 0$ for $s \ne r$.

Then the value of the RHS is $g_r \left({n_1, n_2, \ldots, n_l}\right)$ as required.


Since $\mathcal R_1, \mathcal R_2, \ldots, \mathcal R_k$ are primitive recursive, the functions $\chi_{\mathcal R_1}, \chi_{\mathcal R_2}, \ldots, \chi_{\mathcal R_k}$ are primitive recursive as well.

Hence $f$ is obtained by substitution from:

Hence the result.

$\blacksquare$


Proof of Corollary

Immediate from the main proof and Set Operations on Primitive Recursive Relations.

$\blacksquare$