Menu
CS

Search

Persons

doc. RNDr. Jiří Velebil, Ph.D.

All publications

A categorical view of varieties of ordered algebras

  • DOI: 10.1017/S0960129521000463
  • Link: https://doi.org/10.1017/S0960129521000463
  • Department: Department of Mathematics
  • Annotation:
    It is well known that classical varieties of Sigma-algebras correspond bijectively to finitary monads on 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 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 linings of finitary monads on Set. Finally, varieties presented by equations are proved to correspond to extensions of finitary monads on Set to strongly finitary monads on Pos.

EXTENDING SET FUNCTORS TO GENERALISED METRIC SPACES

  • Authors: Balan, A., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Logical Methods in Computer Science. 2019, 15(1), 1-57. ISSN 1860-5974.
  • Year: 2019
  • DOI: 10.23638/LMCS-15(1:5)2019
  • Link: https://doi.org/10.23638/LMCS-15(1:5)2019
  • Department: Department of Mathematics
  • Annotation:
    For a commutative quantale V, the category V-cat can be perceived as a category of generalised metric spaces and non-expanding maps. We show that any type constructor T (formalised as an endofunctor on sets) can be extended in a canonical way to a type constructor T-V,- on V-cat. The proof yields methods of explicitly calculating the extension in concrete examples, which cover well-known notions such as the Pompeiu-Hausdorff metric as well as new ones.

A PRESENTATION OF BASES FOR PARAMETRIZED ITERATIVITY

  • Department: Department of Mathematics
  • Annotation:
    Finitary monads on a locally finitely presentable category A are wellknown to possess a presentation by signatures and equations. Here we prove that, analogously, bases on A , i.e., finitary functors from A to the category of finitary monads on A , possess a presentation by parametrized signatures and equations.

An institutional approach to positive coalgebraic logic

  • Authors: Balan, A., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Journal of Logic and Computations. 2017, 27(6), 1799-1824. ISSN 0955-792X.
  • Year: 2017
  • DOI: 10.1093/logcom/exv074
  • Link: https://doi.org/10.1093/logcom/exv074
  • Department: Department of Mathematics
  • Annotation:
    Positive modal logic, as introduced by Dunn in 1995, is the negation-free fragment of the standard modal logic of all Kripke frames. Positive coalgebraic logic, introduced by the authors in a previous work, expands the above result from Kripke frames to more general transition systems, namely to coalgebras of weak-pullback preserving functors. We show that this construction is both modular and uniform in the functor giving the type of coalgebra. More precisely, we formalize both Set and Pos-based coalgebraic modal logic as institutions, and we exhibit a morphism of institutions between them giving the positive fragment of coalgebraic modal logic.

Quasivarieties and varieties of ordered algebras: regularity and exactness

  • Authors: Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Mathematical Structures in Computer Science. 2017, 27(7), 1153-1194. ISSN 0960-1295.
  • Year: 2017
  • DOI: 10.1017/S096012951500050X
  • Link: https://doi.org/10.1017/S096012951500050X
  • Department: Department of Mathematics
  • Annotation:
    We characterise quasivarieties and varieties of ordered algebras categorically in terms of regularity, exactness and the existence of a suitable generator. The notions of regularity and exactness need to be understood in the sense of category theory enriched over posets. We also prove that finitary varieties of ordered algebras are cocompletions of their theories under sifted colimits (again, in the enriched sense).

Morita Equivalence for Many-Sorted Enriched Theories

  • DOI: 10.1007/s10485-015-9406-y
  • Link: https://doi.org/10.1007/s10485-015-9406-y
  • Department: Department of Mathematics
  • Annotation:
    Morita equivalence detects the situation in which two different theories admit the same class of models for the given theories. We generalise the result of Adamek, Sobral and Sousa concerning Morita equivalence of many-sorted algebraic theories. This generalisation is two-fold. We work in an enriched setting, so the result is parametric in the choice of enrichment. Secondly, the result works for a reasonably general notion of a theory: the class of limits in the theory can be varied. As an example of an application of our result, we show enriched and many-sorted Morita equivalence results, and we recover the known results in the ordinary case.

Relation lifting, a survey

  • Authors: Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Journal of Logical and Algebraic Methods in Programming. 2016, 85(4), 475-499. ISSN 2352-2208.
  • Year: 2016
  • DOI: 10.1016/j.jlamp.2015.08.002
  • Link: https://doi.org/10.1016/j.jlamp.2015.08.002
  • Department: Department of Mathematics
  • Annotation:
    We survey work in category theory and coalgebra on how to extend a functor from maps to relations. This relation lifting has a universal property, which is presented in some detail and guides us to generalisations to monotone and many-valued relations. As applications, it is shown how different notions of bisimulation, simulation and modal logics do arise. (C) 2016 Elsevier Inc. All rights reserved.

Extensions of functors from Set to V-cat

  • Authors: Balan, A., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Leibniz International Proceedings in Informatics. Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2015. pp. 17-34. ISSN 1868-8969. ISBN 978-3-939897-84-2.
  • Year: 2015
  • DOI: 10.4230/LIPIcs.CALCO.2015.17
  • Link: https://doi.org/10.4230/LIPIcs.CALCO.2015.17
  • Department: Department of Mathematics
  • Annotation:
    We show that for a commutative quantale V every functor Set --> V-cat has an enriched left Kan extension. As a consequence, coalgebras over Set are subsumed by coalgebras over V-cat. Moreover, one can build functors on V-cat by equipping Set-functors with a metric.

Kan injectivity in order-enriched categories

  • Authors: Adámek, J., Sousa, L., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Mathematical Structures in Computer Science. 2015, 25(1), 6-45. ISSN 0960-1295.
  • Year: 2015
  • DOI: 10.1017/S0960129514000024
  • Link: https://doi.org/10.1017/S0960129514000024
  • Department: Department of Mathematics
  • Annotation:
    Continuous lattices were characterised by Martin Escardo 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. For every class H of morphisms, we study the subcategory of all objects that are Kan-injective with respect to H and all morphisms preserving Kan extensions. For categories such as Top_0 and Pos, we prove that whenever H is a set of morphisms, the above subcategory is monadic, and the monad it creates is a Kock-Z¨oberlein monad. However, this does not generalise to proper classes, and we present a class of continuous mappings in Top_0 for which Kan-injectivity does not yield a monadic category.

Positive fragments of coalgebraic logics

  • Authors: Balan, A., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Logical Methods in Computer Science. 2015, 11(3), 1-51. ISSN 1860-5974.
  • Year: 2015
  • DOI: 10.2168/LMCS-11(3:18)2015
  • Link: https://doi.org/10.2168/LMCS-11(3:18)2015
  • Department: Department of Mathematics
  • Annotation:
    Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn’s result from Kripke frames to coalgebras for weak-pullback preserving functors.

Base modules for parametrized iterativity

  • Authors: Adamek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Theoretical Computer Science. 2014, 2014(523), 56-85. ISSN 0304-3975.
  • Year: 2014
  • DOI: 10.1016/j.tcs.2013.12.019
  • Link: https://doi.org/10.1016/j.tcs.2013.12.019
  • Department: Department of Mathematics
  • Annotation:
    Abstrakt: The concept of a base, that is a parametrized finitary monad, which we introduced earlier, followed the footsteps of Tarmo Uustalu in his attempt to formalize parametrized recursion. We proved that for every base free iterative algebras exist, and we called the corresponding monad the rational monad of the base. Here we introduce modules for a base, and we prove that the rational monad of a base gives rise to a canonical module, that is characterized as the free iterative module on the given base.

