Example:Inductive definition of string length

From CS2800 wiki
(Redirected from Length)

For example, we could define a function for computing the length of a string inductively:

Definition: len
Let [math]\href{/cs2800/wiki/index.php/Len}{len} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} → \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php/%CE%95}{ε}) \href{/cs2800/wiki/index.php?title=%3D&action=edit&redlink=1}{=} 0 [/math] and [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := 1 + \href{/cs2800/wiki/index.php/Len}{len}(x) [/math].

It is reasonable to use [math]\href{/cs2800/wiki/index.php/Len}{len}(x) [/math] when defining [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] because [math]x [/math] is a substructure of [math]xa [/math]; we must have already proved that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] before we prove that [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]

We can then compute

[math]\begin{align*} \href{/cs2800/wiki/index.php/Len}{len}(0110) &= 1+\href{/cs2800/wiki/index.php/Len}{len}(011) \\ &= 1 + (1 + \href{/cs2800/wiki/index.php/Len}{len}(01)) \\ &= 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(0) \\ &= 1 + 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=%5Cepsilon&action=edit&redlink=1}{\epsilon}) \\ &= 1 + 1 + 1 + 1 + 0 = 4 \end{align*} [/math]