The real upshot of coinduction is that it allows you to write /proofs/ of objects that are hard to reason about using induction. In an inductive proof, we: 1.

The real upshot of coinduction is that it allows you to write /proofs/ of objects that are hard to reason about using induction. In an inductive proof, we: 1. prove that the base case holds, step(0). 2. show that if step(n) holds, so does step(n+1). So if we were reasoning about a finite numbers of numbers, we would show that some property P holds for: 1. the empty list, P([]). 2. assuming that some property holds for P(xs), show that the property holds for P(cons(x, xs)). Now assume we want to prove something about an infinite list. What is the base case here? there is no "empty list" to start from, is there? So the proof strategy is as follows: 0. We are trying to prove P(generator), where "generator" is the generator of an infinite list. 1. Assume that P(<<generator>>) holds. 2. Let the generator generate some data. Say it gives us (data, <<rest of generator>>) 3. Show that P(data, <<rest of generator>>) holds. So, now, if we want to use the above "co-inductive" proof to prove something about a program that uses data from a generator, here's how we do it: 1. Let the program run and halt in finite time. Since it's spent finite time, it could only have pulled out a finite amount of data from the generator. So the generator is generator = (data1, data2, ...., data n, <<rest of generator>>) 2. Assume that P(<<rest of generator>>) holds --- we don't know if it holds or not, and our program can't inspect it anyway, so it doesn't matter! (sneaky, eh?) 3. We know that given P(<<rest of generator>>) and data generated from the generator, datan, we can show P((datan, <<rest of generator>>) 3.b Repeat to get P((data (n-1), data n, <<rest of generator>>) 3.c Keep repeating to get P((data 1, data 2, ..., data n, <<rest of generator>>) This is a really powerful idea. If I had to write down a quip to express this idea, here's what I'd say: - Induction proves that _something is true_: It shows that a property holds for the whole object. It can do this because the object is finite. - Coinduction proves that something is _not false_: It shows that a property is not false for some finite prefix of an infinite object. We don't know what happens in the part that is "not observed", and we don't care, either. The distinction really doesn't matter inside a programming language like haskell or LISP because they don't really have proofs. It only matters inside something like Coq or Agda, where we want to reason about programs. There is more I could get into, like how coinduction/copattern matching allows us to prove that a program "will be productive", just as how we can show that a recursive program "will halt" by looking for an argument that becomes smaller. For a taste of this, consider the programs: def fib(n): if fib == 0: return 1 return fib(n-1) + fib(n-2) def loop(n): return loop(n) How do we prove that fib(n) halts while loop(n) does not? Note that fib(n) has a decreasing argument, the size of the number n passed as input gets smaller on each recursive call. On the other hand, the size of the recursive argument in loop(n) remains the same. We can formalize this to get a proof that fib(n) will always halt, as long as the inputs are natural numbers. Now consider a similar case with two coinductive programs: def gen_const(): yield 1 yield from gen_const() def gen_loop(): yield from gen_loop() Which coinductive program will produce output? Clearly, it's going to be gen_const. How do we prove this? The idea is that the recursive (yield from gen_const()) is "guarded" by a (yield 1). So we are guaranteed to make progress (yield a 1) before we recursively call ourselves. On the other hand, in the case of gen_loop(), there's no production happening before the recursive yield, so we won't produce anything in finite time! All of this is completely lost without the reasoning ability of coinduction and a language like Coq, Agda, or Idris that forces you to think about how to prove things about programs. I hope this gives some idea of "why coinduction" --- it's not something that LISPers had figured out in the 70s that the FP people are now fetishizing and renaming. Coinduction is a powerful set of proof techniques to prove things about programs that don't terminate, but make progress: web servers, operating systems, etc. None of these are supposed to "halt". they're supposed to "make progress". Coinduction gives us the mathematical calculus to talk about such objects. It's an "open problem" on how to make Coinduction good to use inside these proof systems. See, for example, paco in Coq, Copatterns in agda, etc. This is still bleeding edge research.