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

 From: Hendrik Boom (hendrik at topoi.pooq.com) Date: Wed Feb 2 20:45:16 EST 2011 Previous message: [racket] Inductive and coinductive reasoning? (was "shared and immutable structures") Next message: [racket] Inductive and coinductive reasoning? (was "shared and immutable structures") Messages sorted by: [date] [thread] [subject] [author]

```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

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

```

 Posted on the users mailing list. Previous message: [racket] Inductive and coinductive reasoning? (was "shared and immutable structures") Next message: [racket] Inductive and coinductive reasoning? (was "shared and immutable structures") Messages sorted by: [date] [thread] [subject] [author]