DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.21

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Authors: Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, we identify a general fibrational condition for the IA-FC coincidence, namely in the fiber over an initial algebra in the base category. Identifying (co)algebras in a fiber as (co)inductive predicates, our fibrational IA-FC coincidence allows one to use coinductive witnesses (such as invariants) for verifying inductive properties (such as liveness). Our general fibrational theory features the technical condition of stability of chain colimits; we extend the framework to the presence of a monadic effect, too, restricting to fibrations of complete lattice-valued predicates. Practical benefits of our categorical theory are exemplified by new "upside-down" witness notions for three verification problems: probabilistic liveness, and acceptance and model-checking with respect to bottom-up tree automata.

Cite as

Mayuko Kori, Ichiro Hasuo, and Shin-ya Katsumata. Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kori_et_al:LIPIcs.CONCUR.2021.21,
  author =	{Kori, Mayuko and Hasuo, Ichiro and Katsumata, Shin-ya},
  title =	{{Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{21:1--21:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.21},
  URN =		{urn:nbn:de:0030-drops-143982},
  doi =		{10.4230/LIPIcs.CONCUR.2021.21},
  annote =	{Keywords: initial algebra, final coalgebra, fibration, category theory}
}

Document

DOI: 10.4230/LIPIcs.CALCO.2015.156

Codensity Liftings of Monads

Authors: Shin-ya Katsumata and Tetsuya Sato

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract

We introduce a method to lift monads on the base category of a fibration to its total category using codensity monads. This method, called codensity lifting, is applicable to various fibrations which were not supported by the categorical >>-lifting. After introducing the codensity lifting, we illustrate some examples of codensity liftings of monads along the fibrations from the category of preorders, topological spaces and extended psuedometric spaces to the category of sets, and also the fibration from the category of binary relations between measurable spaces. We next study the liftings of algebraic operations to the codensity-lifted monads. We also give a characterisation of the class of liftings (along posetal fibrations with fibred small limits) as a limit of a certain large diagram.

Cite as

Shin-ya Katsumata and Tetsuya Sato. Codensity Liftings of Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 156-170, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{katsumata_et_al:LIPIcs.CALCO.2015.156,
  author =	{Katsumata, Shin-ya and Sato, Tetsuya},
  title =	{{Codensity Liftings of Monads}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{156--170},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.156},
  URN =		{urn:nbn:de:0030-drops-55329},
  doi =		{10.4230/LIPIcs.CALCO.2015.156},
  annote =	{Keywords: Monads, Lifting, Fibration, Giry Monad}
}

Search Results

Documents authored by Katsumata, Shin-ya

Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down

Abstract

Cite as

Codensity Liftings of Monads

Abstract

Cite as

Thanks for your feedback!

Could not send message