View source for 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 [[rule]]s 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 [[∈]] X</math>; this means that for all of the [[substructure]]s <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 ===

{{Example:inductive definition of string length}}

=== Example: bad inductive definition ===

{{Example:bad inductive function definition}}

=== Example: concatenation ===

{{Example:inductive definition of concatenation of strings}}

=== Example: addition ===

{{Example:inductive definition of addition}}