Generalised coinduction

Final coalgebras of a functor F are suited for an abstract description of infinite datatypes and dynamical systems. Functions into such a domain are specified by coinductive definitions. The format these specifications take when their justification is directly based on finality is called the coiteration schema here. In applications it often turns out to be too rigid to allow for a convenient description of the functions under consideration. Thus, generalisations or variations are desired. We introduce a generic ?-coiteration schema that can be instantiated by a distributive law ? of some functor T over F and show that - under mild assumptions on the underlying category - one obtains principles which uniquely characterise arrows into the carrier of a final F-coalgebra as well. Certain instances of ?-coiteration can be shown to specify arrows that fail to be coiterative. Examples are the duals of primitive recursion and course-of-value iteration, which are known extensions of coiteration. One can furthermore obtain schemata justifying recursive specifications that involve operators such as arithmetic operations on power series, regular operators for 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, many instances of which are weaker than the conventional definition of a bisimulation. It specialises e.g. 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 give a proof showing that every ?-bisimulation only contains pairs of bisimilar states. This principle leads to simpler proofs through the use of less complex relations.