[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
| Date: | -- (:) |
| From: | David Baelde <david.baelde@g...> |
| Subject: | Re: [Caml-list] Coinductive semantics |
In short, An inductive type is the least fixpoint of some equations. The coinductive type is the greatest fixpoint. For "t = nil | cons of e*t", the elements of the inductive type are the lists, but the coinductive type also contains the infinite lists. Now for induction and coinduction, not so easy to tell... The induction is the process building inductive types, the coinduction builds coinductive types. In theory, the induction always terminates and build a finite object. The coinduction should be seen as a lazy process, since it potentially builds an infinite object: running it builds the beginning of the object, then the process freezes and waits for you to inspect the object deep enough. Hope this helps... at least that's a try. -- David