Corecursion and coinduction: how they relate to recursion and induction [pdf]
The real upshot of coinduction is that it allows you to write &#x2F;proofs&#x2F; of objects that are hard to reason about using induction.<p>In an inductive proof, we:<p>1. prove that the base case holds, step(0).<p>2. show that if step(n) holds, so does step(n+1).<p>So if we were reasoning about a finite numbers of numbers, we would show that some property P holds for:<p>1. the empty list, P([]).<p>2. assuming that some property holds for P(xs), show that the property holds for P(cons(x, xs)).<p>Now assume we want to prove something about an <i>infinite list</i>. What is the base case here? there is no &quot;empty list&quot; to start from, is there?<p>So the proof strategy is as follows:<p>0. We are trying to prove P(generator), where &quot;generator&quot; is the generator of an infinite list.<p>1. Assume that P(&lt;&lt;generator&gt;&gt;) holds.<p>2. Let the generator generate some data. Say it gives us (data, &lt;&lt;rest of generator&gt;&gt;)<p>3. Show that P(data, &lt;&lt;rest of generator&gt;&gt;) holds.<p>So, now, if we want to use the above &quot;co-inductive&quot; proof to prove something about a program that uses data from a generator, here&#x27;s how we do it:<p>1. Let the program run and halt in finite time. Since it&#x27;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, &lt;&lt;rest of generator&gt;&gt;)<p>2. Assume that P(&lt;&lt;rest of generator&gt;&gt;) holds --- we don&#x27;t know if it holds or not, and our program can&#x27;t inspect it anyway, so it doesn&#x27;t matter! (sneaky, eh?)<p>3. We know that given P(&lt;&lt;rest of generator&gt;&gt;) and data generated from the generator, datan, we can show P((datan, &lt;&lt;rest of generator&gt;&gt;)
3.b Repeat to get P((data (n-1), data n, &lt;&lt;rest of 
generator&gt;&gt;)<p>3.c Keep repeating to get P((data 1, data 2, ..., data n, &lt;&lt;rest of generator&gt;&gt;)<p>This is a really powerful idea. If I had to write down a quip to express this idea, here&#x27;s what I&#x27;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&#x27;t know what happens in the part that is &quot;not observed&quot;, and we don&#x27;t care, either.<p>The distinction really doesn&#x27;t matter inside a programming language like haskell or LISP because they don&#x27;t really have proofs. It only matters inside something like Coq or Agda, where we want to <i>reason</i> about programs.<p>There is more I could get into, like how coinduction&#x2F;copattern matching allows us to prove that a program &quot;will be productive&quot;, just as how we can show that a recursive program &quot;will halt&quot; by looking for an argument that becomes smaller.<p>For a taste of this, consider the programs:<p><pre><code>    def fib(n):
       if fib == 0: return 1
       return fib(n-1) + fib(n-2)
    def loop(n): return loop(n) 
</code></pre>
How do we prove that fib(n) halts while loop(n) does not? Note that fib(n) has a <i>decreasing</i> 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.<p>Now consider a similar case with two coinductive programs:<p><pre><code>     def gen_const():
        yield 1
        yield from gen_const()

     def gen_loop():
        yield from gen_loop()
</code></pre>
Which coinductive program will produce output? Clearly, it&#x27;s going to be
gen_const. How do we prove this? The idea is that the recursive (yield from gen_const())
is &quot;guarded&quot; 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&#x27;s no production happening
before the recursive yield, so we won&#x27;t produce anything in finite time!<p>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.<p>I hope this gives some idea of &quot;why coinduction&quot; --- it&#x27;s not something that
LISPers had figured out in the 70s that the FP people are now fetishizing
and renaming.<p>Coinduction is a powerful set of proof techniques to prove
things about programs that don&#x27;t terminate, but make progress:
web servers, operating systems, etc. None of these are supposed to &quot;halt&quot;.
they&#x27;re supposed to &quot;make progress&quot;. Coinduction gives us the mathematical
calculus to talk about such objects.<p>It&#x27;s an &quot;open problem&quot; 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.