COIN: Coalgebra in the Netherlands

COIN — Coalgebra in the Netherlands is a bimonthly seminar, to be held on Mondays alternately in Nijmegen and Amsterdam. The aim of COIN is to bring together coalgebra researchers at 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.

Schedule

The next COIN meeting will be in Nijmegen on Monday, 4 June 2012, in room HG00.137 at the Radboud University Nijmegen, from 13:30 until 16:00.

Past talks

Talks and Abstracts

Georgiana Caltais (Reykjavik University Iceland): Final Semantics for Decorated Traces

Slides (PDF)

In concurrency theory, various semantic equivalences on labelled transition systems are based on traces enriched or decorated with some additional observations. They are generally referred to as decorated traces, and examples include ready, failure, trace and complete trace equivalence. In this talk we shall apply the generalized powerset construction in order to give a coalgebraic presentation of decorated trace semantics. This will allow us to provide a uniform notion of canonical, minimal representatives for the various decorated trace equivalences, in terms of final Moore automata. As a consequence, we shall see how proofs of decorated trace equivalence can be given by coinduction, using different types of (Moore-) bisimulation, which is helpful for automation.

This is joint work with Filippo Bonchi (LIP-ENS Lyon), Marcello Bonsangue (Leiden University/CWI), Jan Rutten (CWI/Radboud University Nijmegen), and Alexandra Silva (Radboud University Nijmegen, CWI).

Tomasz Brengos (Warsaw University of Technology): Weak bisimulations for coalgebras over ordered functors

Slides (PDF)

The aim of this talk is to introduce a coalgebraic setting in which it is possible to generalize and compare the two known approaches to weak bisimulation for labelled transition systems. To be more precise, for an ordered functor F and a class of F-coalgebras satisfying some additional properties we define a coalgebraic saturator which will serve as the base for two approaches to generalizing weak bisimulation. Although the two ways of defining weak bisimulation for LTS are known to be equivalent, we will show that in the general setting of ordered functors they do not always have to coincide. We will give sufficient conditions for them to match and present interesting examples of functors and coalgebras where they differ.

Finally, we will talk about restrictions of the generalization and problems for further research.

Clemens Kupke (University of Oxford): Dualities and minimal automata

In my talk I am going to describe how dualities between categories of finite automata (coalgebras) and algebras can be used in order to obtain Brzozowski-like minimisation constructions for different types of (deterministic) automata. In particular, I will focus on linear weighted and probabilistic automata. This is joint work with Nick Bezhanishvili and Prakash Panangaden.

Jörg Endrullis (VU): Causality via productivity / Degree of undecidability of stream equality

Slides (PDF)

The talk consists of two parts:

In part (1) we introduce a concept of relative causality that turns out to be useful in coinductive proofs, in particular using circular coinduction. Moreover, we will establish a link between productivity and causality. Thereby automated methods for proving productivity become applicable for proving (relative) causality.

In part (2) we investigate the degree of undecidability of equality of streams specified by systems of equations. This question has been investigated by G. Rosu in 2006:

"Equality of Streams is a Pi-0-2 complete problem".

However, the results in this paper are based on a peculiar notion of equality. As it turns out, more conventional choices yield entirely different results of significantly higher complexity.

Bart Jacobs (RU): Bases as coalgebras

Slides (PDF)

The free algebra adjunction, between the category of algebras of a monad and the underlying category, induces a comonad on the category of algebras. The coalgebras of this comonad are the topic of study in this talk (following earlier work). It is illustrated how such coalgebras-on-algebras can be understood as bases, decomposing each element x into primitives elements from which x can be reconstructed via the operations of the algebra. This holds in particular for the free vector space monad, but also for other monads. For instance, continuous dcpos or stably continuous frames, where each element is the join of the elements way below it, can be described as such coalgebras. Further, it is shown how these coalgebras-on-algebras give rise to a comonoid structure for copy and delete, and thus to diagonalisation of endomaps like in linear algebra.

Joost Winter (CWI): Generalized context-freeness

Slides (PDF)

We provide a coinductive specification format of algebraic power series, which can be seen as a generalization of a number of existing notions, such as context-free languages, weighted context-free languages, and automatic sequences.

This is done by means of systems of behavioural differential equations in a specific format, which yield exactly this class of sequences. Furthermore, connections are given with and between the various existing notions of algebraic power series.

