[Prev][Next][Index][Thread]
New technical reports on coinduction
The following technical reports are now
available at ftp.cwi.nl as pub/CWIreports/SEN/SEN-R9901.ps.Z
and pub/CWIreports/SEN/SEN-R9826.ps.Z
(also via my home page: http://www.cwi.nl/~janr):
J.J.M.M. Rutten
Automata, power series, and coinduction:
taking input derivatives seriously (extended abstract)
Technical Report SEN-R9901, CWI, Amsterdam, 1999.
Abstract:
Formal power series, which are functions from
the set of words over an alphabet A to a semiring k,
are viewed coalgebraically.
In summary, this amounts to supplying the set of all power series
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 of operators on power series
take the shape of what we have called
behavioural differential equations,
after Brzozowski's notion of input derivative, and include
many classical differential equations for analytic functions.
The use of behavioural differential equations leads, amongst others,
to easy definitions of and proofs about both existing and new
operators on power series, as well as to the construction
of finite (syntactic) nondeterministic automata, implementing them.
*************************************************************
J.J.M.M. Rutten
A note on Coinduction and Weak Bisimilarity for While Programs
Technical Report SEN-R9826, CWI, Amsterdam, 1998.
Abstract
An illustration of coinduction in terms of a notion
of weak bisimilarity is presented.
First, an operational semantics O for while programs is defined
in terms of a final automaton. It identifies any two
programs that are weakly bisimilar, and induces in a
canonical manner a compositional model D.
Next O = D is proved by coinduction.
------- End of Forwarded Message