Definition by Cases is Primitive Recursive

From ProofWiki
Jump to navigation Jump to search


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

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

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

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

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

is primitive recursive.


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

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

where "otherwise" can be replaced by:

$\map {\mathcal R_k} {n_1, n_2, \ldots, n_l} = \lnot \paren {\map {\mathcal R_1} {n_1, n_2, \ldots, n_l} \lor \map {\mathcal R_2} {n_1, n_2, \ldots, n_l} \lor \ldots \lor \map {\mathcal R_{k - 1} } {n_1, n_2, \ldots, n_l} }$

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


We have:

\(\ds \map f {n_1, n_2, \ldots, n_l}\) \(=\) \(\ds \map {g_1} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\mathcal R_1} } {n_1, n_2, \ldots, n_l}\)
\(\ds \) \(\) \(\, \ds + \, \) \(\ds \map {g_2} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\mathcal R_2} } {n_1, n_2, \ldots, n_l}\)
\(\ds \) \(\) \(\, \ds + \, \) \(\ds \cdots\)
\(\ds \) \(\) \(\, \ds + \, \) \(\ds \map {g_k} {n_1, n_2, \ldots, n_l} \times \map {\chi_{\mathcal R_k} } {n_1, n_2, \ldots, n_l}\)

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

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

Then the value of the right hand side is $\map {g_r} {n_1, n_2, \ldots, n_l}$ 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:

the primitive recursive function $\operatorname{add}$
the primitive recursive functions $g_j$
the primitive recursive functions $\chi_{\mathcal R_j}$.

Hence the result.


Proof of Corollary

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