A key requirement on any well-behaved process language is its compositionality: behavioural equivalence of processes should be respected by the constructors of the language. Turi and Plotkin’s abstract GSOS provides an elegant bialgebraic framework for modelling rule formats that guarantee compositionality from the outset. Their original results, however, are restricted to compositionality of strong bisimilarity, a rather fine-grained notion of process equivalence. In the present paper, we demonstrate that Turi and Plotkin’s approach also applies to trace equivalence, which only observes external actions of processes. To this end, we revisit the general compositionality result of their original theory and present it in a refined form with regard to the required naturality conditions. This step makes abstract GSOS applicable over Kleisli categories and thereby enables reasoning about compositionality in the setting of coalgebraic trace semantics. As our main contribution, we introduce De Simone laws, a type of GSOS laws over Kleisli categories, and prove that their operational models are compositional for coalgebraic trace equivalence. This result recovers and explains compositionality of the well-known De Simone rule format for labelled transition systems in a natural categorical setting. As a further application, we derive from our general framework a novel De Simone-type format for probabilistic systems, compositional for probabilistic trace equivalence.

König's lemma is a fundamental result about trees with countless applications in mathematics and computer science. In contrapositive form, it states that if a tree is finitely branching and well-founded (i.e. has no infinite paths), then it is finite. We present a coalgebraic version of König's lemma featuring two dimensions of generalization: from finitely branching trees to coalgebras for a finitary endofunctor H, and from the base category of sets to a locally finitely presentable category C, such as the category of posets, nominal sets, or convex sets. Our coalgebraic König's lemma states that, under mild assumptions on C and H, every well-founded coalgebra for H is the directed join of its well-founded subcoalgebras with finitely generated state space -- in particular, the category of well-founded coalgebras is locally presentable. As applications, we derive versions of König's lemma for graphs in a topos as well as for nominal and convex transition systems. Additionally, we show that the key construction underlying the proof gives rise to two simple constructions of the initial algebra (equivalently, the final recursive coalgebra) for the functor H: The initial algebra is both the colimit of all well-founded and of all recursive coalgebras with finitely presentable state space. Remarkably, this result holds even in settings where well-founded coalgebras form a proper subclass of recursive ones. The first construction of the initial algebra is entirely new, while for the second one our approach yields a short and transparent new correctness proof.

Fixed points are a recurring theme in computer science and are often constructed as limits of suitably seeded fixed point iterations. We present the algebra of iterative constructions (AIC) - a purely algebraic approach to reasoning about fixed point iterations of continuous endomaps on complete lattices. AIC allows derivations of constructive fixed point theorems via equational logic and avoids explicit computations with indices. For example, F ◇ F^* ⊥ = ◇ F^* ⊥ states in AIC that sup_n Fⁿ (⊥) - a construction known from the Kleene fixed point theorem - is a fixed point of F. We demonstrate the applicability of AIC by providing algebraic proofs of several well- and less-well-known fixed point theorems: Among others, we prove the Tarski-Kantorovich principle - a generalization of the Kleene fixed point theorem - as well as a fixed point-theoretic generalization of k-induction - a technique used in software verification. We moreover present a novel fixed point theorem. It improves a recent generalization of the Tarski-Kantorovich principle due to Olszewski for obtaining pre- and postfixed points from lattice-theoretic limit inferiors and limit superiors through iterating an endomap on an arbitrary seed element: We identify sufficient continuity conditions on the endomaps so that these limits become proper fixed points. We have mechanized our algebra in Isabelle/HOL. Isabelle’s sledgehammer tool is able to find proofs of the above fixed point theorems fully automatically. Finally, we investigate the completeness of our axiomatization of AIC. We prove that our finite set of finitary axioms is (a) sound but incomplete for standard models of AIC (sequences of elements from a complete lattice) and that (b) a different finite set of infinitary axioms is complete. We also prove that infinitary axioms are unavoidable: there exists no complete axiomatization of standard models given by finitely many finitary axioms.

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.

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which provides off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term (pointed) higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of combinatory logics and the lambda-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances. Extended and updated version of arXiv:2210.13387

Contains fulltext : 334464.pdf (Publisher’s version ) (Open Access)

