Coinduction Plain and Simple

TL;DR

This paper simplifies the understanding of coinduction, extends its formalism to other predicates, and proposes practical extensions for functional and logic programming.

Contribution

It generalizes the coinduction proof principle beyond equality, making it more intuitive and applicable to a wider range of predicates.

Findings

Generalized coinduction proof principle to other predicates

Enhanced formalism for specifying codata

Proposed extensions for functional and logic programming

Abstract

Coinduction refers to both a technique for the definition of infinite streams, so-called codata, and a technique for proving the equality of coinductively specified codata. This article first reviews coinduction in declarative programming. Second, it reviews and slightly extends the formalism commonly used for specifying codata. Third, it generalizes the coinduction proof principle, which has been originally specified for the equality predicate only, to other predicates. This generalization makes the coinduction proof principle more intuitive and stresses its closeness with structural induction. The article finally suggests in its conclusion extensions of functional and logic programming with limited and decidable forms of the generalized coinduction proof principle.