[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