The bialgebraic abstract GSOS framework by Turi and Plotkin provides an elegant categorical approach to modelling the operational and denotational semantics of programming and process languages. In abstract GSOS, bisimilarity is always a congruence, and it coincides with denotational equivalence. This saves the language designer from intricate, ad-hoc reasoning to establish these properties. The bialgebraic perspective on operational semantics in the style of abstract GSOS has recently been extended to higher-order languages, preserving compositionality of bisimilarity. However, a categorical understanding of bialgebraic denotational semantics according to Turi and Plotkin’s original vision has so far been missing in the higher-order setting. In the present paper, we develop a theory of adequate denotational semantics in higher-order abstract GSOS. The denotational models are parametric in an appropriately chosen semantic domain in the form of a locally final coalgebra for a behaviour bifunctor, whose construction is fully decoupled from the syntax of the language. Our approach captures existing accounts of denotational semantics such as semantic domains built via general step-indexing, previously introduced on a per-language basis, and is shown to be applicable to a wide range of different higher-order languages, e.g. simply typed and untyped languages, or languages with computational effects such as probabilistic or non-deterministic branching.

Coinduction is a widely used technique for establishing behavioural equivalence of programs in higher-order languages. In recent years, the rise of languages with quantitative (e.g. probabilistic) features has led to extensions of coinductive methods to more refined types of behavioural conformances, most notably notions of behavioural distance. To guarantee soundness of coinductive reasoning, one needs to show that the behavioural conformance at hand forms a program congruence, i.e. it is suitably compatible with the operations of the language. This is usually achieved by a complex proof technique known as Howe’s method , which needs to be carefully adapted to both the specific language and the targeted notion of behavioural conformance. We develop a uniform categorical approach to Howe’s method that features two orthogonal dimensions of abstraction: (1) the underlying higher-order language is modelled by an abstract higher-order specification ( AHOS ), a novel and very general categorical account of operational semantics, and (2) notions of behavioural conformance (such as relations or metrics) are modelled via fibrations over the base category of an AHOS. Our main result is a fundamental congruence theorem at this level of generality: Under natural conditions on the categorical ingredients and the operational rules of a language modelled by an AHOS, the greatest behavioural (bi)conformance on its operational model forms a congruence. We illustrate our theory by deriving congruence of bisimilarity and behavioural pseudometrics for probabilistic higher-order languages.

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.

Formal languages over infinite alphabets serve as abstractions of structures and processes carrying data. Automata models over infinite alphabets, such as classical register automata or, equivalently, nominal orbit-finite automata, tend to have computationally hard or even undecidable reasoning problems unless stringent restrictions are imposed on either the power of control or the number of registers. This has been shown to be ameliorated in automata models with name allocation such as regular nondeterministic nominal automata, which allow for deciding language inclusion in elementary complexity even with unboundedly many registers while retaining a reasonable level of expressiveness. In the present work, we demonstrate that elementary complexity survives under extending the power of control to alternation: We introduce regular alternating nominal automata (RANAs), and show that their non-emptiness and inclusion problems have elementary complexity even when the number of registers is unbounded. Moreover, we show that RANAs allow for nearly complete de-alternation, specifically de-alternation up to a single deadlocked universal state. As a corollary to our results, we improve the complexity of model checking for a flavour of Bar-µTL, a fixed-point logic with name allocation over finite data words, by one exponential level.

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.

Reasoning about program equivalence in imperative languages is notoriously challenging, as the presence of states (in the form of variable stores) fundamentally increases the observational power of program terms. The key desideratum for any notion of equivalence is compositionality , guaranteeing that subprograms can be safely replaced by equivalent subprograms regardless of the context. To facilitate compositionality proofs and avoid boilerplate work, one would hope to employ the abstract bialgebraic methods provided by Turi and Plotkin's powerful theory of mathematical operational semantics (a.k.a. abstract GSOS ) or its recent extension by Goncharov et al. to higher-order languages. However, multiple attempts to apply abstract GSOS to stateful languages have thus failed. We propose a novel approach to the operational semantics of stateful languages based on the formal distinction between readers (terms that expect an initial input store before being executed), and writers (running terms that have already been provided with a store). In contrast to earlier work, this style of semantics is fully compatible with abstract GSOS, and we can thus leverage the existing theory to obtain coinductive reasoning techniques. We demonstrate that our approach generates non-trivial compositionality results for stateful languages with first-order and higher-order store and that it flexibly applies to program equivalences at different levels of granularity, such as trace, cost, and natural equivalence.

Levy’s call-by-push-value is a comprehensive programming paradigm that combines elements from functional and imperative programming, supports computational effects and subsumes both call-by-value and call-byname evaluation strategies. In the present work, we develop modular methods to reason about program equivalence in call-by-push-value, and in fine-grain call-by-value, which is a popular lightweight call-by-value sublanguage of the former. Our approach is based on the fundamental observation that presheaf categories of sorted sets are suitable universes to model call-by-(push)-value languages, and that natural, coalgebraic notions of program equivalence such as applicative similarity and logical relations can be developed within. Starting from this observation, we formalize fine-grain call-by-value and call-by-push-value in the higher-order abstract GSOS framework, reduce their key congruence properties to simple syntactic conditions by leveraging existing theory and argue that introducing changes to either language incurs minimal proof overhead.

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.

