Syntactic Monoids and Their Dual 

Jan Rutten (CWI/RU)

Because of the isomorphism $(X \times A) \rightarrow X \cong X \rightarrow (A \rightarrow X)$, the transition structure of a deterministic automaton with state set $X$ and with inputs from an alphabet A can be viewed both as an algebra and as a coalgebra. This algebra-coalgebra duality goes back to Arbib and Manes, who formulated it as a duality between reachability and observability, and is ultimately based on Kalman’s duality in systems theory between controllability and observability. Recently, it was used to give a new proof of Brzozowski’s minimization algorithm for deterministic automata. In this talk, we will discuss deterministic automata as an elementary and typical example for the combined use of algebraic and coalgebraic methods in computer science. The algebra-coalgebra duality of automata will, more specifically, serve as a common perspective for the study of both varieties and covarieties, which are classes of automata and languages defined by equations and coequations, respectively. Along the way, we will establish a first connection with Eilenberg’s definition of varieties of languages, which is based on the classical, algebraic notion of varieties of (transition) monoids. This is joint work with Adolfo Ballester-Bolinches and Enric Cosme-Llopez (University of Valencia).

Moessner’s Theorem: an Exercise in Coinductive Reasoning in Coq 

Robbert Krebbers (RU)

Slides (PDF)

Moessner’s Theorem describes a construction of the sequence of powers $(1^n, 2^n, 3^n, \dotsc)$, by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. In the process of formalizing the original proof we discovered that Long and Salié’s generalization of Moessner’s Theorem could also be proved using (almost) the same bisimulation.

Combining Bialgebraic Semantics and Equations 

Jurriaan Rot (LIACS/CWI)

Slides (PDF)

It was observed by Turi and Plotkin that structural operational semantics can be studied at the level of universal coalgebra, providing specification formats for well-behaved operations at a general level. We extend this framework with non-structural assignment rules which can express, for example, the syntactic format for structural congruences proposed by Mousavi and Reniers. Our main result is that the operational model of such an extended specification is well-behaved, in the sense that bisimilarity is a congruence and that bisimulation-up-to techniques are sound.