Quantitative algebras are $Σ$-algebras acting on metric spaces, where operations are nonexpanding. Mardare, Panangaden and Plotkin introduced 1-basic varieties as categories of quantitative algebras presented by quantitative equations. We prove that for the category $\mathsf{UMet}$ of ultrametric spaces such varieties bijectively correspond to strongly finitary monads on $\mathsf{UMet}$. The same holds for the category $\mathsf{Met}$ of metric spaces, provided that strongly finitary endofunctors are closed under composition. For uncountable cardinals $λ$ there is an analogous bijection between varieties of $λ$-ary quantitative algebras and monads that are strongly $λ$-accessible. Moreover, we present a bijective correspondence between $λ$-basic varieties as introduced by Mardare et al and enriched, surjections-preserving $λ$-accesible monads on $\mathsf{Met}$. Finally, for general enriched $λ$-accessible monads on $\mathsf{Met}$ a bijective correspondence to generalized varieties is presented.

The Vietoris space of compact subsets of a given Hausdorff space yields an endofunctor V on the category of Hausdorff spaces. Vietoris polynomial endofunctors on that category are built from V, the identity and constant functors by forming products, coproducts and compositions. These functors are known to have terminal coalgebras and we deduce that they also have initial algebras. We present an analogous class of endofunctors on the category of extended metric spaces, using in lieu of V the Hausdorff functor ℋ. We prove that the ensuing Hausdorff polynomial functors have terminal coalgebras and initial algebras. Whereas the canonical constructions of terminal coalgebras for Vietoris polynomial functors takes ω steps, one needs ω + ω steps in general for Hausdorff ones. We also give a new proof that the closed set functor on metric spaces has no fixed points.

Quantitative Σ-algebras, where Σ is a signature with countable arities, are Σ-algebras equipped with a metric making all operations nonexpanding. They have been studied by Mardare, Panangaden and Plotkin who also introduced c-basic quantitative equations for regular cardinals c. Categories of quantitative algebras that can be presented by such equations for c = ℵ1 are called ω1-varieties. We prove that they are precisely the monadic categories , where is a countably basic monad on the category of metric spaces

Abstract It is well known that classical varieties of $\Sigma$ -algebras correspond bijectively to finitary monads on $\mathsf{Set}$ . We present an analogous result for varieties of ordered $\Sigma$ -algebras, that is, categories of algebras presented by inequations between $\Sigma$ -terms. We prove that they correspond bijectively to strongly finitary monads on $\mathsf{Pos}$ . That is, those finitary monads which preserve reflexive coinserters. We deduce that strongly finitary monads have a coinserter presentation, analogous to the coequalizer presentation of finitary monads due to Kelly and Power. We also show that these monads are liftings of finitary monads on $\mathsf{Set}$ . Finally, varieties presented by equations are proved to correspond to extensions of finitary monads on $\mathsf{Set}$ to strongly finitary monads on $\mathsf{Pos}$ .

An old theorem of Adámek constructs initial algebras for sufficiently cocontinuous endofunctors via transfinite iteration over ordinals in classical set theory. We prove a new version that works in constructive logic, using "inflationary" iteration over a notion of size that abstracts from limit ordinals just their transitive, directed and well-founded properties. Borrowing from Taylor's constructive treatment of ordinals, we show that sizes exist with upper bounds for any given signature of indexes. From this it follows that there is a rich class of endofunctors to which the new theorem applies, provided one admits a weak form of choice (WISC) due to Streicher, Moerdijk, van den Berg and Palmgren, and which is known to hold in the internal constructive logic of many kinds of topos.

Categories equivalent to single-sorted varieties of finitary algebras were characterized in the famous dissertation of Lawvere. We present a new proof of a slightly sharpened version: those are precisely the categories with kernel pairs and reflexive coequalizers having an abstractly finite, effective strong generator. A completely analogous result is proved for varieties of many-sorted algebras provided that there are only finitely many sorts. In case of infinitely many sorts a slightly weaker result is presented: instead of being abstractly finite, the generator is required to consist of finitely presentable objects.

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.

