Next: Iterative Definition of
Up: Set Theoretic Approach
Previous: Set Theoretic Approach
In the previous lecture we received a brief introduction to monotonicity.
Remember, given two sets 
and 
and an operator 
, 
is
monotone
In English, an operator is monotone
if it preserves subset inclusion on its range.
An interesting fact about inductively defined sets is that
they are expressible using a monontone operator. We can accomplish this
by definining a rule set 
with rules of the form 
,
where
. By
definition of closure on rule sets from the prior lecture, 
is
closed.
Now by definition of least closed sets:
We can abbreviate 
as 
.
Suppose that we are given any inductive rule set 
. Our task is to
show that is expressible as a rule set 
for some monotone
operator . Given any rule
, we can define 
as
is then the set of all conclusions of rule instances whose premises
are a subset of 
.
Exercise Show that 
(i.e. show that the type
defined
by the initial rule set is the same as the type defined by the rule set
over the monotone operator). In doing so, you will have proven that
every inductive definition is expressible using a monotone operator.