Next: An example Stream
Up: Class notes 13
Previous: Plan
When we define inductive types we wish to be sure we know the rules
governing these types. How do we know the rules make sense? Is there a
mathematical model of these types?
In the case of 
-inductive types the rules are very well
understood. They can be classified as following :-
- Formation -
- Element - unroll
- Induction - defined by the -ind form
Using the set model with 
and the
operators +, 
we can build a simple model and define precisely
what we mean by unrolling. We can even implement them using Turing
machines.
But we cannot use conventional set theory to represent co-inductive types
because in set theory a stream like 
would actually
be treated as the set 
. We cannot represent such
an infinite descending chain of sets as it violates the foundation
axiom of ZFC.