Abstract Finitary monads on Pos are characterized as precisely the free-algebra monads of varieties of algebras. These are classes of ordered algebras specified by inequations in context. Analogously, finitary enriched monads on Pos are characterized: here we work with varieties of coherent algebras which means that their operations are monotone.

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.

For every finitary set functor F we demonstrate that free algebras carry a canonical partial order. In case F is bicontinuous, we prove that the cpo obtained as the conservative completion of the free algebra is the free completely iterative algebra. Moreover, the algebra structure of the latter is the unique continuous extension of the algebra structure of the free algebra. For general finitary functors the free algebra and the free completely iterative algebra are proved to be posets sharing the same conservative completion. And for every recursive equation e in the free completely iterative algebra we present an omega-chain of approximate solutions in the free algebra whose join is the solution of e.

Abstract This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving endofunctors on complete and well-powered categories every coalgebra has a well-founded part, and we provide a new, shorter proof that this is the coreflection in the category of all well-founded coalgebras. We present a new more general proof of Taylor’s General Recursion Theorem that every well-founded coalgebra is recursive, and we study conditions which imply the converse. In addition, we present a new equivalent characterization of well-foundedness: a coalgebra is well-founded iff it admits a coalgebra-to-algebra morphism to the initial algebra.

A number of important set functors have countable initial algebras, but terminal coalgebras are uncountable or even non-existent. We prove that the countable cardinality is an anomaly: every set functor with an initial algebra of a finite or uncountable regular cardinality has a terminal coalgebra of the same cardinality. We also present a number of categories that are algebraically complete and cocomplete, i.e., every endofunctor has an initial algebra and a terminal coalgebra. Finally, for finitary set functors we prove that the initial algebra mu F and terminal coalgebra nu F carry a canonical ultrametric with the joint Cauchy completion. And the algebra structure of mu F determines, by extending its inverse continuously, the coalgebra structure of nu F.

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.

For an endofunctor H on a hyper-extensive category preserving countable coproducts we describe the free corecursive algebra on Y as the coproduct of the terminal coalgebra for H and the free H-algebra on Y. As a consequence, we derive that H is a cia functor, i.e., its corecursive algebras are precisely the cias (completely iterative algebras). Also all functors H(-) + Y are then cia functors. For finitary set functors we prove that, conversely, if H is a cia functor, then it has the form H = W \times (-) + Y for some sets W and Y.

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.

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.

Continuous lattices were characterised by Martín Escardó as precisely those objects that are Kan-injective with respect to a certain class of morphisms. In this paper we study Kan-injectivity in general categories enriched in posets. As an example, ω-CPO's are precisely the posets that are Kan-injective with respect to the embeddings ω ↪ ω + 1 and 0 ↪ 1. For every class $\mathcal{H}$ of morphisms, we study the subcategory of all objects that are Kan-injective with respect to $\mathcal{H}$ and all morphisms preserving Kan extensions. For categories such asTop0andPos, we prove that whenever $\mathcal{H}$ is a set of morphisms, the above subcategory is monadic, and the monad it creates is a Kock–Zöberlein monad. However, this does not generalise to proper classes, and we present a class of continuous mappings inTop0for which Kan-injectivity does not yield a monadic category.

Coproducts of monads on $\Set$ have arisen in both the study of computational effects and universal algebra. We describe coproducts of consistent monads on $\Set$ by an initial algebra formula, and prove also the converse: if the coproduct exists, so do the required initial algebras. That formula was, in the case of ideal monads, also used by Ghani and Uustalu. We deduce that coproduct embeddings of consistent monads are injective; and that a coproduct of injective monad morphisms is injective. Two consistent monads have a coproduct iff either they have arbitrarily large common fixpoints, or one is an exception monad, possibly modified to preserve the empty set. Hence a consistent monad has a coproduct with every monad iff it is an exception monad, possibly modified to preserve the empty set. We also show other fixpoint results, including that a functor (not constant on nonempty sets) is finitary iff every sufficiently large cardinal is a fixpoint.

