Reasoning About Codata

Download Now Date Added: Apr 2010
Format: PDF

Programmers happily use induction to prove properties of recursive programs. To show properties of co-recursive programs they employ co-induction, but perhaps less enthusiastically. Co-induction is often considered a rather low-level proof method, in particular, as it departs quite radically from equational reasoning. Co-recursive programs are conveniently defined using recursion equations. Suitably restricted, these equations possess unique solutions. Uniqueness gives rise to a simple and attractive proof technique, which essentially brings equational reasoning to the co-world. The authors illustrate the approach using two major examples: streams and infinite binary trees. Both co-inductive types exhibit a rich structure: they are applicative functors or idioms, and they can be seen as memo-tables or tabulations.