Abstract We present a systematic approach to logical predicates based on universal coalgebra and higher-order abstract GSOS, thus making a first step towards a unifying theory of logical relations. We start with the observation that logical predicates are special cases of coalgebraic invariants on mixed-variance functors. We then introduce the notion of a locally maximal logical refinement of a given predicate, with a view to enabling inductive reasoning, and identify sufficient conditions on the overall setup in which locally maximal logical refinements canonically exist. Finally, we develop induction-up-to techniques that simplify inductive proofs via logical predicates on systems encoded as (certain classes of) higher-order GSOS laws by identifying and abstracting away from their boiler-plate part.

Logical relations constitute a key method for reasoning about contextual equivalence of programs in higher-order languages. They are usually developed on a per-case basis, with a new theory required for each variation of the language or of the desired notion of equivalence. In the present paper we introduce a general construction of (step-indexed) logical relations at the level of Higher-Order Mathematical Operational Semantics, a highly parametric categorical framework for modeling the operational semantics of higherorder languages. Our main result states that for languages whose weak operational model forms a lax bialgebra, the logical relation is automatically sound for contextual equivalence. Our abstract theory is shown to instantiate to combinatory logics and λ-calculi with recursive types, and to different flavours of contextual equivalence.

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin's bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin's framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws. We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the $λ$-calculus w.r.t. a strong variant of Abramsky's applicative bisimilarity are obtained as instances.

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.

Higher-order abstract GSOS is a recent extension of Turi and Plotkin’s framework of Mathematical Operational Semantics to higher-order languages. The fundamental well-behavedness property of all specifications within the framework is that coalgebraic strong (bi)similarity on their operational model is a congruence. In the present work, we establish a corresponding congruence theorem for weak similarity, which is shown to instantiate to well-known concepts such as Abramsky’s applicative similarity for the λ-calculus. On the way, we develop several techniques of independent interest at the level of abstract categories, including relation liftings of mixed-variance bifunctors and higher-order GSOS laws, as well as Howe’s method.

Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.

Compositionality proofs in higher-order languages are notoriously involved, and general semantic frameworks guaranteeing compositionality are hard to come by. In particular, Turi and Plotkin’s bialgebraic abstract GSOS framework, which has been successfully applied to obtain off-the-shelf compositionality results for first-order languages, so far does not apply to higher-order languages. In the present work, we develop a theory of abstract GSOS specifications for higher-order languages, in effect transferring the core principles of Turi and Plotkin’s framework to a higher-order setting. In our theory, the operational semantics of higher-order languages is represented by certain dinatural transformations that we term pointed higher-order GSOS laws . We give a general compositionality result that applies to all systems specified in this way and discuss how compositionality of the SKI calculus and the λ-calculus w.r.t. a strong variant of Abramsky’s applicative bisimilarity are obtained as instances.

Compositionality of denotational semantics is an important concern in programming semantics. Mathematical operational semantics in the sense of Turi and Plotkin guarantees compositionality, but seen from the point of view of stateful computation it applies only to very fine-grained equivalences that essentially assume unrestricted interference by the environment between any two statements. We introduce the more restrictive stateful SOS rule format for stateful languages. We show that compositionality of two more coarse-grained semantics, respectively given by assuming read-only interference or no interference between steps, remains an undecidable property even for stateful SOS. However, further restricting the rule format in a manner inspired by the cool GSOS formats of Bloom and van Glabbeek, we obtain the streamlined and cool stateful SOS formats, which respectively guarantee compositionality of the two more abstract equivalences.

Infinite words over infinite alphabets serve as models of the temporal development of the allocation and (re-)use of resources over linear time. We approach ω-languages over infinite alphabets in the setting of nominal sets, and study languages of infinite bar strings, i.e. infinite sequences of names that feature binding of fresh names; binding corresponds roughly to reading letters from input words in automata models with registers. We introduce regular nominal nondeterministic Büchi automata (Büchi RNNAs), an automata model for languages of infinite bar strings, repurposing the previously introduced RNNAs over finite bar strings. Our machines feature explicit binding (i.e. resource-allocating) transitions and process their input via a Büchi-type acceptance condition. They emerge from the abstract perspective on name binding given by the theory of nominal sets. As our main result we prove that, in contrast to most other nondeterministic automata models over infinite alphabets, language inclusion of Büchi RNNAs is decidable and in fact elementary. This makes Büchi RNNAs a suitable tool for applications in model checking.