Bloom and Ésik's concept of iteration theory summarises all equational properties that iteration has in common applications, for example, in domain theory, where to every system of recursive equations, the least solution is assigned. This paper shows that in the coalgebraic approach to iteration, the more appropriate concept is that of a functorial iteration theory (called Elgot theory). These theories have a particularly simple axiomatisation, and all well-known examples of iteration theories are functorial. Elgot theories are proved to be monadic over the category of sets in context (or, more generally, the category of finitary endofunctors of a locally finitely presentable category). This demonstrates that functoriality is an equational property from the perspective of sets in context. In contrast, Bloom and Ésik worked in the base category of signatures rather than sets in context, and there iteration theories are monadic but Elgot theories are not. This explains why functoriality was not included in the definition of iteration theories.

We prove that the iterative construction of initial algebras converges for endofunctors F of many-sorted sets whenever F has an initial algebra. In the case of one-sorted sets, the convergence takes n steps where n is either an infinite regular cardinal or is at most 3. Dually, the existence of a many-sorted terminal coalgebra implies that the iterative construction of a terminal coalgebra converges. Moreover, every endofunctor with a fixed-point pair larger than the number of sorts is proved to have a terminal coalgebra. As demonstrated by James Worell, the number of steps here need not be a cardinal even in the case of a single sort: it is ω + ω for the finite power-set functor. The above results do not hold for related categories, such as graphs: we present non-constructive initial algebras and terminal coalgebras.

Accessible set functors can be presented by signatures and equations as quotients of polynomial functors.We determine how preservation of pullbacks and other related properties (often applied in coalgebra) are re ected in the structure of the system of equations.

Iterative monads were introduced by Calvin Elgot in the 1970's and are those ideal monads in which every guarded system of recursive equations has a unique solution. We prove that every ideal monad has an iterative reflection, that is, an embedding into an iterative monad with the expected universal property. We also introduce the concept of iterativity for algebras for the monad , following in the footsteps of Evelyn Nelson and Jerzy Tiuryn, and prove that is iterative if and only if all free algebras for are iterative algebras.

Several concepts of algebras with solutions of recursive equation systems are compared: CPO-enrichable algebras are proved to be iteration algebras of Z. Ésik, and iteration algebras are a special case of the recently introduced Elgot algebras (which are the monadic algebras for the free iterative monad). Another special case of iteration algebras are the iterative algebras of E. Nelson and J. Tiuryn, which are algebras with unique solutions of all guarded systems. For each of the above classes of algebras an example is provided showing that the inclusion in a wider class is proper.

To use verification tools for reliability analysis of a software component, it is desirable to specify the behavior of the component by a finite-state model. This is often impossible at design time if the component practices unbounded parallelism. In that case, the behavior of the component widely depends on the environment the component is instantiated in. Unfortunately, covering all possible environments results in an infinite-state model. In this paper, we introduce a solution based on the concept of template-to-model transformation: at design time, a developer describes the behavior of the component by a behavior template, which is automatically transformed into a concrete behavior model when the component is instantiated in an environment. As the concrete behavior model is finite-state, it is a suitable input for verification tools

Denotational semantics can be based on algebras with additional structure (order, metric, etc.) which makes it possible to interpret recursive specifications. It was the idea of Elgot to base denotational semantics on iterative theories instead, i.e., theories in which abstract recursive specifications are required to have unique solutions. Later Bloom and Esik studied iteration theories and iteration algebras in which a specified solution has to obey certain axioms. We propose so-called Elgot algebras as a convenient structure for semantics in the present paper. An Elgot algebra is an algebra with a specified solution for every system of flat recursive equations. That specification satisfies two simple and well motivated axioms: functoriality (stating that solutions are stable under renaming of recursion variables) and compositionality (stating how to perform simultaneous recursion). These two axioms stem canonically from Elgot's iterative theories: We prove that the category of Elgot algebras is the Eilenberg-Moore category of the monad given by a free iterative theory.

