Algebra and Coalgebra in Languages and Automata
An ICTAC 2018 workshop,
Stellenbosch, South Africa, 15 October 2018
Algebra and coalgebra make it possible to address questions about different language classes uniformly and to derive results about them by working out instances of generalities. This workshop is devoted to this methodology.
Talks
Equational Theories for Real-Time Coalgebraic State Machines
Sergey Goncharov (Friedrich-Alexander-Univ. Erlangen-Nürnberg, DE) [DBLP]
Coalgebraic modelling of formal languages is traditionally concerned with systems, which are (a) real-time, i.e. exhibit observable, perpetual, semantically indispensable behaviours and (b) in a suitable sense rational, i.e. do not make use of storage mechanisms. While the former clause is rather difficult to overcome, as it is deeply rooted in the nature of coalgebraic modelling, the latter clause is not an inherent coalgebraic phenomenon, and can thus be relaxed so as to cope with behaviours more complex in the sense of language and complexity theory. In my talk, I will overview recent results on unified coalgebraic treatment of real-time systems over computational effects encapsulated in monads in the style of Moggi. A key feature of our approach is syntactic representations of relevant monads as equational theories, relating our work to Plotking and Power's theory of algebraic effects. This allows for an equational description of effects underlying Turing machines and pushdown automata, as well as their combinations with other effects, such as probability and nondeterminism, in a systematic way, and thus for unifying diverse formalisations previously coached in terms of classical state machines, weighted automata, valence automata and beyond in a uniform coalgebraic framework. I will present a generic Kleene-style theorem as a yardstick result of our theory.
This is based on joint work with Stefan Milius and Alexandra Silva.
CALF: A Categorical Automata Learning Framework
Alexandra Silva (University College London, UK) [DBLP]
Automata learning is a technique that has successfully been applied in verification, with the automaton type varying depending on the application domain. Adaptations of automata learning algorithms for increasingly complex types of automata have to be developed from scratch because there was no abstract theory offering guidelines. This makes it hard to devise such algorithms, and it obscures their correctness proofs. We introduce a simple category-theoretic formalism that provides an appropriately abstract foundation for studying automata learning. Furthermore, our framework establishes formal relations between algorithms for learning, testing, and minimization. We illustrate its generality with two examples: deterministic and weighted automata.
On Compositionally Defined Functions on Regular Expressions
Peter Thiemann (Universität Freiburg, DE) [DBLP]
The Brzozowski derivative is definable as a compositional function on regular expressions. It relies on the auxiliary definition of nullable expressions that is also compositional. We pursue the question why these functions on regular languages exhibit such compositional definitions.
Atoms of Regular Languages
Hellis Tamm (Tallinn University of Technology, EE) [DBLP]
Atoms of regular languages were introduced in 2011 by Brzozowski and Tamm. The atoms of a regular language are non-empty intersections of uncomplemented or complemented left quotients of the language, where each quotient appears in a term of the intersection. Every regular language defines a unique nondeterministic finite automaton (NFA), the atomaton, whose states are the atoms of the language.
In this talk, I will present an overview of the main research results that have been obtained about atoms since their introduction. Besides basic properties of atoms, this includes the following subtopics: quotient complexity of atoms, reinterpretation of NFA minimization by Kameda and Weiner in terms of atoms, presenting the lower bound methods for the size of an NFA in terms of quotients and atoms.
I may also discuss some future research related to this topic.
Derivatives of Existentially Regular Trace Languages
Tarmo Uustalu (Reykjavik University, IS / Tallinn University of Technology, EE) [DBLP]
We provide syntactic (expression-level) language derivative operations, both in the styles of Brzozowski and Antimirov, for trace closures of regular word languages wrt. an independence relation on the alphabet. The Brzozowski and Antimirov style derivatives essentially define functional resp. relational small-step operational semantics of an (abstracted) sequential programming language where some instructions, given by the independence relation, can be reordered without any observable consequences. Our development is motivated by the fact that some aspects of relaxed memories can be explained by allowing the threads of a concurrent program to be reordered in this manner.
This is joint work with Hendrik Maarand.
Program
See in the ICTAC conference program.