Inductively defined function

From CS2800 wiki

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 [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} X [/math]; 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.

Example: length

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

Definition: len
Let [math]\href{/cs2800/wiki/index.php/Len}{len} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} → \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php/%CE%95}{ε}) \href{/cs2800/wiki/index.php?title=%3D&action=edit&redlink=1}{=} 0 [/math] and [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := 1 + \href{/cs2800/wiki/index.php/Len}{len}(x) [/math].

It is reasonable to use [math]\href{/cs2800/wiki/index.php/Len}{len}(x) [/math] when defining [math]\href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] because [math]x [/math] is a substructure of [math]xa [/math]; we must have already proved that [math]x \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] before we prove that [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} \href{/cs2800/wiki/index.php/%E2%88%88}{∈} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]

We can then compute

[math]\begin{align*} \href{/cs2800/wiki/index.php/Len}{len}(0110) &= 1+\href{/cs2800/wiki/index.php/Len}{len}(011) \\ &= 1 + (1 + \href{/cs2800/wiki/index.php/Len}{len}(01)) \\ &= 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(0) \\ &= 1 + 1 + 1 + 1 + \href{/cs2800/wiki/index.php/Len}{len}(\href{/cs2800/wiki/index.php?title=%5Cepsilon&action=edit&redlink=1}{\epsilon}) \\ &= 1 + 1 + 1 + 1 + 0 = 4 \end{align*} [/math]

Example: bad inductive definition

When giving an inductive definition of a function [math]f [/math], it is important to only use [math]f(x') [/math] in the definition of [math]f(x) [/math] if [math]x' [/math] is a substructure of [math]x [/math].

For example, the "function" [math]bogus : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] given inductively by [math]bogus(\href{/cs2800/wiki/index.php/%CE%95}{ε}) := 0 [/math] and [math]bogus(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := bogus(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] is not well-defined. Indeed, try computing [math]bogus("abc") [/math]; any choice of output satisfies the defining equations.

As a more insidious example, consider [math]nasty : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] given by [math]nasty(\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php/%CE%95}{ε} [/math] and [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) := nasty(nasty(x)) [/math]. Here, it is perfectly reasonable to use [math]nasty(x) [/math] in the definition of [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math] because [math]x [/math] is a substructure of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math], but [math]nasty(nasty(x)) [/math] is not ok, because [math]nasty(x) [/math] is not necessarily a substructure of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math] and we can only apply [math]nasty [/math] to substructures of [math]\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math] in the definition of [math]nasty(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa}) [/math].

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 [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]cat(x,ε) := x [/math] and [math]cat(x,ya) := cat(x,y)a [/math].

We could also define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math] inductively on the pair of arguments:

Definition: concatenation
The function [math]\href{/cs2800/wiki/index.php/Cat}{cat} : \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} \href{/cs2800/wiki/index.php/%E2%86%92}{→} \href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math] is given inductively by [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php/%CE%95}{ε} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php/%CE%95}{ε},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb} [/math], [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php/%CE%95}{ε}) := \href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa} [/math], and [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) := \href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y)\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{b} [/math].

Here, we have used [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in the definition of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math]; this is ok because [math](x,\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math] can be considered a substructure of [math](\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},\href{/cs2800/wiki/index.php?title=Yb&action=edit&redlink=1}{yb}) [/math].

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 [math]X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math] before we could show that [math](x,y) \href{/cs2800/wiki/index.php/%E2%88%88}{∈} X \href{/cs2800/wiki/index.php/%5Ctimes}{\times} X [/math].

We might be tempted to use induction on the first argument, but we fail: how do we define [math]\href{/cs2800/wiki/index.php/Cat}{cat}(\href{/cs2800/wiki/index.php?title=Xa&action=edit&redlink=1}{xa},y) [/math] in terms of [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,y) [/math] and [math]a [/math]? You might propose something like [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a)y [/math], but this is undefined for a number of reasons: [math]a \href{/cs2800/wiki/index.php/%E2%88%88}{∈} Σ [/math] (not [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math]), 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 [math]\href{/cs2800/wiki/index.php/Cat}{cat}(x,a) [/math]), we wouldn't need to define [math]\href{/cs2800/wiki/index.php/Cat}{cat} [/math]! Without first defining cat, we can only form strings using the two rules given in the inductive definition of [math]\href{/cs2800/wiki/index.php?title=%CE%A3%5E*&action=edit&redlink=1}{Σ^*} [/math].

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 [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(x,Z) := x [/math] and [math]add(x,S~n) := S~add(x,n) [/math].


Definition: addition
Let [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(Z,x) := x [/math] and [math]add(S~n,x) := S~add(n,x) [/math].


Definition: addition
Let [math]add : \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Ctimes}{\times} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} \href{/cs2800/wiki/index.php/%5Cto}{\to} \href{/cs2800/wiki/index.php/%E2%84%95}{ℕ} [/math] be given inductively by [math]add(Z,Z) := Z [/math], [math]add(Z,S~n) := S~n [/math], [math]add(S~n,Z) := S~n [/math], and [math]add(S~n,S~m) := S~S~add(n,m) [/math].