Iterative theories, which were introduced by Calvin Elgot, formalise potentially infinite computations as unique solutions of recursive equations. One of the main results of Elgot and his coauthors is a description of a free iterative theory as the theory of all rational trees. Their algebraic proof of this fact is extremely complicated. In our paper we show that by starting with ‘iterative algebras’, that is, algebras admitting a unique solution of all systems of flat recursive equations, a free iterative theory is obtained as the theory of free iterative algebras. The (coalgebraic) proof we present is dramatically simpler than the original algebraic one. Despite this, our result is much more general: we describe a free iterative theory on any finitary endofunctor of every locally presentable category .Reportedly, a blow from the welterweight boxer Norman Selby, also known as Kid McCoy, left one victim proclaiming,‘It's the real McCoy!’.

By the Final Coalgebra Theorem of Aczel and Mendler, every endofunctor of the category of sets has a final coalgebra, which, however, may be a proper class. We generalise this to all ‘well-behaved’ categories .

Abstract Dynamic evolution inherently involves dynamic update and the issue of its atomicity. We show how this issue can be addressed in a similar manner to a communication failure via an extension to behavior protocols. First, we discuss the problem of defining a composition operator for behavior protocols so as to be able to reflect communication failures. Classical architecture description languages (ADLs) supporting behavior description, such as Wright and TRACTA, use a CSP‐like parallel composition, which inherently yields only ‘successful traces’ ignoring non‐accepted communication attempts. We show that component composition can produce several different types of behavior errors: bad activity, no activity, and divergence. The key idea behind bad activity is that real programs typically have an asymmetry of roles during event exchange: the caller is considered to be the initiator of the call while the callee has only a passive role. This contrasts with most formal systems, which treat communication symmetrically. We propose a new composition operator, ‘consent’, which reflects these types of errors by producing erroneous traces. By using the consent operator it can be statically determined whether the atomicity of a dynamic update of a component is implicitly guaranteed by the behavior of its current environment. Copyright © 2005 John Wiley & Sons, Ltd.

Reuse is one of the key benefits of components. It inherently means that the functionality of a component may be employed only partially. This triggers the issue whether all of the component's interfaces have to be really bound to the other components in its current environment (missing binding problem). Assuming each of the components is equipped by its behavior protocol (F. Plasil et al., 2002), we show that missing bindings can be statically identified via verification tools, in particular by employing the concept of bad activity error introduced in (J. Adamek et al., 2004).

Every finitary endofunctor of $\Set$ is proved to generate a free iterative theory in the sense of Elgot. This work is based on coalgebras, specifically on parametric corecursion, and the proof is presented for categories more general than just $\Set$ .

A concept of equation morphism is introduced for every endofuctor categories.By dualising, we arrive at a concept of coequation such that covarieties, that is, coequationally specified classes of coalgebras with cofree objects, correspond precisely to comonadic categories. Natural examples of covarieties are presented.

For ω‐continuous endofunctors of Set an ordering of a final coalgebra T is exhibited which makes T a CPO. Moreover, an initial algebra, considered as a canonical subobject of T, hasT as its ideal completion. In more generality, for ω‐continuous endofunctors of locally finitely presentable categories the analogous result holds: here the ordering is considered on the hom‐sets hom(B, T) for all finitely presentable objects B.

Abstract Finitary sketches, i.e., sketches with finite-limit and finite-colimit specifications, are proved to be as strong as geometric sketches, i.e., sketches with finite-limit and arbitrary colimit specifications. Categories sketchable by such sketches are fully characterized in the infinitary first-order logic: they are axiomatizable by σ-coherent theories, i.e., basic theories using finite conjunctions, countable disjunctions, and finite quantifications. The latter result is absolute; the equivalence of geometric and finitary sketches requires (in fact, is equivalent to) the non-existence of measurable cardinals.

Algebraic CPOs naturally generalize to finitely accessible categories, and Scott domains (i.e., consistently complete algebraic CPOs) then correspond to what we call Scott-complete categories: finitely accessible, consistently (co-)complete categories. We prove that the category SCC of all Scott-complete categories and all continuous functors is cartesian closed and provides fixed points for a large collection of endofunctors. Thus, SCC can serve as a basis for semantics of computer languages.

Every accessible category is proved to be sketchable by a sketch with finite colimits. In contrast, a finitely accessible category is presented that cannot be sketched by a finitary sketch, i.e., a sketch with finite limits and finite colimits. Also, a category sketchable by a finitary sketch is found that is not finitely accessible.