Algebra and Coalgebra in Computer Science: CALCO 2009

2009 Editors: Alexander Kurz, Andrzej Tarlecki

This special issue is dedicated to the 3rd Conference on Algebra and Coalgebra in Computer Science held in Udine, Italy, from September 6 to 10, 2009. After CALCO 2005 in Swansea, Wales, and CALCO 2007 in Bergen, Norway, this was the third event in the series of bi-annuala CALCO conferences formed by joining CMCS (the International Workshop on Coalgebraic Methods in Computer Science) and WADT (the Workshop on Algebraic Development Techniques). CALCO focuses on foundationala aspects as well as both traditional and emerging uses of algebras and coalgebras in computer science, where the study of algebra and coalgebra relates to the data, process and structural aspects ofp software systems. We hope that this special issue reflects well thesed key aspects of the research in the area.

Proceedings of the conference with the original contributions byd invited speakers and submissions selected by the Programme Committee were published by Springer-Verlag as volume 5728 of Lecture Notes in Computer Science.

Many thanks to the University of Udine and the local Organizing Committee chaired by Marina Lenisa for the very smooth, interesting and enjoyable event!

This special issue, which appears just in time for the next CALCO 2011 to take place in Winchester, UK, from August 30 to September 2, 2011, contains the essentially revised and often considerably extendedn versions of six papers selected from the presentations at CALCO 2009.

All of the papers have undergone the usual refereeing procedure, with a further round (sometimes more than one) of critical review andn careful revision according to the standards of the journal.

We would like to thank the members of the CALCO 2009 Program Committee and the referees of the original submissions and of the revisedP versions for their valuable and constructive comments, whiche contributed to the high quality of the papers.

First of all though, we are grateful to the authors for theire contributions and for their efforts in preparing the final versions of their papers for this special issue.

Alexander Kurz and Andrzej Tarlecki
Guest Editors

1. Relating coalgebraic notions of bisimulation

Sam Staton.

The theory of coalgebras, for an endofunctor on a category, has been proposed as a general theory of transition systems. We investigate and relate four generalizations of bisimulation to this setting, providing conditions under which the four different generalizations coincide. We study transfinite sequences whose limits are the greatest bisimulations.

2. Symbolic and Asynchronous Semantics via Normalized Coalgebras

Filippo Bonchi ; Ugo Montanari.

The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics (that is defined in terms of bisimilarity) is characterized by the final morphism in some category of coalgebras. Since the behaviour of interactive systems is for many reasons infinite, symbolic semantics were introduced as a mean to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, symbolic bisimilarity has a different shape with respect to ordinary bisimilarity, and thus the standard coalgebraic characterization does not work. In this paper, we introduce its coalgebraic models. We will use as motivating examples two asynchronous formalisms: open Petri nets and asynchronous pi-calculus. Indeed, as we have shown in a previous paper, asynchronous bisimilarity can be seen as an instance of symbolic bisimilarity.

3. Being Van Kampen is a universal property

Pawel Sobocinski ; Tobias Heindel.

Colimits that satisfy the Van Kampen condition have interesting exactness properties. We show that the elementary presentation of the Van Kampen condition is actually a characterisation of a universal property in the associated bicategory of spans. The main theorem states that Van Kampen cocones are precisely those diagrams in a category that induce bicolimit diagrams in its associated bicategory of spans, provided that the category has pullbacks and enough colimits.

4. Finitely generated free Heyting algebras via Birkhoff duality and coalgebra

Nick Bezhanishvili ; Mai Gehrke.

Algebras axiomatized entirely by rank 1 axioms are algebras for a functor and thus the free algebras can be obtained by a direct limit process. Dually, the final coalgebras can be obtained by an inverse limit process. In order to explore the limits of this method we look at Heyting algebras which have mixed rank 0-1 axiomatizations. We will see that Heyting algebras are special in that they are almost rank 1 axiomatized and can be handled by a slight variant of the rank 1 coalgebraic methods.

5. Conway games, algebraically and coalgebraically

Furio Honsell ; Marina Lenisa.

Using coalgebraic methods, we extend Conway's theory of games to possibly non-terminating, i.e. non-wellfounded games (hypergames). We take the view that a play which goes on forever is a draw, and hence rather than focussing on winning strategies, we focus on non-losing strategies. Hypergames are a fruitful metaphor for non-terminating processes, Conway's sum being similar to shuffling. We develop a theory of hypergames, which extends in a non-trivial way Conway's theory; in particular, we generalize Conway's results on game determinacy and characterization of strategies. Hypergames have a rather interesting theory, already in the case of impartial hypergames, for which we give a compositional semantics, in terms of a generalized Grundy-Sprague function and a system of generalized Nim games. Equivalences and congruences on games and hypergames are discussed. We indicate a number of intriguing directions for future work. We briefly compare hypergames with other notions of games used in computer science.

6. Semantics of Higher-Order Recursion Schemes

Jiri Adamek ; Stefan Milius ; Jiri Velebil.

Higher-order recursion schemes are recursive equations defining new operations from given ones called "terminals". Every such recursion scheme is proved to have a least interpreted semantics in every Scott's model of \lambda-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite \lambda-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in \lambda-calculus by an endofunctor H\lambda and they explained simultaneous substitution of \lambda-terms by proving that the presheaf of \lambda-terms is an initial H\lambda-monoid. Here we work with the presheaf of rational infinite \lambda-terms and prove that this is an initial iterative H\lambda-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.