mmmodularity!

» by Scott Kilpatrick

Jacobs and Rutten. A Tutorial on (Co)Algebras and (Co)Induction, 1997. (pdf)

* * *

I’ve been trying to brush up on my knowledge of coinduction (in the general sense). In the last paper, the authors make use of a coinductively interpreted inference rule to do some magic with fixed points and recursion. Not knowing what the hell that meant, I needed some background.

This paper, loaded with exposition and free of original research, provides a good foundation for coinductive principles. Jacobs and Rutten first describe induction in terms of algebras on functors: both inductive definitions of functions and inductive proofs of, say, equality. They approach this from the algebraic perspective to facilitate the introduction of coinduction since all of the (algebraic) notions can be dualized. Many examples of inductive/coinductive definitions/proofs are described, both in prose and with diagrams proving commutativity a la category theory.

I highly recommend this paper for its exposition of these fundamentals; I have a much better intuition about induction vs. coinduction now. However, I still have no clue how to interpret the aforementioned coinductive inference rules.