Coinductive Proofs over Streams as CHR Confluence Proofs
Rémy Haemmerlé · 2012
Abstract. Coinduction is an important theoretical tool for defining and reasoning about unbounded data structures (such as streams, infinite trees, rational numbers...), and infinite-behavior systems. Confluence is a fundamental property of Constraint Handling Rules (CHR) since, as in other rewriting formalisms, it guarantees that the computations are not dependent on rule application order, and also because it implies the logical consistency of the program’s declarative view. In this paper, we illustrate how the confluence of CHR can be used to prove universal coinductive properties. In particular we give several examples of bisimulation proofs over streams. 1