Second Principle of Recursive Definition

From ProofWiki
Jump to navigation Jump to search


Let $\N$ be the natural numbers.

Let $T$ be a set.

Let $a \in T$.

For each $n \in \N_{>0}$, let $G_n: T^n \to T$ be a mapping.

Then there exists exactly one mapping $f: \N \to T$ such that:

$\forall x \in \N: f(x) = \begin{cases} a & : x = 0\\ G_n \left({f(0), \ldots, f(n)}\right) & : x = n + 1 \end{cases}$


Define $T^*$ to be the Kleene closure of $T$, i.e.:

$T^* = \displaystyle \bigcup_{i = 1}^\infty T^i$

Note how we, for convenience, exclude the empty sequence from $T^*$.

Now define a mapping $\mathcal G: T^* \to T^*$ by:

$\mathcal G \left({t_1, \ldots, t_n}\right) = \left({t_1, \ldots, t_n, G_n \left({t_1, \ldots, t_n}\right)}\right)$

that is, extending each finite sequence $(t_1, \ldots, t_n)$ with the element $G_n \left({t_1, \ldots, t_n}\right) \in T$.

By the Principle of Recursive Definition applied to $\mathcal G$ and the finite sequence $( a )$, we obtain a unique mapping:

$\mathcal F: \N \to T^*, \mathcal F(x) = \begin{cases}(a) & : x = 0 \\ \mathcal G \left({ \mathcal F(n) }\right) & : x = n + 1\end{cases}$

Next define $f: \N \to T$ by:

$f(n) = \text{the last element of $\mathcal F(n)$}$

We claim that this $f$ has the sought properties, which will be proven by the Principle of Mathematical Induction.

We prove the following assertions by induction:

$\mathcal F(n) = \left({f(0), f(1), \ldots, f(n-1), G_n \left({f(0), \ldots, f(n-1)}\right)}\right)$
$f(n) = G_n \left({f(0), \ldots, f(n-1)}\right)$

For $n = 0$, these statements do not make sense, however it is immediate that $f(0) = \operatorname{last}((a)) = a$.

For the base case, $n = 1$, we have:

\(\displaystyle \mathcal F(1)\) \(=\) \(\displaystyle \mathcal G((a))\)
\(\displaystyle \) \(=\) \(\displaystyle (a, G_1(a))\)
\(\displaystyle \implies \ \ \) \(\displaystyle f(1)\) \(=\) \(\displaystyle G_1(a)\)

Now assume that we have that:

$\mathcal F(n) = \left({f(0), f(1), \ldots, f(n-1), G_n \left({f(0), \ldots, f(n-1)}\right)}\right)$
$f(n) = G_n \left({f(0), \ldots, f(n-1)}\right)$.


\(\displaystyle \mathcal F(n+1)\) \(=\) \(\displaystyle \mathcal G( \mathcal F(n) )\)
\(\displaystyle \) \(=\) \(\displaystyle \mathcal G \left({ (f(0),\ldots, f(n-1), G_{n-1} \left({f(0),\ldots,f(n-1)}\right)}\right)\) Induction hypothesis on $\mathcal F$
\(\displaystyle \) \(=\) \(\displaystyle \mathcal G \left({ (f(0),\ldots, f(n-1), f(n)}\right)\) Induction hypothesis on $f$
\(\displaystyle \) \(=\) \(\displaystyle \left({f(0), \ldots, f(n), G_n \left({f(0), \ldots, f(n)}\right)}\right)\) Definition of $\mathcal G$
\(\displaystyle \implies \ \ \) \(\displaystyle f(n+1)\) \(=\) \(\displaystyle \operatorname{last}( \mathcal F(n+1) )\)
\(\displaystyle \) \(=\) \(\displaystyle G_n \left({f(0), \ldots, f(n)}\right)\)

The result follows by the Principle of Mathematical Induction.


Also known as

Some authors go through considerable effort to define the sequence $(G_n)_n$ as a single mapping $G$.

The domain of such a mapping is then for example given as one of the following:

$\operatorname{dom} G := \left\{{f: \N_{<n} \to T \mid n \in \N_{>0} }\right\} = \displaystyle \bigcup_{n \mathop\in \N} [\N_{<n} \to T]$
$\operatorname{dom} G := \displaystyle \bigcup_{n \mathop\in \N_{>0} } T^n$

At $\mathsf{Pr} \infty \mathsf{fWiki}$ we deem the presentation with separate $G_n$ to be more enlightening.

Also see