Go backward to
Typing Rules
Go up to
Top
Go forward to
Structural Induction
Induction and Recursion
Syntax rule
E ::=
true
|
not
E | E
1
&E
2
Inductive definition:
true
is in Expression.
If E is in Expression, then so is
not
E.
If E
1
and E
2
are in Expression, then so is E
1
&E
2
.
No other trees are in expression.
Expression = set of trees!
Generate all trees in stages.
stage
0
= {}.
stage
i+1
=
stage
i
union {
not
E | E in
stage
i
} union { E
1
&E
2
| E
1
, E
2
in
stage
i
}.
Expression = union of all
stage
i
with
i >= 0
.
Any tree in Expression is constructed in a finite number of stages.
Author:
Wolfgang Schreiner
Last Modification: March 26, 1998
