Subject: categories: Preprint: Behavioural differential equations: a coinductive calculus of streams, automata, and power series

From: Jan Rutten <[email-masked]>
Date: Mon, 02 Oct 2000 16:26:49 +0200

The following technical report is now
available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R0023.ps.Z
(also via my home page: http://www.cwi.nl/~janr):

J.J.M.M. Rutten
Behavioural differential equations: a coinductive calculus of 
streams, automata, and power series
Technical Report SEN-R0023, CWI, Amsterdam, 2000.

Abstract:
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 aspects of) calculus
from classical analysis.

(This report combines and extends earlier papers
on automata and languages (CONCUR '98) and
formal power series (ICALP '99).)