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 <math>f(x)</math.
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: