Document Open Access Logo

Identity-Preserving Lax Extensions and Where to Find Them

Authors Sergey Goncharov , Dirk Hofmann , Pedro Nora , Lutz Schröder , Paul Wild

PDF
Thumbnail PDF

File

LIPIcs.STACS.2025.40.pdf
  • Filesize: 0.8 MB
  • 20 pages

Document Identifiers

Author Details

Sergey Goncharov
  • University of Birmingham, UK
Dirk Hofmann
  • CIDMA, University of Aveiro, Portugal
Pedro Nora
  • Radboud Universiteit, Nijmegen, The Netherlands
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Paul Wild
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

  • Goncharov, Sergey: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 501369690.
  • Hofmann, Dirk: This work is supported by CIDMA under the FCT (Portuguese Foundation for Science and Technology) Multi-Annual Financing Program for R&D Units.
  • Schröder, Lutz: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 531706730.
  • Wild, Paul: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - project number 434050016.

Cite As Get BibTex

Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. Identity-Preserving Lax Extensions and Where to Find Them. In 42nd International Symposium on Theoretical Aspects of Computer Science (STACS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 327, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.STACS.2025.40

Abstract

Generic notions of bisimulation for various types of systems (nondeterministic, probabilistic, weighted etc.) rely on identity-preserving (normal) lax extensions of the functor encapsulating the system type, in the paradigm of universal coalgebra. It is known that preservation of weak pullbacks is a sufficient condition for a functor to admit a normal lax extension (the Barr extension, which in fact is then even strict); in the converse direction, nothing is currently known about necessary (weak) pullback preservation conditions for the existence of normal lax extensions. In the present work, we narrow this gap by showing on the one hand that functors admitting a normal lax extension preserve 1/4-iso pullbacks, i.e. pullbacks in which at least one of the projections is an isomorphism. On the other hand, we give sufficient conditions, showing that a functor admits a normal lax extension if it weakly preserves either 1/4-iso pullbacks and 4/4-epi pullbacks (i.e. pullbacks in which all morphisms are epic) or inverse images. We apply these criteria to concrete examples, in particular to functors modelling neighbourhood systems and weighted systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Concurrency
Keywords
  • (Bi-)simulations
  • lax extensions
  • modal logics
  • coalgebra

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, Manchester, UK, September 5-8, 1989, Proceedings, volume 389 of Lecture Notes in Computer Science, pages 357-365. Springer, 1989. URL: https://doi.org/10.1007/BFB0018361.
  2. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories: The joy of cats. John Wiley & Sons Inc., 1990. Republished in: Reprints in Theory and Applications of Categories, No. 17 (2006) pp. 1-507. URL: http://tac.mta.ca/tac/reprints/articles/17/tr17abs.html.
  3. Roland Carl Backhouse, Peter J. de Bruin, Paul F. Hoogendijk, Grant Malcolm, Ed Voermans, and Jaap van der Woude. Polynomial relators (extended abstract). In Maurice Nivat, Charles Rattray, Teodor Rus, and Giuseppe Scollo, editors, Algebraic Methodology and Software Technology, AMAST 1991, Workshops in Computing, pages 303-326. Springer, 1991. Google Scholar
  4. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Coalgebraic behavioral metrics. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:20)2018.
  5. Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, number 137 in Lect. Notes Math., pages 39-55. Springer, 1970. URL: https://doi.org/10.1007/BFb0060439.
  6. Michael Barr. Relational algebras. In Reports of the Midwest Category Seminar IV, pages 39-55. Springer, 1970. URL: https://doi.org/10.1007/bfb0060439.
  7. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  8. Richard S. Bird and Oege de Moor. Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, 1997. Google Scholar
  9. Filippo Bonchi, Marcello M. Bonsangue, Michele Boreale, Jan J. M. M. Rutten, and Alexandra Silva. A coalgebraic perspective on linear weighted automata. Inf. Comput., 211:77-105, 2012. URL: https://doi.org/10.1016/J.IC.2011.12.002.
  10. Brian F. Chellas. Modal Logic - An Introduction. Cambridge University Press, 1980. URL: https://doi.org/10.1017/CBO9780511621192.
  11. Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic mu-calculus. Log. Methods Comput. Sci., 7(3), 2011. URL: https://doi.org/10.2168/LMCS-7(3:3)2011.
  12. Maria Manuel Clementino, Dirk Hofmann, and George Janelidze. The monads of classical algebra are seldom weakly cartesian. J. Homotopy and Related Structures, 9(1):175-197, 2014. Google Scholar
  13. Francesco Gavazzo. Quantitative behavioural reasoning for higher-order effectful programs: Applicative distances. In Anuj Dawar and Erich Grädel, editors, Logic in Computer Science, LICS 2018, pages 452-461. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209149.
  14. Sergey Goncharov, Dirk Hofmann, Pedro Nora, Lutz Schröder, and Paul Wild. A point-free perspective on lax extensions and predicate liftings. Mathematical Structures in Computer Science, pages 1-30, 2023. URL: https://doi.org/10.1017/S096012952300035X.
  15. Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40206-7_19.
  16. H. Peter Gumm. Free-algebra functors from a coalgebraic perspective. In Daniela Petrisan and Jurriaan Rot, editors, Coalgebraic Methods in Computer Science, CMCS 2020, volume 12094 of LNCS, pages 55-67. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-57201-3_4.
  17. H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, Berlin, Germany, March 25-26, 2000, volume 33 of Electronic Notes in Theoretical Computer Science, pages 111-131. Elsevier, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80346-9.
  18. H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Andrea Corradini, Marina Lenisa, and Ugo Montanari, editors, Coalgebraic Methods in Computer Science, CMCS 2001, volume 44(1) of ENTCS, pages 185-204. Elsevier, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80908-3.
  19. H. Peter Gumm and Tobias Schröder. Types and coalgebraic structure. Algebra universalis, 53(2–3):229-252, August 2005. URL: https://doi.org/10.1007/s00012-005-1888-2.
  20. H. Peter Gumm and Mehdi Zarrad. Coalgebraic simulations and congruences. In Marcello M. Bonsangue, editor, Coalgebraic Methods in Computer Science - 12th IFIP WG 1.3 International Workshop, CMCS 2014, Colocated with ETAPS 2014, Grenoble, France, April 5-6, 2014, Revised Selected Papers, volume 8446 of Lecture Notes in Computer Science, pages 118-134. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44124-4_7.
  21. Helle Hvid Hansen and Clemens Kupke. A coalgebraic perspective on monotone modal logic. In Jirí Adámek and Stefan Milius, editors, Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 121-143. Elsevier, 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.028.
  22. Wim H. Hesselink and Albert Thijs. Fixpoint semantics and simulation. Theor. Comput. Sci., 238(1-2):275-311, 2000. URL: https://doi.org/10.1016/S0304-3975(98)00176-5.
  23. Dirk Hofmann, Gavin J. Seal, and Walter Tholen, editors. Monoidal Topology. A Categorical Approach to Order, Metric, and Topology, volume 153 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge, July 2014. Authors: Maria Manuel Clementino, Eva Colebunders, Dirk Hofmann, Robert Lowen, Rory Lucyshyn-Wright, Gavin J. Seal and Walter Tholen. URL: https://doi.org/10.1017/cbo9781107517288.
  24. Jesse Hughes and Bart Jacobs. Simulations in coalgebra. Theor. Comput. Sci., 327(1-2):71-108, 2004. URL: https://doi.org/10.1016/J.TCS.2004.07.022.
  25. Thomas Ihringer. Algemeine Algebra. Mit einem Anhang über Universelle Coalgebra von H. P. Gumm, volume 10 of Berliner Studienreihe zur Mathematik. Heldermann Verlag, 2003. Google Scholar
  26. Bartek Klin. Structural operational semantics for weighted transition systems. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday, volume 5700 of LNCS, pages 121-139. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04164-8_7.
  27. Clemens Kupke, Alexander Kurz, and Yde Venema. Completeness for the coalgebraic cover modality. Log. Methods Comput. Sci., 8(3), 2012. URL: https://doi.org/10.2168/LMCS-8(3:2)2012.
  28. Alexander Kurz and Raul Andres Leal. Modalities in the stone age: A comparison of coalgebraic logics. Theor. Comput. Sci., 430:88-116, 2012. URL: https://doi.org/10.1016/J.TCS.2012.03.027.
  29. Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 27-41. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_3.
  30. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, CMCS 2021, volume 7399 of LNCS, pages 150-169. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32784-1_9.
  31. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. Journal of Computer and System Sciences, 81(5):880-900, 2015. URL: https://doi.org/10.1016/j.jcss.2014.12.006.
  32. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  33. Rohit Parikh. Propositional game logic. In Foundations of Computer Science, FOCS 1983, pages 195-200. IEEE Computer Society, 1983. URL: https://doi.org/10.1109/SFCS.1983.47.
  34. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45(1):19-33, 2004. URL: https://doi.org/10.1305/ndjfl/1094155277.
  35. David Peleg. Concurrent dynamic logic (extended abstract). In Robert Sedgewick, editor, Symposium on Theory of Computing, STOC 1985, pages 232-239. ACM, 1985. URL: https://doi.org/10.1145/22145.22172.
  36. Jacques Riguet. Relations binaires, fermetures, correspondances de Galois. Bulletin de la Société Mathématique de France, 76:114-155, 1948. URL: https://doi.org/10.24033/bsmf.1401.
  37. Jan J. M. M. Rutten. Relators and metric bisimulations. In Bart Jacobs, Larry Moss, Horst Reichel, and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1998, volume 11 of ENTCS, pages 252-258. Elsevier, 1998. URL: https://doi.org/10.1016/S1571-0661(04)00063-5.
  38. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  39. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2-3):230-247, January 2008. URL: https://doi.org/10.1016/j.tcs.2007.09.023.
  40. Christoph Schubert and Gavin J. Seal. Extensions in the theory of lax algebras. Theory and Applications of Categories, 21(7):118-151, 2008. Google Scholar
  41. Gavin J. Seal. Canonical and op-canonical lax algebras. Theory and Applications of Categories, 14(10):221-243, 2005. URL: http://www.tac.mta.ca/tac/volumes/14/10/14-10abs.html.
  42. Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform interpolation in coalgebraic modal logic. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science, CALCO 2017, volume 72 of LIPIcs, pages 21:1-21:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPICS.CALCO.2017.21.
  43. Albert Thijs. Simulation and fixpoint semantics. PhD thesis, University of Groningen, 1996. Google Scholar
  44. Věra Trnková. General theory of relational automata. Fund. Inform., 3(2):189-233, 1980. URL: https://doi.org/10.3233/FI-1980-3208.
  45. Paul Wild and Lutz Schröder. Characteristic logics for behavioural metrics via fuzzy lax extensions. In Igor Konnov and Laura Kovács, editors, Concurrency Theory, CONCUR 2020, volume 171 of LIPIcs, pages 27:1-27:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPICS.CONCUR.2020.27.
  46. Paul Wild and Lutz Schröder. Characteristic logics for behavioural hemimetrics via fuzzy lax extensions. Log. Methods Comput. Sci., 18(2), 2022. URL: https://doi.org/10.46298/LMCS-18(2:19)2022.
  47. James Worrell. Coinduction for recursive data types: partial orders, metric spaces and Ω-categories. In Horst Reichel, editor, Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 337-356. Elsevier, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80356-1.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact