Generalised Coinduction
Falk Bartels · Electronic Notes in Theoretical Computer Science · 2001
We introduce the λ-coiteration schema for a distributive law λ of a functor T over a functor F. Under certain conditions it can be shown to uniquely characterise functions into the carrier of a final F-coalgebra, generalising the basic coiteration schema as given by finality. The duals of primitive recursion and course-of-value iteration, which are known extensions of coiteration, arise as instances of our framework. One can furthermore obtain schemata justifying recursive specifications that involve operators such as addition of power series, regular operators on languages, or parallel and sequential composition of processes. Next, the same type of distributive law λ is used to generalise coinductive proof techniques. To this end, we introduce the notion of a λ-bisimulation relation. It specialises to what could be called bisimulation up-to-equality or bisimulation up-to-context for contexts built from operators of the type mentioned above. We state that every such relation is contained in some larger conventional bisimulation and demonstrate that this principle leads to simpler bisimilarity proofs using less complex relations.