Given an inductively defined set , we know that every element of is formed using one of the rules defining . Therefore, if we want to define a function with domain , it suffices to describe how to evaluate it for objects formed with each rule.
Moreover, we can think of forming the value of substructures of (i.e. the "smaller" elements of that were used to construct ), we can assume that has already been defined, and use it in the definition of .
at the same time that we show that ; this means that for all of the
A function defined in this way is called an inductively defined function or a recursive function.
For example, we could define a function for computing the length of a string inductively:
It is reasonable to use substructure of ; we must have already proved that before we prove that
when defining because is a
We can then compute
Example: bad inductive definition
When giving an inductive definition of a function , it is important to only use in the definition of if is a substructure of .
For example, the "function" given inductively by and is not well-defined. Indeed, try computing ; any choice of output satisfies the defining equations.
As a more insidious example, consider substructure of , but is not ok, because is not necessarily a substructure of and we can only apply to substructures of in the definition of .
given by and . Here, it is perfectly reasonable to use in the definition of because is a
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:
We could also define inductively on the pair of arguments:
Here, we have used substructure of .
in the definition of ; this is ok because can be considered a
If 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 cat, we can only form strings using the two rules given in the inductive definition of .
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
We can inductively define familiar operations like addition and
There are several alternatives: we could induct on the second argument, on
the first argument, or on both arguments: