Hi,

I am studying coinduction(not induction) as part of a class on static analysis. Rummaging around the internet, I am simply not finding a clear, concise description of:

• How coinduction actually proves something(it seems that coinduction is like waving a magic hand in the treatments I've read)
• What propositions require coinductive proof
• How to operate a coinductive proof

I have reviewed Wikipedia and a tutorial on co-induction/co-algebras.

My best understanding:

Coinduction is used in propositions such as:

f(x) = ... f(x) ...

Where ... denotes "stuff here that doesn't rely on f(x)".

Then, f(x) is assumed true, and the ... is proved. If ... holds, then the proposition f(x) holds, out to and including infinity.

The treatments I've read include a functional function Q that takes f(x) and returns some f'(x), and somehow that makes it all better.

At an abstract level, I read that coinduction operates over a coalgebra, which is dual to induction/algebras.

This (1) seems awfully like circular reasoning and (2)seems awfully like voodoo. I suspect part of what I'm missing is a careful and clear description of coalgebras, plus how we jump from algebra into a coalgebra and back again. The professor declined to go into that part of the subject.

Note: I'm not an algebraicist by study- I write software and my thesis is over low-level software operations. So this is really unfamiliar to me and I'm trying to de-jargon this into my head.

(semi-cross-posted from stackoverflow.com)