Behavioural differential equations: a coinductive calculus of streams, automata, and power series*1
Abstract
We present a theory of streams (infinite
sequences), automata and languages, and formal power series, in terms
of the notions of homomorphism and bisimulation, which are the
cornerstones of the theory of (universal) coalgebra. This coalgebraic
perspective leads to a unified theory, in which the observation that
each of the aforementioned sets carries a so-called final
automaton structure, plays a central role. Finality forms the basis for
both definitions and proofs by coinduction, the coalgebraic counterpart
of induction. Coinductive definitions take the shape of what we have
called behavioural differential equations, after Brzozowski's notion of
input derivative. A calculus is developed for coinductive reasoning
about all of the aforementioned structures, closely resembling calculus
from classical analysis.
Author Keywords: Coalgebra; Automaton; Homomorphism;
Bisimulation; Finality; Coinduction; Stream; Formal language; Formal
power series; Differential equation; Input derivative
Mathematical subject codes: 68Q10; 68Q55; 68Q85
*1 This paper is a revised version of Technical Report SEN-R0023, CWI, Amsterdam, 2000.
Cite or link using doi
, 