Coalgebraic Semantics for Nominal Automata

TL;DR

This paper develops a coalgebraic framework for understanding the semantics of nominal automata, specifically NOFAs and RNNAs, incorporating name binding and alpha-equivalence, and provides new theoretical insights into coalgebraic trace semantics.

Contribution

It introduces a coalgebraic approach to the semantics of nominal automata, unifying trace and language semantics, and offers a simplified proof for a key coalgebraic result.

Findings

Semantics of NOFAs and RNNAs derived from coalgebraic trace and language semantics.

Established a unified coalgebraic framework for nominal automata.

Provided a more general and simplified proof for coalgebraic initial algebra and terminal coalgebra correspondence.

Abstract

This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. While NOFAs are a straightforward nominal version of non-deterministic automata, RNNAs feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNAs are strings formed by ordinary letters and name binding letters. Bar languages are sets of such words modulo $\alpha$-equivalence, and to every state of an RNNA one associates its accepted bar language. We show that the semantics of NOFAs and RNNAs, respectively, arise both as an instance of the Kleisli-style coalgebraic trace semantics as well as an instance of the coalgebraic language semantics obtained via generalized determinization. On the way we revisit coalgebraic trace semantics in general and give a new compact proof for the main result in that theory stating that an initial algebra for a functor yields the terminal coalgebra for the Kleisli extension of the functor. Our proof requires fewer assumptions on the functor than all previous ones.