Presheaves and nominal sets provide alternative abstract models of sets of syntactic objects with free and bound variables, such as λ-terms. One distinguishing feature of the presheaf-based perspective is its elegant syntax-free characterization of substitution using a closed monoidal structure. In this paper, we introduce a corresponding closed monoidal structure on nominal sets, in the spirit of Fiore et al.’s substitution tensor for presheaves over finite sets. To this end, we present a general method to derive a closed monoidal structure on a category from a given action of a monoidal category on that category. We demonstrate that this method not only uniformly recovers known substitution tensors for various kinds of presheaf categories but also yields notions of substitution tensor for nominal sets and their relatives, such as renaming sets. In the process, we shed new light on different incarnations of nominal sets and (pre-)sheaf categories and establish a number of correspondences between them.

Codensity monads provide a universal method to generate complex monads from simple functors. Recently, a wide range of important monads in logic, denotational semantics, and probabilistic computation, such as several incarnations of the ultrafilter monad, the Vietoris monad, and the Giry monad, have been presented as codensity monads, using complex arguments. We propose a unifying categorical approach to codensity presentations of monads, based on the idea of relating the presenting functor to a dense functor via a suitable duality between categories. We prove a general presentation result applying to every such situation and demonstrate that most codensity presentations known in the literature emerge from this strikingly simple duality-based setup, drastically alleviating the complexity of their proofs and in many cases completely reducing them to standard duality results. Additionally, we derive a number of novel codensity presentations using our framework, including the first non-trivial codensity presentations for the filter monads on sets and topological spaces, the lower Vietoris monad on topological spaces, and the expectation monad on sets.

Regular languages - the languages accepted by deterministic finite automata - are known to be precisely the languages recognized by finite monoids. This characterization is the origin of algebraic language theory. In this paper, we generalize the correspondence between automata and monoids to automata with generic computational effects given by a monad, providing the foundations of an effectful algebraic language theory. We show that, under suitable conditions on the monad, a language is computable by an effectful automaton precisely when it is recognizable by (1) an effectful monoid morphism into an effect-free finite monoid, and (2) a monoid morphism into a monad-monoid bialgebra whose carrier is a finitely generated algebra for the monad, the former mode of recognition being conceptually completely new. Our prime application is a novel algebraic approach to languages computed by probabilistic finite automata. Additionally, we derive new algebraic characterizations for nondeterministic probabilistic finite automata and for weighted finite automata over unrestricted semirings, generalizing previous results on weighted algebraic recognition over commutative rings.

Extensions of Stone-type dualities have a long history in algebraic logic and have also been instrumental in proving results in algebraic language theory. We show how to extend abstract categorical dualities via monoidal adjunctions, subsuming various incarnations of classical extended Stone and Priestley duality as special cases, and providing the foundation for two new concrete dualities: First, we investigate residuation algebras, which are lattices with additional residual operators modeling language derivatives algebraically. We show that the subcategory of derivation algebras is dually equivalent to the category of profinite ordered monoids, restricting to a duality between Boolean residuation algebras and profinite monoids. We further refine this duality to capture relational morphisms of profinite ordered monoids, which dualize to natural morphisms of residuation algebras. Second, we apply the categorical extended duality to the discrete setting of sets and complete atomic Boolean algebras to obtain a concrete description for the dual of the category of all small categories.

Abstract Extensions of Stone-type dualities have a long history in algebraic logic and have also been instrumental for proving results in algebraic language theory. We show how to extend abstract categorical dualities via monoidal adjunctions, subsuming various incarnations of classical extended Stone and Priestley duality as a special case. Guided by these categorical foundations, we investigate residuation algebras, which are algebraic models of language derivatives, and show the subcategory of derivation algebras to be dually equivalent to the category of profinite ordered monoids, restricting to a duality between boolean residuation algebras and profinite monoids. We further extend this duality to capture relational morphisms of profinite ordered monoids, which dualize to natural morphisms of residuation algebras.

We propose a novel topological perspective on data languages recognizable by orbit-finite nominal monoids. For this purpose, we introduce pro-orbit-finite nominal topological spaces. Assuming globally bounded support sizes, they coincide with nominal Stone spaces and are shown to be dually equivalent to a subcategory of nominal boolean algebras. Recognizable data languages are characterized as topologically clopen sets of pro-orbit-finite words. In addition, we explore the expressive power of pro-orbit-finite equations by establishing a nominal version of Reiterman's pseudovariety theorem.

Abstract Partition refinement is a method for minimizing automata and transition systems of various types. Recently we have developed a partition refinement algorithm and the tool that is generic in the transition type of the input system and matches the theoretical run time of the best known algorithms for many concrete system types. Genericity is achieved by modelling transition types as functors on sets and systems as coalgebras. Experimentation has shown that memory consumption is a bottleneck for handling systems with a large state space, while running times are fast. We have therefore extended an algorithm due to Blom and Orzan, which is suitable for a distributed implementation to the coalgebraic level of genericity, and implemented it in . Experiments show that this allows to handle much larger state spaces. Running times are low in most experiments, but there is a significant penalty for some.