Regular Behaviours with Names

TL;DR

This paper studies the behavior of orbit-finite coalgebras on nominal sets, providing conditions for rational fixpoints to lift from set functors and describing rational fixpoints of quotient functors, with applications to automata and infinitary lambda-terms.

Contribution

It introduces conditions under which rational fixpoints lift from set functors to nominal sets and characterizes rational fixpoints of quotient functors using sub-strengths, with applications to binding signatures.

Findings

Rational fixpoints of orbit-finite coalgebras can be lifted under certain conditions.

Sub-strengths enable canonical quotients of rational fixpoints for quotient functors.

Concrete descriptions of rational fixpoints for functors related to infinitary lambda-terms.

Abstract

Nominal sets provide a framework to study key notions of syntax and semantics such as fresh names, variable binding and $\alpha$-equivalence on a conveniently abstract categorical level. Coalgebras for endofunctors on nominal sets model, e.g., various forms of automata with names as well as infinite terms with variable binding operators (such as $\lambda$-abstraction). Here, we first study the behaviour of orbit-finite coalgebras for functors $\bar F$ on nominal sets that lift some finitary set functor $F$. We provide sufficient conditions under which the rational fixpoint of $\bar F$, i.e. the collection of all behaviours of orbit-finite $\bar F$-coalgebras, is the lifting of the rational fixpoint of $F$. Second, we describe the rational fixpoint of the quotient functors: we introduce the notion of a sub-strength of an endofunctor on nominal sets, and we prove that for a functor $G$ with a sub-strength the rational fixpoint of each quotient of $G$ is a canonical quotient of the rational fixpoint of $G$. As applications, we obtain a concrete description of the rational fixpoint for functors arising from so-called binding signatures with exponentiation, such as those arising in coalgebraic models of infinitary $\lambda$-terms and various flavours of automata.