Abstract We introduce a new measure on regular languages: theirnondeterministic syntactic complexity. It is the least degree of any extension of the ‘canonical boolean representation’ of the syntactic monoid. Equivalently, it is the least number of states of anysubatomicnondeterministic acceptor. It turns out that essentially all previous structural work on nondeterministic state-minimality computes this measure. Our approach rests on an algebraic interpretation of nondeterministic finite automata as deterministic finite automata endowed with semilattice structure. Crucially, the latter form a self-dual category.

Nondeterministic automata may be viewed as succinct programs implementing deterministic automata, i.e. complete specifications. Converting a given deterministic automaton into a small nondeterministic one is known to be computationally very hard; in fact, the ensuing decision problem is PSPACE-complete. This paper stands in stark contrast to the status quo. We restrict attention to subatomic nondeterministic automata, whose individual states accept unions of syntactic congruence classes. They are general enough to cover almost all structural results concerning nondeterministic state-minimality. We prove that converting a monoid recognizing a regular language into a small subatomic acceptor corresponds to an NP-complete problem. The NP certificates are solutions of simple equations involving relations over the syntactic monoid. We also consider the subclass of atomic nondeterministic automata introduced by Brzozowski and Tamm. Given a deterministic automaton and another one for the reversed language, computing small atomic acceptors is shown to be NP-complete with analogous certificates. Our complexity results emerge from an algebraic characterization of (sub)atomic acceptors in terms of deterministic automata with semilattice structure, combined with an equivalence of categories leading to succinct representations.

Abstract For every finitary monad $T$ on sets and every endofunctor $F$ on the category of $T$-algebras, we introduce the concept of an ffg-Elgot algebra for $F$, i.e. an algebra admitting coherent solutions for finite systems of recursive equations with effects represented by the monad $T$. The goal is to study the existence and construction of free ffg-Elgot algebras. To this end, we investigate the locally ffg fixed point $\varphi F$, i.e. the colimit of all $F$-coalgebras with free finitely generated carrier, which is shown to be the initial ffg-Elgot algebra. This is the technical foundation for our main result: the category of ffg-Elgot algebras is monadic over the category of $T$-algebras.

Profinite equations are an indispensable tool for the algebraic classification of formal languages. Reiterman’s theorem states that they precisely specify pseudovarieties, i.e., classes of finite algebras closed under finite products, subalgebras and quotients. In this article, Reiterman’s theorem is generalized to finite Eilenberg-Moore algebras for a monad T on a category D: we prove that a class of finite T -algebras is a pseudovariety iff it is presentable by profinite equations. As a key technical tool, we introduce the concept of a profinite monad T ^ associated to the monad T , which gives a categorical view of the construction of the space of profinite terms.

We propose a generic categorical framework for learning unknown formal languages of various types (e.g. finite or infinite words, weighted and nominal languages). Our approach is parametric in a monad T that represents the given type of languages and their recognizing algebraic structures. Using the concept of an automata presentation of T-algebras, we demonstrate that the task of learning a T-recognizable language can be reduced to learning an abstract form of algebraic automaton whose transitions are modeled by a functor. For the important case of adjoint automata, we devise a learning algorithm generalizing Angluin's L*. The algorithm is phrased in terms of categorically described extension steps; we provide for a termination and complexity analysis based on a dedicated notion of finiteness. Our framework applies to structures like ω-regular languages that were not within the scope of existing categorical accounts of automata learning. In addition, it yields new learning algorithms for several types of languages for which no such algorithms were previously known at all, including sorted languages, nominal languages with name binding, and cost functions.

Abstract This paper proposes a new category theoretic account of equationally axiomatizable classes of algebras. Our approach is well-suited for the treatment of algebras equipped with additional computationally relevant structure, such as ordered algebras, continuous algebras, quantitative algebras, nominal algebras, or profinite algebras. Our main contributions are a generic HSP theorem and a sound and complete equational logic, which are shown to encompass numerous flavors of equational axiomizations studied in the literature.

