Behavioural differential equations : a coinductive calculus of streams, automata, and power series
Streams, (automata and) languages, and formal power series are viewed coalgebraically. In summary, this amounts to supplying these sets with a deterministic automaton structure, which has the universal property of being final. Finality then 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 afore mentioned structures, closely resembling (and at times generalising) calculus from classical analysis.
|COMPUTATION BY ABSTRACT DEVICES (acm F.1), LOGICS AND MEANINGS OF PROGRAMS (acm F.3)|
|Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (msc 68Q10), Semantics (msc 68Q55), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software (theme 1)|
|Software Engineering [SEN]|
Rutten, J.J.M.M. (2000). Behavioural differential equations : a coinductive calculus of streams, automata, and power series. Software Engineering [SEN]. CWI.