arXiv subjects

Stefan Milius

Publications and source records attributed to Stefan Milius.

At least 73 records · Page 4Linked to original sources

arXiv2017

Eilenberg Theorems for Free

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. Numerous such correspondences are known in the literature. We demonstrate 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 $\infty$-languages, the variety theorem for cost functions of Daviaud, Kuperberg, and Pin, and unifies the two previous categorical approaches of Bojańczyk and of Adámek et al. In addition we derive a number of new results, including an extension of the local variety theorem of Gehrke, Grigorieff, and Pin from finite to infinite words.

cs.FL↗

arXiv2016

Regular Behaviours with Names

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 $\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 $λ$-terms and various flavours of automata.

cs.LO↗

arXiv2016

Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion

Motivated by the recent interest in models of guarded (co-)recursion, we study their equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Ésik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading, hopefully, towards future description of classifying theories for guarded recursion.

cs.LO↗

arXiv2016

Complete Elgot Monads and Coalgebraic Resumptions

Monads are extensively used nowadays to abstractly model a wide range of computational effects such as nondeterminism, statefulness, and exceptions. It turns out that equipping a monad with a (uniform) iteration operator satisfying a set of natural axioms allows for modelling iterative computations just as abstractly. The emerging monads are called complete Elgot monads. It has been shown recently that extending complete Elgot monads with free effects (e.g. operations of sending/receiving messages over channels) canonically leads to generalized coalgebraic resumption monads, previously used as semantic domains for non-wellfounded guarded processes. In this paper, we continue the study of the relationship between abstract complete Elgot monads and those that capture coalgebraic resumptions, by comparing the corresponding categories of (Eilenberg-Moore) algebras. To this end we first provide a characterization of the latter category; even more generally, we formulate this characterization in terms of Uustalu's parametrized monads. This is further used for establishing a characterization of complete Elgot monads as precisely those monads whose algebras are coherently equipped with the structure of algebras of coalgebraic resumption monads.

cs.LO↗

arXiv2016

Profinite Monads, Profinite Equations, and Reiterman's Theorem

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 paper Reiterman's theorem is generalised to finite Eilenberg-Moore algebras for a monad T on a variety D of (ordered) algebras: a class of finite T-algebras is a pseudovariety iff it is presentable by profinite (in-)equations. As an application, quasivarieties of finite algebras are shown to be presentable by profinite implications. Other examples include finite ordered algebras, finite categories, finite infinity-monoids, etc.

cs.FL↗

arXiv2015

Syntactic Monoids in a Category

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.

cs.LO↗

arXiv2015

Finitary Corecursion for the Infinitary Lambda Calculus

Kurz et al. have recently shown that infinite $λ$-trees with finitely many free variables modulo $α$-equivalence form a final coalgebra for a functor on the category of nominal sets. Here we investigate the rational fixpoint of that functor. We prove that it is formed by all rational $λ$-trees, i.e. those $λ$-trees which have only finitely many subtrees (up to isomorphism). This yields a corecursion principle that allows the definition of operations such as substitution on rational $λ$-trees.

math.CT↗

arXiv2015

Varieties of Languages in a Category

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, Polak and Reutenauer, respectively, and yields new Eilenberg-type correspondences.

cs.FL↗

arXiv2015

Generalized Eilenberg Theorem I: Local Varieties of Languages

We investigate the duality between algebraic and coalgebraic recognition of languages to derive a generalization of the local version of Eilenberg's theorem. This theorem states that the lattice of all boolean algebras of regular languages over an alphabet Σ closed under derivatives is isomorphic to the lattice of all pseudovarieties of Σ-generated monoids. By applying our method to different categories, we obtain three related results: one, due to Gehrke, Grigorieff and Pin, weakens boolean algebras to distributive lattices, one weakens them to join-semilattices, and the last one considers vector spaces over the binary field.

cs.FL↗

arXiv2014

Simplified Coalgebraic Trace Equivalence

The analysis of concurrent and reactive systems is based to a large degree on various notions of process equivalence, ranging, on the so-called linear-time/branching-time spectrum, from fine-grained equivalences such as strong bisimilarity to coarse-grained ones such as trace equivalence. The theory of concurrent systems at large has benefited from developments in coalgebra, which has enabled uniform definitions and results that provide a common umbrella for seemingly disparate system types including non-deterministic, weighted, probabilistic, and game-based systems. In particular, there has been some success in identifying a generic coalgebraic theory of bisimulation that matches known definitions in many concrete cases. The situation is currently somewhat less settled regarding trace equivalence. A number of coalgebraic approaches to trace equivalence have been proposed, none of which however cover all cases of interest; notably, all these approaches depend on explicit termination, which is not always imposed in standard systems, e.g. LTS. Here, we discuss a joint generalization of these approaches based on embedding functors modelling various aspects of the system, such as transition and braching, into a global monad; this approach appears to cover all cases considered previously and some additional ones, notably standard LTS and probabilistic labelled transition systems.

cs.LO↗

arXiv2014

Coproducts of Monads on Set

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.

cs.LO↗

arXiv2014

