Programme

• Sjaak Smetsers, 13:30 – 14:15

• Joost Winter, 14:15 – 15:00

• Enric Cosme-Llopez & Jan Rutten, 15:15 – 16:00

Bialgebraic semantics in PVS

Sjaak Smetsers ¹

Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed by Turi and Plotkin both styles of semantics are unified using a single, syntax independent format, known as GSOS, in which the operational rules of a language are specified. From this format, the operational and denotational semantics are derived. The approach of Turi and Plotkin is based on the categorical notion of bialgebras. We have formalized this work in the theorem prover PVS. The latest release of PVS, version 6.0, provides so-called declaration parameters, and our main goal was to investigate whether this new version of PVS is adequately suited for formalizing meta theory. In this talk, I will present the most remarkable aspects of this formalization, and discuss some positive and negative issues we have encountered.

Brzozowski Bialgebras

Joost Winter ²

In this talk, we consider a class of automata that satisfy both linearity (with respect to a commutative semiring $S$) on the output and derivative, and that furthermore satisfy Brzozowski’s product rule

$$\begin{align*} & 1_a = 0 \\ & (xy)_a = x_a y + o(x) y_a \end{align*}$$

for all ‘nonterminals’ $x$ and $y$ and alphabet symbols $a$. These automata, which we call Brzozowski bialgebras, form a category, which is related to (and can in fact be derived from) categories of $\lambda$-bialgebras, sharing some ‘good’ properties with them. More precisely, Brzozowski bialgebras can be seen as (unital, associative) algebras over $S$ together with an automata structure.

We mention some instances of Brzozowski bialgebras, and besides their discussion to distributive laws and $\lambda$-bialgebras, also note the similarity between a Brzozowski bialgebra, and the classical notion of a differential algebra, with the classical product rule being substituted by Brzozowski’s product rule.

Furthermore, Brzozowski bialgebras can be seen (at least intuitively) as monoids in categories of linear automata (extending the way in which unital, associative $S$-algebras can be seen as monoids in the category of $S$-modules), leading us to conjecture that Brzozowski bialgebras, too, can be obtained as monoids in a monoidal category. Here the definition of the tensor (or monoidal) product should be dependent on the precise product rule being used.

The dual equivalence of equations and coequations for automata

• Enric Cosme-Llopez ³
• Jan Rutten ^{2 1}

Joint work with Adolfo Ballester-Bolinches ³.

Because of the isomorphism:

$$(X \times A) \rightarrow X \cong X \rightarrow (A \rightarrow X)$$

the transition structure $t : X \rightarrow (A \rightarrow X)$ 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. Here we will use this algebra-coalgebra duality of automata as a common perspective for the study of equations and coequations.

Equations are sets of pairs of words $(v,w)$ that are satisfied by a state $x$ in $X$ if they lead to the same state: $x_v = x_w$. Dually, coequations are sets of languages and are satisfied by a state $x$ if the language accepted by $x$ belongs to that set.

For every automaton $(X,t)$, we define two new automata: $\mathrm{free}(X,t)$ and $\mathrm{cofree}(X,t)$ that represent, respectively, the greatest set of equations and the smallest set of coequations satisfied by $(X,t)$. Both constructions are shown to be functorial, that is, they act also on automaton homomorphisms. The automaton $\mathrm{free}(X,t)$ is isomorphic to the so-called transition monoid of $(X,t)$ and thereby, $\mathrm{cofree}(X,t)$ can be seen as its dual.

Our main result is that the restrictions of $\mathrm{free}$ and $\mathrm{cofree}$ to, respectively, varieties of languages and to quotients $A^*/C$ of $A^*$ with respect to a congruence relation $C$, form a dual equivalence. In the present context, varieties of languages are sets of – not necessarily regular – languages that are complete atomic Boolean algebras closed under left and right language derivatives.

This duality comes along with a coinduction proof principle, phrased in terms of the new notion of equational bisimulation, with which one can prove that a language belongs to a given variety.