Inductively defined function

Given an inductively defined set [math]X [/math], we know that every element [math]x [/math] of [math]X [/math] is formed using one of the rules defining [math]X [/math]. Therefore, if we want to define a function with domain [math]X [/math], it suffices to describe how to evaluate it for objects formed with each rule.

Moreover, we can think of forming the value of [math]f(x) [/math] at the same time that we show that ; this means that for all of the substructures [math]x' [/math] of [math]x [/math] (i.e. the ``smaller elements of [math]X [/math] that were used to construct [math]x [/math]), we can assume that [math]f(x') [/math] has already been defined, and use it in the definition of <math>f(x)</math.

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

As a more insidious example, consider given by and . Here, it is perfectly reasonable to use [math]nasty(x) [/math] in the definition of because [math]x [/math] is a substructure of , but [math]nasty(nasty(x)) [/math] is not ok, because [math]nasty(x) [/math] is not necessarily a substructure of and we can only apply [math]nasty [/math] to substructures of in the definition of .

Example: concatenation

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 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 [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 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 [math]a [/math]? You might propose something like , but this is undefined for a number of reasons: (not ), 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 ), 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 .

Inductively defined function

Contents

Example: length

Example: bad inductive definition

Example: concatenation

Example: addition