Coalgebraic Semantics for Nominal Automata

This paper provides a coalgebraic approach to the language semantics of regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. These automata 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 this semantics arises 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.