[racket] Inductive and coinductive reasoning? (was "shared and immutable structures")

On Wed, Feb 02, 2011 at 04:39:07PM -0800, mike at goblin.punk.net wrote:
> On Wed, Feb 02, 2011 at 11:30:45AM -0500, Shriram Krishnamurthi wrote:
> > Yes you do.  Far less useful at our level.  But shared + immutable
> > gives you coinductive.  That's why the distinction helps.
> 
> I'm not familiar with these terms and had trouble follwiong that
> thread.  Would someone explain or point me to appropriate reading?

The term is used in coq, a proof-checking system.

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/bertot_sl2.pdf

But since his is rather obscure, let me elaborate a bit.

Induction over a tree structure just relies on then tree having bounded 
depth, so that the inductio eventually terminates.  This is the usual 
recursive tree processing we all know well.

Coinduction deals with trees that may indeed be infinite.  They may 
be infinite, implemented by lazy evaluation, so that the infinitude 
doesn't have to be present in its totality in out finite computers. 

To a first approximation, it means that the recusive function is so 
coded that it produces output after examining only a finite part of the 
tree, no matter what it finds when looking through the tree.

But that in itself isn't the whole story.  It's really applicable when 
the function produces another lazy data structure.  In this case, the 
function will produce any part of the output (lazily, when needed) 
by looking at only a finite part of the input.  Of course the amount onf 
input it looks at may depend on what output is demanded.

So this is useful for such things as stream processors, which take a 
lazy stream as argument and produce another as output.

Of course, this isn't the only definition of coinduction.

There's another in whihc you are performing two inductions at once, 
intertwined in some way.  I don't think this is the one the OP was 
talking about, but I could be wrong.

-- hendrik