Next: Defining
Up: Class notes 9
Previous: Class notes 9
Today we will cover the following material:
-
We will develop a recursive definition of the set of propositional
formulas,
.
-
We will use this to consider what giving a recursive definition of the type
of formulas,
, would involve. This will then used to understand the general
process of recursively defining types. In particular,
this involved an introduction to the
ML constructs rec and absrectype and to a general induction
principle for them.
-
We will briefly look at the fixpoints of monotone operators and their connection
to inductively - defined sets.