21 Nov 2011
Nijmegen, The Netherlands
COIN, or Coalgebra in the Netherlands, is a newly organized seminar
planned to take place alternating at the Radboud University Nijmegen
and the CWI in Amsterdam. The aim of COIN is to bring together
coalgebra researchers from various locations in the Netherlands, and
share current results and questions in the world of coalgebra. We
welcome presentations on any subject related to coalgebra.
COIN is coordinated by Marcello Bonsangue (Leiden University/CWI),
Bart Jacobs (Radboud Universiteit Nijmegen), and Jan Rutten
(CWI/Radboud Universiteit Nijmegen), and its website can be found at
http://homepages.cwi.nl/~winter/coin.html
The first COIN meeting is scheduled for Monday, 21 November 2011, at
CWI, in room L120. The schedule is as follows:
14:30 - 15:15 Dimitri Hendriks (VU) and Jörg Endrullis (VU)
Equational Reasoning and Bisimulation in Coq
15:15 - 16:00 Jan Rutten (CWI/RU)
On the Final Coalgebra of Automatic Sequences
16:15 - 17:00 Marcello Bonsangue (Leiden/CWI)
Coalgebraic Characterizations of Regular and Context-Free
Languages
Abstracts
=========
Dimitri Hendriks (VU) and Jörg Endrullis (VU)
Equational Reasoning and Bisimulation in Coq
--------------------------------------------
We investigate methods for proving in Coq bisimilarity of infinite
objects using coinduction and equational reasoning.
To avoid the introduction of non-normalizable terms, in Coq the
construction of a coinductive object is subjected to a simple
syntactic criterion called guarded corecursion. Every corecursive call
has to be guarded by (to be an argument of) at least one constructor
of the coinductive type we are building a term in, and only by such
constructors. Guardedness ensures productivity (the unique existence
of infinite constructor normal forms), but rejects many productive
specifications. In Coq, proofs are terms, and bisimilarity is defined
as a coinductive type, and so also bisimilarity proofs are forced to
be guarded. However equational reasoning (i.e., rewriting) usually
obstructs guardedness. Typically, applications of transitivity are in
between the guard and the coinduction hypothesis.
We adopt techniques from process algebra and employ the notion of
bisimulations-up-to. Let R be a binary relation on streams, and F a
function from relations to relations. Then R is a bisimulation up-to F
if s R t implies s(0) = t(0) and s' F(R) t'. For certain F this is
sufficient to conclude that R is a subset of ~ (bisimilarity).
Typically R is a subset of F(R), and thus, in comparison with a full
bisimulation, less diagrams have to be checked. We take F(R) to be the
least relation including R and ~, and closed under causal contexts,
and under transitivity and symmetry. For this F we show that if R is a
bisimulation up-to F, then F(R) is a subset of ~. We show that
causality can be proved using techniques to prove productivity.
This method allows for an elegant rendering of equational, coinductive
proofs, and avoids the troubles with guardedness.
Jan Rutten (CWI/Radboud Universiteit Nijmegen)
On the Final Coalgebra of Automatic Sequences
---------------------------------------------
Streams are omnipresent in both mathematics and theoretical computer
science. Automatic sequences form a particularly interesting class of
streams that live in both worlds at the same time: they are defined in
terms of finite automata, which are basic computational structures in
computer science; and they appear in mathematics in many different
ways, for instance in number theory. Examples of automatic sequences
include the celebrated Thue- Morse sequence and the Rudin-Shapiro
sequence.
In this talk, we shall apply the coalgebraic perspective on streams to
automatic sequences. We shall show that the set of automatic sequences
carries a final coalgebra structure, consisting of the operations of
head, even, and odd. This will allow us to show that automatic
sequences are to (general) streams what rational languages are to
(arbitrary) languages.
This is joint work with Clemens Kupke, Oxford University.
Marcello Bonsangue (Leiden University/CWI)
Coalgebraic Characterizations of Regular and Context-Free Languages
-------------------------------------------------------------------
In this lecture we present coalgebraic characterizations of regular
and context free languages using grammars, behavioural differential
equations and generalized regular expressions in which the Kleene star
is replaced by a unique fixed point operator.