We have taken the induction principle as an axiom for defining recursive types. In set-theory however, it is possible to take the principle as a theorem that is provable from properties of fixpoints. This set-theory also explains why we limited F in rec(X.F[X]) to be an algebraic type expression.
Given a set A, let
.
is monotone iff
As with rule-induction, we can give a definition of a set being
A set
, if, when
is applied to it,
nothing new is obtained. That
is
. Notice that the intersection of all
sets will also be
. Thus
is the least
- closed set.
The connection to recursively defined sets now follows. Every inductive definition can
be expressed as a monotone operator, and, conversely, the least - closed set of any monotone
operator can always be described inductively. In short:
To see this,
given
, set
. Conversely, given
, let
iff
.
Since disjoint union and cartesion product (considered as operators on sets) are monotonic, it follows that the fixpoint of any expression, F[X], built from these, could also be defined inductively.
We will show next class how we can obtain I() by iterating
(void) over
all ordinals.