Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Coinductive semantics
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2006-01-05 (19:48)
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.