# Difference between revisions of "Inductively defined function"

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 at the same time that we show that ; this means that for all of the 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 [itex]f(x)</math.

A function defined in this way is called an inductively defined function or a recursive function.

## Contents

### Example: length

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

Definition: len
Let be given inductively by and .

It is reasonable to use when defining because is a substructure of ; we must have already proved that before we prove that

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 given by and . Here, it is perfectly reasonable to use in the definition of because is a 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 .

### Example: concatenation

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 .

### Example: addition

We can inductively define familiar operations like addition and multiplication.

There are several alternatives: we could induct on the second argument, on the first argument, or on both arguments:

Definition: addition
Let be given inductively by and .

Definition: addition
Let be given inductively by and .

Definition: addition
Let be given inductively by , , , and .