One of the most critical points about our definition of is that it is inductive. This can be seen better if we use
the common prefix form and write a recursviely defined predicate, that
is
Exercise Write an induction rule for any recursively defined predicate of the form
where is monotone in
.
Recall that we proved this fundamental equivalence
Theorem For all closed terms
~iff ~
Exercise Show that the same equivalence theorem holds for eager evaluation (see CN93 ???).