[Agda] What is coinduction?

[wren ng thornton]

On 10/4/10 6:57 PM, Gregory Crosswhite wrote:
> Hey everyone,
>
> Would someone be kind enough to give me a brief explanation about what
> the point of Coinduction/Codata is?

As for the reasoning behind it, think about trying to prove that 
functions are safe/terminating. All this applies outside of Agda, for 
partial languages, logic, etc, because we all want to avoid ill-defined 
things.

With induction you have something of finite "size", and you're breaking 
it apart. Thus, if you can prove that every recursive call is given 
something "smaller" than the original input, then you're guaranteed to 
terminate. That is, after a finite number of steps, your inductive 
process will yield some output.

With coinduction you're dealing with something of possibly infinite 
"size". Because it's possibly infinite there's no well-ordering, so 
getting "smaller" isn't guaranteed to terminate. But, if you can prove 
that all the recursive calls are such that after consuming some finite 
portion of input they produce some output, then you know your 
coinductive process will yield some output after a finite number of 
steps (even if it may produce infinite output in the long run). The 
simplest way to prove there's some output after finite input is to 
require that all recursive sites are guarded by a constructor; whence 
the "guarded recursion is corecursion" mantra.

-- 
Live well,
~wren