This is joint work with Jan Rutten (CWI/Radboud University) and Marcello Bonsangue (Leiden University/CWI).

Dimitri Hendriks (VU) and Jörg Endrullis (VU): Equational reasoning and bisimulation in Coq

Slides (PDF)

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/RU): 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/CWI): Coalgebraic characterizations of regular and context-free languages

Slides (PDF)

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.

This is joint work with Jan Rutten (CWI/Radboud University) and Joost Winter (CWI).

Alexandra Silva (RU): Trace Semantics via Determinization

In this talk, we take a fresh look at the topic of trace semantics in the theory of coalgebras. The first development of coalgebraic trace semantics used final coalgebras in Kleisli categories, stemming from an initial algebra in the underlying category. This approach requires some non-trivial assumptions, like dcpo enrichment, which do not always hold, even in cases where one can reasonably speak of traces (like for weighted automata). More recently, it has been noticed that trace semantics can also arise by first performing a determinization construction. We show that the two different views on trace semantics are equivalent, in the examples where both approaches are applicable.

Viktor Winschel (University of Mannheim): Reflexivity and the Lucas Critique in Economics

I present the Lucas critique of policy evaluation in macroeconomics and the epistemological issues that have led into the so called rational expectations revolution in the seventies. After discussing the basic approach of rational expectation models, I argue that the underlying problem of the critique is self-referentiality or reflexivity which is known since the 1920th to be the distinguishing feature of social sciences. I point to various problems of the rational expectations approach and some of its extensions and argue that we have so far essentially tried to cope with the aftereffects of the not properly addressed mathematical reflexivity. Beside the Lucas critique I sketch some additional and essential fields of economics if not the very definition of social sciences that are affected by reflexivity and that are wide open to an approach with coalgebras, Scott domains and category theory in general.

Clemens Grabmayer (Universiteit Utrecht): Automatic Sequences and Zip-Specifications

We consider infinite sequences of symbols, also known as streams, and the decidability question for equality of streams defined in a restricted format. (Some formats lead to undecidable equivalence problems.) This restricted format consists of prefixing a symbol at the head of a stream, of the stream function `zip', and recursion variables. Here `zip' interleaves the elements of two streams alternatingly. The celebrated Thue--Morse sequence is obtained by the succinct `zip-specification'

M = 0 : X     X = 1 : zip(X,Y)     Y = 0 : zip(Y,X)

Our main results are as follows. We establish decidability of equivalence of zip-specifications, by employing bisimilarity of observation graphs based on a suitably chosen cobasis. Furthermore, our analysis, based on term rewriting and coalgebraic techniques, reveals an intimate connection between zip- specifications and automatic sequences. This leads to a new and simple characterization of automatic sequences. The study of zip-specifications is placed in a wider perspective by employing observation graphs in a dynamic logic setting, yielding yet another alternative characterization of automatic sequences.

By the first characterization result, zip-specifications can be perceived as a term rewriting syntax for automatic sequences. For streams s the following are equivalent:

1. s can be specified using zip;
2. s is 2-automatic;
3. s has a finite observation graph using the cobasis (head,even,odd).

Here even and odd are defined by

even(a : s) = a : odd(s)     odd(a : s) = even(s)

The generalization to zip-k specifications (with zip-k interleaving k streams) and to k-automaticity is straightforward.

As a natural extension of the class of automatic sequences, we also consider `zip-mix' specifications that use zips of different arities in one specification. The corresponding notion of automaton employs a state-dependent input-alphabet, with a number representation (n)_A = d_m ... d_0 where the base of digit d_i is determined by the automaton A on input d_{i-1} ... d_0.

Finally we show that equivalence is undecidable for a simple extension of the zip-mix format with projections analogous to even and odd.

Coordinators

• Marcello Bonsangue
• Bart Jacobs
• Jan Rutten

Participating institutions and representatives

	CWI	Joost Winter
	Radboud University Nijmegen	Alexandra Silva
	Leiden University	Marcello Bonsangue
	University of Amsterdam	Yde Venema
	VU University Amsterdam	Jan-Willem Klop
	Eindhoven University of Technology	Erik de Vink

For comments, e-mail to J dot Winter at cwi dot nl.