mmmodularity!

» by Scott Kilpatrick

Andrew D. Gordon. A Tutorial on Co-induction and Functional Programming, 1994. (@MSR)

* * *

Aaron Turon recommended this paper in the comments of the last post.

Gordon briefly defines coinduction as a proof principle using greatest fixpoints of monotonic functions — the usual thang — and then builds up a small call-by-name functional language. Divergence is defined coinductively and then proven identical (by coinduction!) to the divergence relation gotten from the small-step semantics.

He then defines a labelled transition system and, naturally, bisimilarity and bisimulation. A couple proofs about stream bisimilarity motivate coinduction as a proof technique; a proof that contextual equivalence equals bisimilarity appeared interesting yet convoluted.

I enjoyed seeing further application of the coinductive proof principle — most generally, that a set X is a subset of the greatest fixpoint of a monotonic function F, if X is contained in F(X) — in the context of a little Haskell-y FP language. (I say “further” because in the Jacobs-Rutten paper they too give proofs about FP-like languages, albeit in a more algebraic, less direct language.) However, my initial curiosity about “coinductive inference rules” remains.