Please note: If you wish to give a talk, told us, and you don't see your name here, please contact us immediately!

Abstracts

Jiri Adamek

On relative final coalgebras

For every algebra a: FA -> A the chain of iterations (a, Fa, FFa,...) yields, whenever it converges, a coalgebra together with a coalgebra-to-algebra homomorphism h into the given algebra. It turns out that h is universal among all such coalgebra-to-algebra homomorphisms. We call the coalgebra thus obtained a coalgebra final relative to the given algebra. We prove that every relative final coalgebra is a fixed point of the functor. And for accessible functors we prove that every algebra defines a relative final coalgebra.

Examples: for classical algebras over a signature the relative final coalgebra is the coalgebra of all unrestricted computations. For the (trivial) final algebra we obtain precisely the final coalgebra. And Scott's original model of lambda-calculus as a continuous lattice was constructed as a relative final coalgebra.

Stefan Millius

CIA structures and the semantics of recursion

Final coalgebras for a functor serve as semantic domains for state based systems of various types. For example, formal languages, streams, non-well-founded sets and behaviors of CCS processes form final coalgebras. In my talk I present a uniform account of the semantics of recursive definitions in final coalgebras by combining two ideas:

1. final coalgebras are also initial completely iterative algebras (cia);
2. additional algebraic operations on final coalgebras may be presented in terms of distributive laws

We first show that a distributive law leads to new extended cia structures on the final coalgebra. Then we introduce the notion of a recursive program scheme for a given distributive law λ, which formalizes recursive function definitions involving operations given by λ. We show that every recursive program scheme for λ has a unique solution in the corresponding extended cia.

Finally we apply this to the four concrete final coalgebras mentioned above; as special instances of our results we obtain:

1. Milner's unique solution theorem for CCS agents and, in addition, the fact that this remains true if the calculus is extended by new process combinators recursively defined from the given ones,
2. that a finite stream circuit defines a unique stream function,
3. unique solutions of recursive function definition on non-well founded sets,
4. definitions of operations on formal languages by distributive laws in a compositional way.

Alexandra Silva

Algebraic Enriched coalgebras

Coalgebra is an abstract framework for the uniform study of different kinds of dynamical systems. An endofunctor F determines both the types of systems (F -coalgebras) and a notion of behavioral equivalence (?F ) amongst them. Many types of transition systems and their equivalences can be captured by a functor F . For example, for deterministic automata the derived equivalence is language equivalence, while for non-deterministic automata is ordinary bisimilarity. The powerset construction is a standard method for converting a non- deterministic automaton into an equivalent deterministic one as far as language is concerned. In this talk, we lift the powerset construction on automata to the more general framework of coalgebras with enriched state spaces. Examples of application include partial Mealy machines, (enriched) Moore automata, and Rabin probabilistic automata.

Jan Rutten

Dijkstra's Continued Concatenations Revisited

We will recall Dijkstra's treatment of stream of the Hamming numbers and then describe them coalgebraically. Thus an example is obtained that is both instructive for beginners and at the same time serves as the basis for generalisations in various directions.

Minghui Ma

Definability in Coalgebraic Graded Modal Logic

Graded modal logic (GML) is subsumed within a large buddle of coalgebraic modal logics. We first introduce the language and coalgebraic semantic for GML. Then we show some preservation results of GML-formulas under homomorphism and CG-bisimulation. Especially, we define the new notion of CG-ultrafilter extension and prove the anti-preservation result. Two main theorems are considered. One is the definability of labelled coalgebras (models), and the other is definability of coalgebras (frames). These are new results for GML which are not consequences of the Goldblatt-Thomason theorem proved by A. Kurz and J. Rosicky (2007).

Jacob Vosmaer

Geometric coalgebraic modal logic and formal topology

joint work with Yde Venema and Steve Vickers

We introduce a generalized T-Vietoris construction on locales for arbitrary weak pullback preserving set functors T, inspired by the Carioca Axiomatization (Bilkova, Palmigiano and Venema, 2008) of Moss's coalgebraic modal logic. For T=P, this gives us the Vietoris construction of (Johnstone, 1982). Surprisingly, one of the three Carioca axioms can be made redundant in this application of coalgebraic techniques (relation lifting) to the domain of point-free topology.

Christian Kissig

Infinite Traces through Coalgebras

Coalgebras for a functor T in the category Set of sets and functions generalise state-based and possibly non-terminating transition systems. Their semantics in the final T-coalgebra defines T-behaviour which identifies precisely T-bisimilar states.

Previous work on generic trace theory has shown that an additional structuring in a Set-monad B introduces branching which subsumes non-determinism, probabilism and graded branching. We call coalgebras with branching type B and transition type T as (B,T)-coalgebras.

Semantics by BT-behaviour turns out to be unsuitable for (B,T)-coalgebras. Jacobs et al defined an alternative semantics by lifting into the Kleisli-category. The so obtained semantics is known as trace semantics. We distinguish semantics in finite and infinite traces. Jacobs gave a uniform definition for the first, but for the latter only in the case of non-deterministic branching.

In this talk we give a first exposition of infinite trace semantics generic for a large class of branching and transition types. We characterise the codomain of infinite trace semantics as Cauchy converging sequences. The characterisation is based on a stratified axiomatisation of infinite traces from T-behaviour and a span which describes whether the continuation in a trace is plausible. In particular cases we can reconstruct a coalgebra structure on the codomain of infinite trace semantics. The coalgebra structure is not final, as infinite trace semantics is not unique.

The most prominent application of infinite trace semantics is in the language theory of automata. We show that the acceptance behaviour of non-deterministic coalgebra automata is an infinite trace semantics. The infinite trace semantics of Jacobs arises as a special case where the automata have a trivial acceptance condition.

Vincenzo Ciancia

Automata and languages with names and binders

We present the results of a preliminary investigation on a theory of automata with names. The recognised languages are (nominal) sets of strings over an alphabet with names. More expressive power is obtained by adding the ability to bind names along transitions. These nominal automata can be represented in two ways: either as coalgebras over the nominal sets by Gabbay and Pitts, or as history dependent automata (Montanari-Pistore).

Using the latter, more compact representation, we can allocate names over a loop. This result in a "finite memory effect" which is made formal by proving that the finite memory automata of Kaminski and Francez can be encoded as history-dependent automata.

On the other hand, translating history-dependent automata along the equivalence between their base category of named sets, and nominal sets, one sees that the resulting automata are infinite, and the recognition process is exactly the set-theoretical one. Therefore, history dependent automata can be seen as a well-behaved class of infinite automata.

It turns out that the recognized languages have an implicit notion of symmetry, which can be used to compress large, symmetric data-sets, by representing groups of permutations using their generators.

Joint work with Emilio Tuosto (Leicester, UK).

List of participants

Jiri Adamek, Marcello Bonsangue, Cecilia Chavez, Vincenzo Ciancia, Helle Hvid Hansen, Daiske Ikegami, Md. Aquil Khan, Christian Kissig, Raul Leal Rodriguez, Minghui Ma, Johannes Marti, Stefan Millius, Dimiter Milushev, Milad Niqui, Jan Rutten, Katsuhiko Sano, Alexandra Silva, Jaap van der Woude, Yde Venema, Jacob Vosmaer.