For finite automata as coalgebras in a category C , we study languages they accept and varieties of such languages. This generalizes Eilenberg’s concept of a variety of languages, which corresponds to choosing as C the category of Boolean algebras. Eilenberg established a bijective correspondence between pseudovarieties of monoids and varieties of regular languages. In our generalization, we work with a pair C / D of locally finite varieties of algebras that are predual, i.e., dualize on the level of finite algebras, and we prove that pseudovarieties of D -monoids bijectively correspond to varieties of regular languages in C . As one instance, Eilenberg’s result is recovered by choosing D = sets and C = Boolean algebras. Another instance, Pin’s result on pseudovarieties of ordered monoids, is covered by taking D = posets and C = distributive lattices. By choosing as C amp;equals; D the self-predual category of join-semilattices, we obtain Polák’s result on pseudovarieties of idempotent semirings. Similarly, using the self-preduality of vector spaces over a finite field K , our result covers that of Reutenauer on pseudovarieties of K -algebras. Several new variants of Eilenberg’s theorem arise by taking other predualities, e.g., between the categories of non-unital Boolean rings and of pointed sets. In each of these cases, we also prove a local variant of the bijection, where a fixed alphabet is assumed and one considers local varieties of regular languages over that alphabet in the category C .

The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category $\mathcal D$. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott ($\mathcal D=$ sets), the syntactic ordered monoids of Pin ($\mathcal D =$ posets), the syntactic semirings of Pol\'ak ($\mathcal D=$ semilattices), and the syntactic associative algebras of Reutenauer ($\mathcal D$ = vector spaces). Assuming that $\mathcal D$ is a commutative variety of algebras or ordered algebras, we prove that the syntactic $\mathcal D$-monoid of a language $L$ can be constructed as a quotient of a free $\mathcal D$-monoid modulo the syntactic congruence of $L$, and that it is isomorphic to the transition $\mathcal D$-monoid of the minimal automaton for $L$ in $\mathcal D$. Furthermore, in the case where the variety $\mathcal D$ is locally finite, we characterize the regular languages as precisely the languages with finite syntactic $\mathcal D$-monoids.

In the coalgebraic approach to state-based systems, semantics is captured up to behavioural equivalence by special coalgebras such as the final coalgebra, the final locally finitely presentable coalgebra (Adámek, Milius, and Velebil), or the final locally finitely generated coalgebra (Milius, Pattinson, and Wißmann). The choice of the proper semantic domain is determined by finiteness restrictions imposed on the systems of interest. We propose a unifying perspective by introducing the concept of a final locally (I,M)-presentable coalgebra, where the two parameters I and M determine what a "finite" system is. Under suitable conditions on the categories and type functors, we show that the final locally (I,M)-presentable coalgebra exists and coincides with the initial (I,M)-iterative algebra, thereby putting a common roof over several results on iterative, fg-iterative and completely iterative algebras that were given a separate treatment before.

Eilenberg-type correspondences, relating varieties of languages (e.g., of finite words, infinite words, or trees) to pseudovarieties of finite algebras, form the backbone of algebraic language theory. We show that they all arise from the same recipe: one models languages and the algebras recognizing them by monads on an algebraic category, and applies a Stone-type duality. Our main contribution is a variety theorem that covers e.g. Wilke's and Pin's work on infinity-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two categorical approaches of Bojanczyk and of Adamek et al. In addition we derive new results, such as an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.

The syntactic monoid of a language is generalized to the level of a symmetric monoidal closed category D. This allows for a uniform treatment of several notions of syntactic algebras known in the literature, including the syntactic monoids of Rabin and Scott (D = sets), the syntactic semirings of Polak (D = semilattices), and the syntactic associative algebras of Reutenauer (D = vector spaces). Assuming that D is an entropic variety of algebras, we prove that the syntactic D-monoid of a language L can be constructed as a quotient of a free D-monoid modulo the syntactic congruence of L, and that it is isomorphic to the transition D-monoid of the minimal automaton for L in D. Furthermore, in case the variety D is locally finite, we characterize the regular languages as precisely the languages with finite syntactic D-monoids.

For predual categories C and D we establish isomorphisms between opfibrations representing local varieties of languages in C, local pseudovarieties of D-monoids, and finitely generated profinite D-monoids. The global sections of these opfibrations are shown to correspond to varieties of languages in C, pseudovarieties of D-monoids, and profinite equational theories of D-monoids, respectively. As an application, we obtain a new proof of Eilenberg's variety theorem along with several related results, covering varieties of languages and their coalgebraic modifications, Straubing's C-varieties, fully invariant local varieties, etc., within a single framework.

Eilenberg's variety theorem, a centerpiece of algebraic automata theory, establishes a bijective correspondence between varieties of languages and pseudovarieties of monoids. In the present paper this result is generalized to an abstract pair of algebraic categories: we introduce varieties of languages in a category C, and prove that they correspond to pseudovarieties of monoids in a closed monoidal category D, provided that C and D are dual on the level of finite objects. By suitable choices of these categories our result uniformly covers Eilenberg's theorem and three variants due to Pin, Polák and Reutenauer, respectively, and yields new Eilenberg-type correspondences.