Regular Behaviours with Names
Stefan Milius, Lutz Schr\"oder, Thorsten Wi{\ss}mann

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 -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 -abstraction). Here, we first study the behaviour of orbit-finite coalgebras for functors on nominal sets that lift some finitary set functor . We provide sufficient conditions under which the rational fixpoint of , i.e. the collection of all behaviours of orbit-finite -coalgebras, is the lifting of the rational fixpoint of . 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 …
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Logic, Reasoning, and Knowledge · semigroups and automata theory
