Example:Inductive definition of concatenation of strings

From CS2800 wiki
(Redirected from Cat)

We often want to concatenate two strings [math]x [/math] and [math]y [/math]: put one of them at the end of another. [math]xy [/math] is not a string according to the inductive definition of Σ^*, but we can define a function that produces that string (which we will then abbreviate as [math]xy [/math]).

There are at least two options. We could use induction on the second argument:

Definition: concatenation
The function [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]cat(x,ε) := x [/math] and [math]cat(x,ya) := cat(x,y)a [/math].

We could also define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math] inductively on the pair of arguments:

Definition: concatenation
The function [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php/%CE%95}{ε} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math], and [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y)\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{b} [/math].

Here, we have used [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in the definition of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math]; this is ok because [math](x,\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math] can be considered a substructure of [math](\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math].

If [math]x' [/math] and [math]y' [/math] are substructures of [math]x [/math] and [math]y [/math] respectively, then [math](x',y') [/math], [math](x,y') [/math] and [math](x',y) [/math] can all be considered substructures of [math](x,y) [/math]: they must all have been shown to be in [math]X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math] before we could show that [math](x,y) \href{/cs2800/wiki/index.php/%E2%88%88}{∈} X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math].

We might be tempted to use induction on the first argument, but we fail: how do we define [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in terms of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,y) [/math] and [math]a [/math]? You might propose something like [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a)y [/math], but this is undefined for a number of reasons: [math]a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Σ [/math] (not [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]), so [math]cat(x,a) [/math] is undefined. Moreover, if we could just stick a string at the end of another string (in this case, appending [math]y [/math] to [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a) [/math]), we wouldn't need to define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math]! Without first defining cat, we can only form strings using the two rules given in the inductive definition of [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math].