Corecursive Algebras, Corecursive Monads and Bloom Monads

An algebra is called corecursive if from every coalgebra a unique coalgebra-to-algebra homomorphism exists into it. We prove that free corecursive algebras are obtained as coproducts of the terminal coalgebra (considered as an algebra) and free algebras. The monad of free corecursive algebras is proved to be the free corecursive monad, where the concept of corecursive monad is a generalization of Elgot's iterative monads, analogous to corecursive algebras generalizing completely iterative algebras. We also characterize the Eilenberg-Moore algebras for the free corecursive monad and call them Bloom algebras.

cs.LO↗

arXiv2014

How to Kill Epsilons with a Dagger -- A Coalgebraic Take on Systems with Algebraic Label Structure

We propose an abstract framework for modeling state-based systems with internal behavior as e.g. given by silent or $ε$-transitions. Our approach employs monads with a parametrized fixpoint operator $\dagger$ to give a semantics to those systems and implement a sound procedure of abstraction of the internal transitions, whose labels are seen as the unit of a free monoid. More broadly, our approach extends the standard coalgebraic framework for state-based systems by taking into account the algebraic structure of the labels of their transitions. This allows to consider a wide range of other examples, including Mazurkiewicz traces for concurrent systems.

cs.LO↗

arXiv2013

Abstract GSOS Rules and a Modular Treatment of Recursive Definitions

Terminal coalgebras for a functor serve as semantic domains for state-based systems of various types. For example, behaviors of CCS processes, streams, infinite trees, formal languages and non-well-founded sets form terminal coalgebras. We present a uniform account of the semantics of recursive definitions in terminal coalgebras by combining two ideas: (1) abstract GSOS rules l specify additional algebraic operations on a terminal coalgebra; (2) terminal coalgebras are also initial completely iterative algebras (cias). We also show that an abstract GSOS rule leads to new extended cia structures on the terminal coalgebra. Then we formalize recursive function definitions involving given operations specified by l as recursive program schemes for l, and we prove that unique solutions exist in the extended cias. From our results it follows that the solutions of recursive (function) definitions in terminal coalgebras may be used in subsequent recursive definitions which still have unique solutions. We call this principle modularity. We illustrate our results by the five concrete terminal coalgebras mentioned above, e.\,g., a finite stream circuit defines a unique stream function.

cs.LO↗

arXiv2013

Guard Your Daggers and Traces: On The Equational Properties of Guarded (Co-)recursion

Motivated by the recent interest in models of guarded (co-)recursion we study its equational properties. We formulate axioms for guarded fixpoint operators generalizing the axioms of iteration theories of Bloom and Esik. Models of these axioms include both standard (e.g., cpo-based) models of iteration theories and models of guarded recursion such as complete metric spaces or the topos of trees studied by Birkedal et al. We show that the standard result on the satisfaction of all Conway axioms by a unique dagger operation generalizes to the guarded setting. We also introduce the notion of guarded trace operator on a category, and we prove that guarded trace and guarded fixpoint operators are in one-to-one correspondence. Our results are intended as first steps leading to the description of classifying theories for guarded recursion and hence completeness results involving our axioms of guarded fixpoint operators in future work.

cs.LO↗

arXiv2013

Well-Pointed Coalgebras

For endofunctors of varieties preserving intersections, a new description of the final coalgebra and the initial algebra is presented: the former consists of all well-pointed coalgebras. These are the pointed coalgebras having no proper subobject and no proper quotient. The initial algebra consists of all well-pointed coalgebras that are well-founded in the sense of Osius and Taylor. And initial algebras are precisely the final well-founded coalgebras. Finally, the initial iterative algebra consists of all finite well-pointed coalgebras. Numerous examples are discussed e.g. automata, graphs, and labeled transition systems.

cs.LO↗

arXiv2012

On the specification of operations on the rational behaviour of systems

Structural operational semantics can be studied at the general level of distributive laws of syntax over behaviour. This yields specification formats for well-behaved algebraic operations on final coalgebras, which are a domain for the behaviour of all systems of a given type functor. We introduce a format for specification of algebraic operations that restrict to the rational fixpoint of a functor, which captures the behaviour of finite systems. In other words, we show that rational behaviour is closed under operations specified in our format. As applications we consider operations on regular languages, regular processes and finite weighted transition systems.

cs.LO↗

arXiv2011

Semantics of Higher-Order Recursion Schemes

Higher-order recursion schemes are recursive equations defining new operations from given ones called "terminals". Every such recursion scheme is proved to have a least interpreted semantics in every Scott's model of λ-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite λ-terms we follow the idea of Fiore, Plotkin and Turi and work in the category of sets in context, which are presheaves on the category of finite sets. Fiore et al showed how to capture the type of variable binding in λ-calculus by an endofunctor Hλand they explained simultaneous substitution of λ-terms by proving that the presheaf of λ-terms is an initial Hλ-monoid. Here we work with the presheaf of rational infinite λ-terms and prove that this is an initial iterative Hλ-monoid. We conclude that every guarded higher-order recursion scheme has a unique uninterpreted solution in this monoid.

cs.LO↗