definition by cases

Definition A (total) function $f:{\mathbb{N}}^k\to \mathbb{N}$ is said to be defined by cases if there are functions $f_1,\mathrm{\dots },f_m:{\mathbb{N}}^k\to \mathbb{N}$, and predicates ${\mathrm{\Phi }}_1(𝒙),\mathrm{\dots },{\mathrm{\Phi }}_m(𝒙)$, which are pairwise exclusive

$$S({\mathrm{\Phi }}_i)\cap S({\mathrm{\Phi }}_j)=\mathrm{\varnothing }$$

for $i\ne j$, such that

Since $f$ is a total function (domain is all of ${\mathbb{N}}^k$), we see that $S({\mathrm{\Phi }}_1)\cup \mathrm{\cdots }\cup S({\mathrm{\Phi }}_m)={\mathbb{N}}^k$.

Proposition 1.

As above, if the functions $f_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{f}_m\mathrm{:}{\mathrm{N}}^k\mathrm{\to }\mathrm{N}$, as well as the predicates ${\mathrm{\Phi }}_{\mathrm{1}}\mathit{}\mathrm{(}𝐱\mathrm{)}\mathrm{,}\mathrm{\dots }\mathrm{,}{\mathrm{\Phi }}_m\mathit{}\mathrm{(}𝐱\mathrm{)}$, are primitive recursive, then so is the function $f\mathrm{:}{\mathrm{N}}^k\mathrm{\to }\mathrm{N}$ defined by cases from the $f_i$ and ${\mathrm{\Phi }}_j$.

To see this, we first need the following:

Lemma 1.

If functions $f_{\mathrm{1}}\mathrm{,}\mathrm{\dots }\mathrm{,}{f}_m\mathrm{:}{\mathrm{N}}^k\mathrm{\to }\mathrm{N}$ are primitive recursive, so is $f_{\mathrm{1}}\mathrm{+}\mathrm{\cdots }\mathrm{+}{f}_m$.

Proof.

By induction on $m$. The case when $m=1$ is clear. Suppose the statement is true for $m=n$. Then $f_1+\mathrm{\cdots }+f_n+f_{n+1}=\mathrm{add}(f_1+\mathrm{\cdots }+f_n,f_{n+1})$, which is primitive recursive, since $\mathrm{add}$ is, and that primitive recursiveness is preserved under functional composition. ∎

Proof of Proposition 1.

$f$ is just

which can be re-written as

$$f={\phi }_{S({\mathrm{\Phi }}_1)}{f}_1+\mathrm{\cdots }+{\phi }_{S({\mathrm{\Phi }}_m)}{f}_m,$$

where ${\phi }_S$ denotes the characteristic function of set $S$. By assumption, both $f_i$ and ${\phi }_{S({\mathrm{\Phi }}_i)}$ are primitive recursive, so is their product, and hence the sum of these products. As a result, $f$ is primitive recursive too. ∎

Title	definition by cases
Canonical name	DefinitionByCases
Date of creation	2013-03-22 19:08:13
Last modified on	2013-03-22 19:08:13
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	5
Author	CWoo (3771)
Entry type	Example
Classification	msc 03D20