# Example:Inductive definition of concatenation of strings

(Redirected from Concatenate)

We often want to concatenate two strings and : put one of them at the end of another. 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 ).

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

Definition: concatenation
The function is given inductively by and .

We could also define inductively on the pair of arguments:

Definition: concatenation
The function is given inductively by , , , and .

Here, we have used in the definition of ; this is ok because can be considered a substructure of .

If and are substructures of and respectively, then , and can all be considered substructures of : they must all have been shown to be in before we could show that .

We might be tempted to use induction on the first argument, but we fail: how do we define in terms of and ? You might propose something like , but this is undefined for a number of reasons: (not ), so is undefined. Moreover, if we could just stick a string at the end of another string (in this case, appending to ), we wouldn't need to define ! Without first defining cat, we can only form strings using the two rules given in the inductive definition of .