# Co-induction understanding

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)

-
Are you familiar with Haskell? Its data types are coalgebraic (by default). – Reid Barton Oct 16 '09 at 19:11
Not such that I can write it; I can follow it a bit. – Paul Oct 17 '09 at 17:55

## 2 Answers

Here's an informal example of a proof by coinduction.

The extended natural numbers E = {0, 1, 2, ..., ∞} are the final coalgebra for the functor F(X) = 1 + X. (If we have an F-coalgebra X, i.e. a set X with a map f : X -> 1 + X, and an element of X, what we can do is repeatedly apply f until we get the element of 1 rather than a new element of X. Counting the number of times we got new elements of X gives us an element of E. This is the unique F-coalgebra map X -> E.) In Haskell we would write

data Nat = Z | S Nat   -- possible values are Z, S Z, S (S Z), ..., S (S (S ...))


We can define addition:

add :: Nat -> Nat -> Nat
add Z b = b
add (S a1) b = S (add a1 b)


I'll prove that add a Z = a by coinduction. We perform case analysis on a. If a = Z then it follows from the first equation. If a = S a1 then add a Z = add (S a1) Z = S (add a1 Z) = S a1 = a where the next-to-last step used the coinductive hypothesis.

Why isn't that circular reasoning? We were allowed to apply the coinductive hypothesis because we did so inside an application of the "constructor" S. In other words, even if you didn't believe the coinductive hypothesis, you would still conclude that add a Z and a were both of the form Z or both of the form S x--in other words, add a Z and a agree for to one observation. Using that statement where we used the coinductive hypothesis, you find that add a Z and a agree to two observations, etc. Since an element of E is determined by all the finite sequences of observations we can make, it follows that add a Z = a.

(Note that this argument works even when a = S (S (S ...))!)

Exercise: Give a formal version of this argument, using the definition of E as the final F-coalgebra.

-
If you take the minimum solution of (Nat = Z | S Nat) then the argument by induction is (add Z Z = Z) and (add (S b) Z = S (add b Z) = S b). That is, it looks exactly the same as your argument by coinduction! Does this always happen? Often? – rgrig Sep 8 '10 at 12:06

This was my attempt to produce a proof by coinduction. A coalgebra for an endofunctor F on a category C is just an object of C, say X, together with a map, X \to FX. The best introduction to coalgebra I found was Bart Jacobs Introduction to Coalgebra.

-
I actually came across your post when googling. Unfortunately, the jargon is a bit over my head at this point. :( – Paul Oct 16 '09 at 14:19