Go backward to 5.3 Properties of Recursive DefinitionsGo up to 5 Induction and Recursion |

The concept of induction is not limited to **N**; it can be applied to any
set whose construction is based on a corresponding principle.

with object constant

( forallx_{1},...,x_{m1},y_{1}inS, ...,y_{n1}inS:f_{1}(x_{1}, ...,x_{m1},y_{1}, ...,y_{n1}) inS), ... , ( forallx_{1},...,x_{mc},y_{1}inS, ...,y_{nc}inS:f_{c}(x_{1}, ...,x_{mc},y_{1}, ...,y_{nc}) inS)

By this definition, `S` denotes the smallest set
on which the conjunction of these formulas holds.

The notion "smallest" used in above definition implies that every element of the defined set is denoted by a constructor term

for some termsf_{i}(T_{1}, ...,T_{mi},S_{1}, ...,S_{ni})

- The set
**N**is inductively defined by

for some constructors 0 and '. Every element of0 in **N**,**forall**`x`in**N**:`x`' in**N****N**is of the form0'

e.g. 0'''' is interpreted as the number 4 in^{...}',**N**. - For every set
`T`, the set "List(`T`)" is defined by

for some constructors "nil" and "cons". Every element of List(nil in List( `T`),**forall**`e`in`T`,`l`in List(`T`): cons(`e`,`l`) in List(`T`).`T`) is of the formcons(

e.g. "cons(2, cons(3, nil))" is interpreted as the list [2, 3] in List(`e`_{0}, ..., cons(`e`_{n-1}, nil)),**N**). - For every set
`T`, the set "Tree(`T`)" is defined by

for some constructors "empty" and "tree". Every element of Tree(empty in Tree( `T`),**forall**`e`in`T`,`l`in Tree(`T`),`r`in List(`T`): node(`e`,`l`,`r`) in Tree(`T`).`T`) is of the formnode(

e.g. "node(1, node(2, node(3, empty, empty), node(4, empty, empty)), node(5, empty, empty))" is interpreted as the following tree in Tree(`n`_{0}, node(`n`_{11}, ...), node(`n`_{21}, ...)),**N**):1

2 5

3 4 - The set "Term" is defined by

for some constructors 0, 1, -, +, *. An element of "Term" is "1+(1+0)*1".0 in Term, 1 in Term, **forall**`x`in Term: -`x`in Term,**forall**`x`in Term,`y`in Term:`x`+`y`in Term,**forall**`x`in Term,`y`in Term:`x`*`y`in Term - The set "Formula" is defined by

for some constructors "T", "not", "and", "forall". An element of "Formula" is "forall(X, and(T, or(T, F)))" (assuming X in "Variable").T in Formula **forall**`x`in Formula: not(`x`) in Formula,**forall**`x`in Formula,`y`in Formula: and(`x`,`y`) in Formula,**forall**`x`in Variable,`y`in Formula: forall(`x`,`y`) in Formula

Inductive set definitions may appear in various notations; e.g., the set "Term" in above example is more conveniently defined as

Term ::= 0 | 1 | -Term | Term+Term | Term*Term.in the syntax of

We now constrain our notion of inductive sets such that the elements preserve "knowledge" about their construction.

i.e.,

forallx,y:f(x) =f(y) =>x=y

i.e., different constructors yield different results.

forallx,y:f(x) !=g(y)

Every element of a term algebra is denoted by *one and only one*
constructor term

for some termsf_{i}(T_{1}, ...,T_{mi},S_{1}, ...,S_{ni})

A nice property of a term algebra is that they allow inductive function and
predicate definitions in the style of inductive definitions over **N**; we do
not introduce these definitions formally but give some examples.

- Take the set List(
`T`) defined in the previous example and assume that it is a term algebra. We define the length of a list as

Then we have length(cons(1, cons(2, nil))) = 2.length: List( `T`) ->**N**length(nil) := 0 length(cons( `e`,`l`)) := 1+length(`l`). - Take the set List(
`T`) defined in the previous example and assume that it is a term algebra. We define the depth of a tree as

Then we have depth(node(1, empty, node(2, node(3, empty, empty), empty))) = 3.depth: Tree( `T`) ->**N**depth(empty) := 0 depth(node( `n`,`l`,`r`)) := 1+max(depth(`l`), depth(`r`)). - Take the set Term defined in the previous example
and assume that it is a term algebra. We define the value of a term
as

Then we have value(1+(1+0)*1)=2.value: Term -> **N**value(0) := 0 _{N}value(1) := 1 _{N}value(- `x`) := -_{N}value(`x`)value( `x`+`y`) := value(`x`)+_{N}value(`y`)value( `x`*`y`) := value(`x`)*_{N}value(`y`)

On inductively defined sets (not necessarily term algebras) we have the following induction principle.

for an inductively defined setforallxinS:F

for every constructor

forallx_{1},...,x_{mi},y_{1}inS, ...,y_{ni}inS:( F[x:=y_{1}] /\ ... /\F[x:=y_{ni}]) =>F[x:=f_{i}(x_{1},...,x_{mi},y_{1}, ...,y_{ni})]

Intuitively, we let the induction run over the "structure" of every term

denoting some elementf_{i}(x_{1},...,x_{mi},y_{1}, ...,y_{ni}).

We define

nil in List( T),foralleinT,lin List(T): cons(e,l) in List(T).

and claim that (for the function "length" defined in the previous example) the following holds:

append: List( T) x List(T) -> List(T)append(nil, y) :=yappend(cons( e,x),y) := cons(e, append(x,y))

forallxin List(T),yin List(T):length(append( x,y)) = length(x)+length(y).

We proceed by structural induction on `x`:

**Case**`x`=nil:- We have to show

Take arbitrary**forall**`y`in List(`T`):length(append(nil, `y`)) = length(nil)+length(`y`).`y`in List(`T`). We havelength(append(nil, `y`))= (definition append) length( `y`)= 0+length( `y`)= (definition length) length(nil)+length( `y`). **Case**`x`=cons(`e`,`l`):- Take arbitrary
`e`in`T`and`l`in List(`T`).We assume (induction hypothesis)

and have to show**forall**`y`in List(`T`):length(append( `l`,`y`)) = length(`l`)+length(`y`)

Take arbitrary**forall**`y`in List(`T`):length(append(cons( `e`,`l`),`y`)) = length(cons(`e`,`l`)) +length(`y`).`y`in List(`T`). We havelength(append(cons( `e`,`l`),`y`))= (definition append) length(cons( `e`, append(`l`,`y`)))= (definition length) 1 + length(append( `l`,`y`))= (induction hypothesis) 1 + (length( `l`) + length(`y`))= (1 + length( `l`)) + length(`y`)= (definition length) length(cons( `e`,`l`)) + length(`y`).

Several formal concepts in computer science, e.g. datatypes and formal languages, can be reduced to inductively defined sets; the principle of structural induction is therefore of great importance.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999