Enriched Logical Connections

  • DOI: 10.1007/s10485-011-9267-y
  • Link: https://doi.org/10.1007/s10485-011-9267-y
  • Department: Department of Mathematics
  • Annotation:
    Abstract: In the setting of enriched category theory, we describe dual adjunctions of the form Ldashv R:Spa^op --> Alg between the dual of the category Spa of ``spaces'' and the category Alg of ``algebras'' that arise from a schizophrenic object Omega, which is both an ``algebra'' and a ``space''. We call such adjunctions logical connections. We prove that the exact nature of Omega is that of a module that allows to lift optimally the structure of a ``space'' and an ``algebra'' to certain diagrams. Our approach allows to give a unified framework known from logical connections over the category of sets and analyzed, e.g., by Hans Porst and Walter Tholen, with future applications of logical connections in coalgebraic logic and elsewhere, where typically, both the category of ``spaces'' and the category of ``algebras'' consist of ``structured presheaves`'.

How iterative reflections of monads are constructed

  • DOI: 10.1016/j.ic.2013.02.003
  • Link: https://doi.org/10.1016/j.ic.2013.02.003
  • Department: Department of Mathematics
  • Annotation:
    Every ideal monad M on the category of sets is known to have a reflection hat{M} in the category of all iterative monads of Elgot. Here we describe the iterative reflection hat{M} as the monad of free iterative Eilenberg-Moore algebras for M. This yields numerous concrete examples: if M is the free-semigroup monad, then hat{M} is obtained by adding a single absorbing element; if M is the monad of finite trees then hat{M} is the monad of rational trees, etc.

Positive Fragments of Coalgebraic Logics

  • Authors: Balan, A., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Algebra and Coalgebra in Computer Science. Berlin: Springer, 2013. pp. 51-65. Lecture Notes in Computer Science.. ISBN 978-3-642-40205-0.
  • Year: 2013
  • DOI: 10.1007/978-3-642-40206-7_6
  • Link: https://doi.org/10.1007/978-3-642-40206-7_6
  • Department: Department of Mathematics
  • Annotation:
    Positive modal logic was introduced in an influential 1995 paper of Dunn as the positive fragment of standard modal logic. His completeness result consists of an axiomatization that derives all modal formulas that are valid on all Kripke frames and are built only from atomic propositions, conjunction, disjunction, box and diamond. In this paper, we provide a coalgebraic analysis of this theorem, which not only gives a conceptual proof based on duality theory, but also generalizes Dunn's result from Kripke frames to coalgebras of weak-pullback preserving functors. For possible application to fixed-point logics, it is note-worthy that the positive coalgebraic logic of a functor is given not by all predicate-liftings but by all monotone predicate liftings.

Relation lifting, with an application to the many-valued cover modality

  • Authors: Bílková, M., Kurz, A., Petrisan, D., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Logical Methods in Computer Science. 2013, 9(4:8), 1-48. ISSN 1860-5974.
  • Year: 2013
  • DOI: 10.2168/LMCS-9(4:8)2013
  • Link: https://doi.org/10.2168/LMCS-9(4:8)2013
  • Department: Department of Mathematics
  • Annotation:
    We introduce basic notions and results about relation liftings on categories enriched in a commutative quantale. We derive two necessary and sufficient conditions for a 2-functor T to admit a functorial relation lifting: one is the existence of a distributive law of T over the "powerset monad" on categories, one is the preservation by T of "exactness" of certain squares. Both characterisations are generalisations of the "classical" results known for set functors: the first characterisation generalises the existence of a distributive law over the genuine powerset monad, the second generalises preservation of weak pullbacks. The results presented in this paper enable us to compute predicate liftings of endofunctors of, for example, generalised (ultra)metric spaces. We illustrate this by studying the coalgebraic cover modality in this setting.

Distributive substructural logics as coalgebraic logics over posets

  • Authors: Bílková, M., Horčík, R., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Advances in Modal Logic 2012. London: King's College, 2012. pp. 119-142. College Publications. ISBN 978-1-84890-068-4.
  • Year: 2012
  • Department: Department of Mathematics
  • Annotation:
    We show how to understand frame semantics >> of distributive substructural logics coalgebraically, >> thus opening a possibility to study them as coalgebraic >> logics. As an application of this approach we prove >> a general version of Goldblatt-Thomason theorem >> that characterizes definability of classes of frames >> for logics extending the distributive Full Lambek logic, >> as e.g. relevance logics, many-valued logics or >> intuitionistic logic. The paper is rather conceptual >> and does not claim to contain signicant new results. >> We consider a category of frames as posets equipped >> with monotone relations, and show that they can be >> understood as coalgebras for an endofunctor of the >> category of posets. In fact, we adopt a more general >> definition of frames that allows to cover a wider class >> of distributive modal logics

Expressiveness of positive coalgebraic logic

  • Authors: Kapulkin, K., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Advances in Modal Logic 2012. London: King's College, 2012. pp. 368-385. College Publications. ISBN 978-1-84890-068-4.
  • Year: 2012
  • Department: Department of Mathematics
  • Annotation:
    From the point of view of modal logic, coalgebraic logic >> over posets is the natural coalgebraic generalisation of positive >> modal logic. From the point of view of coalgebra, >> posets arise if one is interested in simulations as opposed to >> bisimulations. From a categorical point of view, one moves from >> ordinary categories to enriched categories. >> We show that the basic setup of coalgebraic logic extends >> to this more general setting and that every finitary functor >> on posets has a logic that is expressive, that is, has >> the Hennessy-Milner property.

On coalgebraic logic over posets

  • Department: Department of Mathematics
  • Annotation:
    We relate the abstract coalgebraic logic >> for finitary Set-functors with the corresponding logic >> for their Pos-extensions. Namely, we prove that for >> a finitary Set-functor T preserving weak pullbacks >> and its posetification T', the coalgebraic modal logic >> L' of T' is a positive fragment of the coalgebraic >> modal logic L of T.

Elgot theories: A new perspective on the equational properties of iteration

  • Authors: Adámek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Mathematical Structures in Computer Science. 2011, 2011(21), 417-480. ISSN 0960-1295.
  • Year: 2011
  • DOI: 10.1017/S0960129510000496
  • Link: https://doi.org/10.1017/S0960129510000496
  • Department: Department of Mathematics
  • Annotation:
    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

Equational presentations of functors and monads

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Kurz, A.
  • Publication: Mathematical Structures in Computer Science. 2011, 2011(21), 363-381. ISSN 0960-1295.
  • Year: 2011
  • DOI: 10.1017/S0960129510000575
  • Link: https://doi.org/10.1017/S0960129510000575
  • Department: Department of Mathematics
  • Annotation:
    We study equational presentations of functors and monads defined on a category K that is equipped by an adjunction F -| U : K -~ X of descent type. We present a class of functors/monads that admit such an equational presentation that involves finitary signatures in X. We apply these results to an equational description of functors arising in various areas of theoretical computer science.

Final coalgebras in accessible categories

  • Authors: Karazeris, P., Matzaris, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Mathematical Structures in Computer Science. 2011, 21(5), 1067-1108. ISSN 0960-1295.
  • Year: 2011
  • DOI: 10.1017/S0960129511000351
  • Link: https://doi.org/10.1017/S0960129511000351
  • Department: Department of Mathematics
  • Annotation:
    We propose a construction of the final coalgebra for a finitary endofunctor of a finitely accessible category and study conditions under which this construction is available. Our conditions always apply when the accessible category is cocomplete, and is thus a locally finitely presentable (l.f.p.) category, and we give an explicit and uniform construction of the final coalgebra in this case. On the other hand, our results also apply to some interesting examples of final coalgebras beyond the realm of l.f.p. categories. In particular, we construct the final coalgebra for every finitary endofunctor on the category of linear orders, and analyse Freyd's coalgebraic characterisation of the closed unit as an instance of this construction. We use and extend results of Tom Leinster, developed for his study of self-similar objects in topology, relying heavily on his formalism of modules (corresponding to endofunctors) and complexes for a module.

On monotone modalities and adjointness

  • Authors: Bílková, M., doc. RNDr. Jiří Velebil, Ph.D., Venema, Y.
  • Publication: Mathematical Structures in Computer Science. 2011, 2011(21), 383-416. ISSN 0960-1295.
  • Year: 2011
  • DOI: 10.1017/S0960129510000514
  • Link: https://doi.org/10.1017/S0960129510000514
  • Department: Department of Mathematics
  • Annotation:
    We fix a logical connection (Stone -| Pred : Set^op -> BA given by 2 as a schizophrenic object) and study coalgebraic modal logic that is induced by a functor T : Set -> Set that is finitary and standard and preserves weak pullbacks and finite sets. We prove that for any such T, the cover modality nabla is a left (and its dual delta is a right) adjoint relative to P_omega. We then consider monotone unary modalities arising from the logical connection and show that they all are left (or right) adjoints relative to P_omega.

On second-order iterative monads

  • Authors: Adámek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Theoretical Computer Science. 2011, 412(38), 4969-4988. ISSN 0304-3975.
  • Year: 2011
  • DOI: 10.1016/j.tcs.2011.04.027
  • Link: https://doi.org/10.1016/j.tcs.2011.04.027
  • Department: Department of Mathematics
  • Annotation:
    B. Courcelle studied algebraic trees as precisely the solutions of all recursive program schemes for a given signature in Set. He proved that the corresponding monad is iterative. We generalize this to recursive program schemes over a given unitary endofunctor H of a "suitable" category. A monad is called second-order iterative if every guarded recursive program scheme has a unique solution in it. We construct two second-order iterative monads: one, called the second-order rational monad, S(H), is proved to be the initial second-order iterative monad. The other one, called the context-free monad, C(H), is a quotient of S(H) and in the original case of a polynomial endofunctor H of Set we prove that C(H) is the monad studied by B. Courcelle. The question whether these two monads are equal is left open. (C) 2011 Elsevier B.V. All rights reserved.

Relation liftings on preorders and posets

  • Authors: Bílková, M., Kurz, A., Petrisan, D., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Proceedings of CALCO 2011. Berlin: Springer-Verlag, 2011. pp. 115-129. Springer Lecture Notes in Computer Science series.. ISSN 0302-9743. ISBN 978-3-642-22943-5.
  • Year: 2011
  • DOI: 10.1007/978-3-642-22944-2_9
  • Link: https://doi.org/10.1007/978-3-642-22944-2_9
  • Department: Department of Mathematics
  • Annotation:
    The category Rel(Set) of sets and relations can be described as a category of spans and as the Kleisli category for the powerset monad. A set-functor can be lifted to a functor on Rel(Set) iff it preserves weak pullbacks. We show that these results extend to the enriched setting, if we replace sets by posets or preorders. Preservation of weak pullbacks becomes preservation of exact lax squares. As an application we present Moss’s coalgebraic over posets

Semantics of higher-order recursion schemes

  • Authors: Adámek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Logical Methods in Computer Science. 2011, 2011(7), 1-43. ISSN 1860-5974.
  • Year: 2011
  • DOI: 10.2168/LMCS-7(1:15)2011
  • Link: https://doi.org/10.2168/LMCS-7(1:15)2011
  • Department: Department of Mathematics
  • Annotation:
    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 lambda-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite lambda-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 lambda-calculus by an endofunctor H and they explained simultaneous substitution of lambda-terms by proving that the presheaf of lambda-terms is an initial H-monoid. Here we work with the presheaf of rational infinite lambda-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.

Algebraic Theories over Nominal Sets

  • Department: Department of Mathematics
  • Annotation:
    We investigate the foundations of a theory of algebraic data types with variable binding inside classical universal algebra. In the first part, a category-theoretic study of monads over the nominal sets of Gabbay and Pitts leads us to introduce new notions of finitary based monads and uniform monads. In a second part we spell out these notions in the language of universal algebra, show how to recover the logics of Gabbay-Mathijssen and Clouston-Pitts, and apply classical results from universal algebra.

Equational Properties of Iterative Monads

  • Authors: Adámek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Information and Computation. 2010, 208(12), 1306-1348. ISSN 0890-5401.
  • Year: 2010
  • DOI: 10.1016/j.ic.2009.10.006
  • Link: https://doi.org/10.1016/j.ic.2009.10.006
  • Department: Department of Mathematics
  • Annotation:
    Iterative monads of Calvin Elgot were introduced to treat the semantics of recursive equations purely algebraically. They are Lawvere theories with the property that all ideal systems of recursive equations have unique solutions. We prove that the unique solutions in iterative monads satisfy all the equational properties of iteration monads of Stephen Bloom and Zoltán Ésik, whenever the base category is hyper-extensive and locally finitely presentable. This result is a step towards proving that functorial iteration monads form a monadic category over sets in context. This shows that functoriality is an equational property when considered w.r.t. sets in context.

Expressivity of Coalgebraic Logic over Posets

  • Authors: Kapulkin, K., Kurz, A., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Short contributions CMCS 2010''. Amsterdam: CWI, Centrum Wiskunde & Informatica, 2010. pp. 16-17. ISSN 1386-369X.
  • Year: 2010
  • Department: Department of Mathematics
  • Annotation:
    Most of coalgebraic logic so far has focussed on set-coalgebras and their Boolean logics. Here we start a systematic investigation of coalgebras over posets and set ourselves the modest aim to show how to transfer to Pos the result of Schroder and Klin, namely that the logic of all predicate liftings is expressive.

Iterative Reflections of Monads

  • Authors: Adamek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Mathematical Structures in Computer Science. 2010, 20(3), 419-452. ISSN 0960-1295.
  • Year: 2010
  • DOI: 10.1017/S0960129509990326
  • Link: https://doi.org/10.1017/S0960129509990326
  • Department: Department of Mathematics
  • Annotation:
    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 M 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 M, following in the footsteps of Evelyn Nelson and Jerzy Tiuryn, and prove that M is iterative if and only if all free algebras for M are iterative algebras.

Recursive Program Schemes and Context-Free Monads

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Milius, S.
  • Publication: Electronic Notes in Theoretical Computer Science. 2010, 2010(264), 3-23. ISSN 1571-0661.
  • Year: 2010
  • Department: Department of Mathematics
  • Annotation:
    Solutions of recursive program schemes over a given signature were characterized by Bruno Courcelle as precisely the context-free (or algebraic) \Sigma-trees. These are the finite and infinite \Sigma-trees yielding, via labelling of paths, context-free languages. Our aim is to generalize this to finitary endofunctors H of general categories: we construct a monad C^H generated by solutions of recursive program schemes of type H, and prove that this monad is ideal. In case of polynomial endofunctors of Set our construction precisely yields the monad of context-free \Sigma-trees of Courcelle. Our result builds on a result by N. Ghani et al on solutions of algebraic systems.

A Description of Iterative Reflections of Monads

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Milius, S.
  • Publication: Proceedings of FoSSaCS 2009. London: Springer, 2009. pp. 152-166. LNCS 5504. ISBN 978-3-642-00595-4.
  • Year: 2009
  • DOI: 10.1007/978-3-642-00596-1
  • Link: https://doi.org/10.1007/978-3-642-00596-1
  • Department: Department of Mathematics
  • Annotation:
    For ideal monads in Set (e. g. the finite list monad, the finite bag monad etc.) we have recently proved that every set generates a free iterative algebra. This gives rise to a new monad. We prove now that this monad is iterative in the sense of Calvin Elgot, in fact, this is the iterative reflection of the given ideal monad. This shows how to freely add unique solutions of recursive equations to a given algebraic theory. Examples: the monad of free commutative binary algebras has the monad of binary rational unordered trees as iterative reflection, and the finite list monad has the iterative reflection given by adding an absorbing element.

Elgot Theories: A new Perspective of Iteration Theories (Extended Abstract)

  • Authors: Adámek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Electronic Notes in Theoretical Computer Science. 2009, 2009(249), 407-427. ISSN 1571-0661.
  • Year: 2009
  • Department: Department of Mathematics
  • Annotation:
    The concept of iteration theory of Bloom and ´Esik summarizes all equational properties that iteration has in usual applications, e.g., in Domain Theory where to every system of recursive equations the least solution is assigned. However, this assignment in Domain Theory is also functorial. Yet, functoriality is not included in the definition of iteration theory. Pity: functorial iteration theories have a particularly simple axiomatization, and most of examples of iteration theories are functorial. The reason for excluding functoriality was the view that this property cannot be called equational. This is true from the perspective of the category Sgn of signatures as the base category: whereas iteration theories are monadic (thus, equationally presentable) over Sgn, functorial iteration theories are not. In the present paper we propose to change the perspective and work, in lieu of Sgn, in the category of sets in context (the presheaf category of finite sets and functions). We p

Final coalgebras in accessible categories

  • Department: Department of Mathematics
  • Annotation:
    We give conditions on a finitary endofunctor of a finitely accessible category to admit a final coalgebra. Our conditions always apply to the case of a finitary endofunctor of a locally finitely presentable (l.f.p.) category and they bring an explicit construction of the final coalgebra in this case. On the other hand, there are interesting examples of final coalgebras beyond the realm of l.f.p. categories to which our results apply. We rely on ideas developed by Tom Leinster for the study of self-similar objects in topology.

Representability Relative to a Doctrine

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Karazeris, P.
  • Publication: Cahiers de topologie et geometrie differentielle categoriques. 2009, L(1), 3-22. ISSN 0008-0004.
  • Year: 2009
  • Department: Department of Mathematics
  • Annotation:
    We propose the notion of a doctrine to provide a uniform environment for studying weak representability concepts. Since (co)limits are representability notions, this allows us to define and study weakened (co)limit concepts. For example, in case the doctrine in question is the doctrine of free cocompletions under colimits of some class, the existence of weakened limits in the ambient category is closely related to honest limits in free cocompletions. Similarly, we can relate certain weak promonoidal structures on a category to honest monoidal structures on a free cocompletion.

Semantics of Higher-Order Recursion Schemes

  • Authors: Adamek, J., Milius, S., doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: ALGEBRA AND COALGEBRA IN COMPUTER SCIENCE, PROCEEDINGS. Udine: Centre International des Sciences Mechaniques, 2009. pp. 49-63. Lecture Notes in Computer Science. ISSN 0302-9743. ISBN 978-3-642-03740-5.
  • Year: 2009
  • DOI: 10.1007/978-3-642-03741-2_5
  • Link: https://doi.org/10.1007/978-3-642-03741-2_5
  • Department: Department of Mathematics
  • Annotation:
    Higher-order recursion schemes are equations defining recursively 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 \lambda-calculus in which the terminals are interpreted as continuous operations. For the uninterpreted semantics based on infinite \lambda-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. Whereas Fiore et al proved that the presheaf F of \lambda-terms is an initial H-monoid, we work with the presheaf R of rational infinite \lambda-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 R.

Analytic Functors and Weak Pullbacks, accepted for publication

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J.
  • Publication: Theory and Applications of Categories. 2008, 2008(21), 191-209. ISSN 1201-561X.
  • Year: 2008
  • Department: Department of Mathematics
  • Annotation:
    For accessible set-functors it is well-known that weak preservation of limits is equivalent to representability, and weak preservation of connected limits to familial representability. In contrast, preservation of weak wide pullbacks is equivalent to being a coproduct of quotients of hom-functors modulo groups of automorphisms. For finitary functors this was proved by Andre Joyal who called these functors analytic. We introduce a generalization of Joyal's concept from endofunctors of $\Set$ to endofunctors of a symmetric monoidal category.

Bases for Parametrized Iterativity

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Milius, S.
  • Publication: Information and Computation. 2008, 206(8), 966-1002. ISSN 0890-5401.
  • Year: 2008
  • DOI: 10.1016/j.ic.2008.05.002
  • Link: https://doi.org/10.1016/j.ic.2008.05.002
  • Department: Department of Mathematics
  • Annotation:
    Parametrized iterativity of an algebra means the existence of unique solutions of all finitary recursive systems of equations where recursion is allowed to use only some variables (chosen as a parameter). We show how such algebras can be introduced in an arbitrary category A by employing a base, i.e., an operation interpreting objects of A as monads on A. For every base we prove that free base algebras and free iterative base algebras exist. The main result is a coalgebraic construction of the latter: all equation morphisms form a diagram whose colimit is proved to be a free iterative base algebra.

Iterative Algebras: How Iterative are They?

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Borger, R., Milius, S.
  • Publication: Theory and Applications of Categories. 2008, 19(5), 61-92. ISSN 1201-561X.
  • Year: 2008
  • Department: Department of Mathematics
  • Annotation:
    Iterative algebras, defined by the property that every guarded system of recursive equations has a unique solution, are proved to have a much stronger property: every system of recursive equations has a unique strict solution. Those systems that have a unique solution in every iterative algebra are characterized.

Algebras with Parametrized Iterativity

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Milius, S.
  • Publication: Theoretical Computer Science. 2007, 388(1-3), 130-151. ISSN 0304-3975.
  • Year: 2007
  • DOI: 10.1016/j.tcs.2007.06.015
  • Link: https://doi.org/10.1016/j.tcs.2007.06.015
  • Department: Department of Mathematics
  • Annotation:
    Iterative algebras, as studied by Nelson and Tiuryn, are generalized to algebras whose iterativity is parametrized in the sense that only some variables can be used for iteration. For example, in the case of one binary operation, the free iterative algebra is the algebra of all rational binary trees; if only the left-hand variable is allowed to be iterated, then the free iterative algebra is the algebra of all right-well-founded rational binary trees. In order to express such parametrized iterativity, we work with parametrized endofunctors of sets, i.e. finitary endofunctors H: Set x Set-> Set, and introduce the concept of iterativity for algebras for the endofunctor H:X |-> H(X,X). We then describe free iterative H-algebras.

Dense Morphisms of Monads

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Karazeris, P.
  • Publication: Theory and Applications of Categories. 2007, 2007(18), 372-399. ISSN 1201-561X.
  • Year: 2007
  • Department: Department of Mathematics
  • Annotation:
    Given an arbitrary locally finitely presentable category K and finitary monads T and S on K, we characterize monad morphisms alpha: S --> T with the property that the induced functor alpha_*: K^T --> K^S between the categories of Eilenberg-Moore algebras is fully faithful. We call such monad morphisms dense and give a characterization of them in the spirit of Beth's definability theorem. We also give a characterization in terms of epimorphic property of alpha and clarify the connection between various notions of epimorphisms between monads.

What are Iteration Theories?

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Adámek, J., Milius, S.
  • Publication: Proceedings of MFCS 2007. Berlin: Springer, 2007. pp. 240-252. ISSN 0302-9743. ISBN 978-3-540-74455-9.
  • Year: 2007
  • Department: Department of Mathematics
  • Annotation:
    We prove that iteration theories can be introduced as algebras for the monad Rat on the category of signatures assigning to every signature Sigma the rational-Sigma-tree signature. This supports the result that iteration theories axiomatize precisely the equational properties of least fixed points in domain theory: Rat is the monad of free rational theories and every free rational theory has a continuous completion.

Elgot Algebras

  • DOI: 10.2168/LMCS-2(5:4)2006
  • Link: https://doi.org/10.2168/LMCS-2(5:4)2006
  • Department: Department of Mathematics
  • Annotation:
    We introduce so-called Elgot algebras and propose them as a convenient structure for semantics. Elgot algebrais an algebra with a specified solution for every flat system of recursive equations. This specification must satisfy two well motivated axioms.

Elgot Algebras (Extended Abstract)

  • Department: Department of Mathematics
  • Annotation:
    We axiomatize algebras that allow a solution of finitary recursive equations. We prove that these algebras arise as Eilenberg-Moore algebras of the free iterative monad.

How Iterative are Iterative Algebras?

  • Department: Department of Mathematics
  • Annotation:
    Iterative algebras are defined by the property that every guarded system of recursive equations has a unique solutions. We prove that they have a much stronger property: every system of recursive equations has a unique strict solution.

Iterative Algebras at Work

  • DOI: 10.1017/S0960129506005706
  • Link: https://doi.org/10.1017/S0960129506005706
  • Department: Department of Mathematics
  • Annotation:
    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.

A General Final Coalgebra Theorem

  • Department: Department of Mathematics
  • Annotation:
    By the Final Coalgebra Theorem of Aczel and Mendler, every endofunctor of the category of sets has a final coalgebra that may be a proper class. We generalize this to ``well-behaved'' categories.

Completeness of Cocompletions

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Karazeris, P., Rosický, J.
  • Publication: Journal of Pure and Applied Algebra. 2005, 2005(196), 229-250. ISSN 0022-4049.
  • Year: 2005
  • Department: Department of Mathematics
  • Annotation:
    Several weakenings of the notion of a limit are studied. The weakened completeness notions are then used to analyzing the existence of limits in free cocompletions under colimits

Iterative Algebras for a Base

  • Department: Department of Mathematics
  • Annotation:
    We introduce iterativity w.r.t. to a base (a functor of two variables yielding finitary monads in one variable). We provide a coalgebraic construction of free iterative algebras

From Iterative Algebras to Iterative Theories

  • Department: Department of Mathematics
  • Annotation:
    The coalgebraic proof of the existence of a free iterative theory is given. The proof uses a concept of iterative algebras and is much simpler and more general than the original proof given by Calvin Elgot and his collaborators.

On Coalgebra Based on Classes

  • Department: Department of Mathematics
  • Annotation:
    The category Class of classes is proved to have a number of properties suitable for algebra and coalgebra: for example, every endofunctor is set-based, has an initial algebra and final coalgebra. A description of a final coalgebra of the power-set functor is given

Free Iterative Theories

Infinite Trees and Completely Iterative Theories

On Rational Monads and Free Iterative Theories

Some Remarks on Finitary and Iterative Monads

A Remark on Conservative Cocompletions of Categories

Final Coalgebras and a Solution Theorem for Arbitrary Endofunctors

Simultaneously Reflective and Coreflective Subcategories of Presheaves

A Coalgebraic View of Infinite Trees and Iteration

Categorical Methods of the Theory of Structures and Computer Science

On Functors Which Are Lax Epimorphisms

Recursive Equations in Infinite Trees

  • Authors: doc. RNDr. Jiří Velebil, Ph.D.,
  • Publication: Applications of Modern Mathematical Methods. Ljubljana: Univerza v Ljubljani, 2001. pp. 179-190. ISBN 961-6209-27-2.
  • Year: 2001

A Duality between Infinitary Varieties and Algebraic Theories

Categorical Generalization of a Universal Domain

Categorical Methods of the Theory of Structures and Computer Science

On Categories Generalizing Universal Domains

  • Authors: doc. RNDr. Jiří Velebil, Ph.D., Trnková, V.
  • Publication: Mathematical Structures in Computer Science. 1999,(9), 159-175. ISSN 0960-1295.
  • Year: 1999

Responsible person Ing. Mgr. Radovan Suk