Document Open Access Logo

How to Write a Coequation ((Co)algebraic pearls)

Authors Fredrik Dahlqvist , Todd Schmid

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.13.pdf
  • Filesize: 1 MB
  • 25 pages

Document Identifiers

Author Details

Fredrik Dahlqvist
  • Department of Computer Science, University College London, UK
Todd Schmid
  • Department of Computer Science, University College London, UK

Funding

  • Dahlqvist, Fredrik: Leverhulme Project Grant `Verification of machine learning algorithms'

Acknowledgements

The authors are most grateful to Alexander Kurz for his services as history consultant. The responsibility for any mistake or mischaracterisation lie solely with the authors.

Cite AsGet BibTex

Fredrik Dahlqvist and Todd Schmid. How to Write a Coequation ((Co)algebraic pearls). In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 13:1-13:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.13

Abstract

There is a large amount of literature on the topic of covarieties, coequations and coequational specifications, dating back to the early seventies. Nevertheless, coequations have not (yet) emerged as an everyday practical specification formalism for computer scientists. In this review paper, we argue that this is partly due to the multitude of syntaxes for writing down coequations, which seems to have led to some confusion about what coequations are and what they are for. By surveying the literature, we identify four types of syntaxes: coequations-as-corelations, coequations-as-predicates, coequations-as-equations, and coequations-as-modal-formulas. We present each of these in a tutorial fashion, relate them to each other, and discuss their respective uses.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Program specifications
Keywords
  • Coalgebra
  • coequation
  • covariety

Metrics

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

References

  1. Peter Aczel. Non-Well-Founded Sets. Number 14 in Lecture Notes. Center for the Study of Language and Information (CSLI), 1988. Google Scholar
  2. Peter Aczel and Nax Mendler. A final coalgebra theorem. In Category theory and computer science, pages 357-365. Springer, 1989. Google Scholar
  3. Jiří Adámek. Birkhoff’s covariety theorem without limitations. Commentationes Mathematicae Universitatis Carolinae, 46(2):197-215, 2005. Google Scholar
  4. Jiří Adámek. A logic of coequations. In International Workshop on Computer Science Logic, pages 70-86. Springer, 2005. Google Scholar
  5. Jiří Adámek, Horst Herrlich, and George E Strecker. Abstract and concrete categories. The joy of cats, 2004. Google Scholar
  6. Jiří Adámek and Hans-E Porst. From varieties of algebras to covarieties of coalgebras. Electronic Notes in Theoretical Computer Science, 44(1):27-46, 2001. Google Scholar
  7. Jiří Adámek and Hans-E Porst. On varieties and covarieties in a category. Mathematical Structures in Computer Science, 13(2):201, 2003. Google Scholar
  8. Jirí Adámek and Hans-E. Porst. On tree coalgebras and coalgebra presentations. Theor. Comput. Sci., 311(1-3):257-283, 2004. Google Scholar
  9. Jiří Adámek and Vera Trnková. Automata and algebras in categories, volume 37. Springer Science & Business Media, 1990. Google Scholar
  10. Jiří Adámek, Stefan Milius, Robert S.R. Myers, and Henning Urbat. Generalized Eilenberg theorem: Varieties of languages in a category. ACM Trans. Comput. Logic, 20(1), 2018. Google Scholar
  11. Steve Awodey and Jesse Hughes. The coalegebraic dual of Birkoff’s variety theorem. Technical report, Carnegie Mellon University, 2000. Google Scholar
  12. Adriana Balan, Alexander Kurz, and Jiří Velebil. Positive fragments of coalgebraic logics. In International Conference on Algebra and Coalgebra in Computer Science, pages 51-65. Springer, 2013. Google Scholar
  13. Adolfo Ballester-Bolinches, Enric Cosme-Llópez, and Jan J. M. M. Rutten. The dual equivalence of equations and coequations for automata. Inf. Comput., 244:49-75, 2015. Google Scholar
  14. Bernhard Banaschewski and Horst Herrlich. Subcategories defined by implications. McMaster Univ., 1975. Google Scholar
  15. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  16. Michael Barr. Terminal coalgebras in well-founded set theory. Theoretical Computer Science, 114(2):299-315, 1993. Google Scholar
  17. Garrett Birkhoff. On the structure of abstract algebras. Proceedings of the Cambridge, 1935. Google Scholar
  18. Patrick Blackburn, Johan FAK van Benthem, and Frank Wolter. Handbook of modal logic. Elsevier, 2006. Google Scholar
  19. Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM, 11(4):481-494, 1964. Google Scholar
  20. Corina Cîrstea. A coequational approach to specifying behaviours. Electronic Notes in Theoretical Computer Science, 19:142-163, 1999. Google Scholar
  21. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. The Computer Journal, 54(1):31-41, 2011. Google Scholar
  22. Edmund M. Clarke, E Allen Emerson, and A Prasad Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244-263, 1986. Google Scholar
  23. Ranald Clouston and Robert Goldblatt. Covarieties of coalgebras: comonads and coequations. In International Colloquium on Theoretical Aspects of Computing, pages 288-302. Springer, 2005. Google Scholar
  24. John Horton Conway. Regular algebra and finite machines. Courier Corporation, 2012. Google Scholar
  25. Fredrik Dahlqvist. Completeness-via-canonicity for coalgebraic logics. PhD thesis, Imperial College London, 2015 . Google Scholar
  26. Fredrik Dahlqvist. Coalgebraic completeness-via-canonicity. In International Workshop on Coalgebraic Methods in Computer Science, pages 174-194. Springer, 2016. Google Scholar
  27. Fredrik Dahlqvist and Alexander Kurz. The positivication of coalgebraic logics. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO), 2017. Google Scholar
  28. Fredrik Dahlqvist and David Pym. Completeness via canonicity for distributive substructural logics: a coalgebraic perspective. In International Conference on Relational and Algebraic Methods in Computer Science, pages 119-135. Springer, 2015. Google Scholar
  29. Robert Davis. Universal coalgebra and categories of transition systems. Mathematical systems theory, 4(1):91-95, 1970. Google Scholar
  30. Robert Davis. Multivalued operations and universal coalgebra. Proceedings of the American Mathematical Society, 32(2):385-388, 1972. Google Scholar
  31. Robert Davis. Quasi cotripleable categories,. Proceedings of the American Mathematical Society, 35:43-48, 1972. Google Scholar
  32. Robert Davis. Combinatorial examples in universal coalgebra. Proceedings of the American Mathematical Society, 89(1):32-34, 1983. Google Scholar
  33. Robert Davis. Combinatorial examples in universal coalgebra. iii. Proceedings of the American Mathematical Society, 92(3):332-334, 1984. Google Scholar
  34. E Allen Emerson and Joseph Y Halpern. Decision procedures and expressiveness in the temporal logic of branching time. Journal of computer and system sciences, 30(1):1-24, 1985. Google Scholar
  35. W. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. An EATCS Series. Springer Berlin Heidelberg, 2013. Google Scholar
  36. Nate Foster, Dexter Kozen, Matthew Milano, Alexandra Silva, and Laure Thompson. A coalgebraic decision procedure for NetKAT. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pages 343-355. ACM, 2015. Google Scholar
  37. Rob Gerth, Doron Peled, Moshe Y Vardi, and Pierre Wolper. Simple on-the-fly automatic verification of linear temporal logic. In International Conference on Protocol Specification, Testing and Verification, pages 3-18. Springer, 1995. Google Scholar
  38. Robert Goldblatt. Logics of time and computation. Center for the Study of Language and Information, 1987. Google Scholar
  39. Robert Goldblatt. A comonadic account of behavioural covarieties of coalgebras. Mathematical Structures in Computer Science, 15(2):243-269, 2005. Google Scholar
  40. Clemens Grabmayer and Wan Fokkink. A complete proof system for 1-free regular expressions modulo bisimilarity. Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, July 2020. Google Scholar
  41. H Peter Gumm. Elements of the general theory of coalgebras, 1999. Google Scholar
  42. H Peter Gumm. Functors for coalgebras. Algebra universalis, 45(2):135-147, 2001. Google Scholar
  43. H Peter Gumm and Tobias Schröder. Products of coalgebras. Algebra Universalis, 46(1):163-185, 2001. Google Scholar
  44. Heinz-Peter Gumm. Equational and implicational classes of coalgebras. Theoretical Computer Science, 260(1-2):57-69, 2001. Google Scholar
  45. Heinz-Peter Gumm and Tobias Schröder. Covarieties and complete covarieties. Electronic Notes in Theoretical Computer Science, 11:42-55, 1998. Google Scholar
  46. Helle Hvid Hansen, Clemens Kupke, and Jan Rutten. Stream differential equations: specification formats and solution methods. arXiv preprint arXiv:1609.08367, 2016. Google Scholar
  47. Ulrich Hensel and Horst Reichel. Defining equations in terminal coalgebras. In Recent Trends in Data Type Specification, pages 307-318. Springer, 1994. Google Scholar
  48. Jesse Hughes. Modal operators for coequations. Electronic Notes in Theoretical Computer Science, 44(1):205-226, 2001. Google Scholar
  49. Jesse Hughes. A study of categories of algebras and coalgebras. PhD thesis, Carnegie Mellon University, 2001. Google Scholar
  50. Bart Jacobs. Mongruences and cofree coalgebras. In International Conference on Algebraic Methodology and Software Technology, pages 245-260. Springer, 1995. Google Scholar
  51. Bart Jacobs. The temporal logic of coalgebras via Galois algebras. Mathematical Structures in Computer Science, 12(6):875-903, 2002. Google Scholar
  52. Bart Jacobs. Introduction to Coalgebra, volume 59. Cambridge University Press, 2017. Google Scholar
  53. Bart Jacobs and Ana Sokolova. Exemplaric expressivity of modal logics. Journal of logic and computation, 20(5):1041-1068, 2010. Google Scholar
  54. Peter Jipsen. Concurrent Kleene algebra with tests. In Peter Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors, Relational and Algebraic Methods in Computer Science - 14th International Conference, RAMiCS 2014. Proceedings, volume 8428 of Lecture Notes in Computer Science, pages 37-48. Springer, 2014. Google Scholar
  55. Christian Jäkel. A unified categorical approach to graphs, 2015. URL: http://arxiv.org/abs/1507.06328.
  56. Tobias Kappé, Paul Brunet, Alexandra Silva, and Fabio Zanasi. Concurrent Kleene algebra: Free model and completeness. CoRR, abs/1710.02787, 2017. Google Scholar
  57. Yasuo Kawahara and Masao Mori. A small final coalgebra theorem. Theor. Comput. Sci., 233(1-2):129-145, 2000. Google Scholar
  58. Dexter Kozen. A completeness theorem for Kleene algebras and the algebra of regular events. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), pages 214-225. IEEE Computer Society, 1991. Google Scholar
  59. Dexter Kozen and Frederick Smith. Kleene algebra with tests: Completeness and decidability. In Computer Science Logic, 10th International Workshop, CSL '96, Annual Conference of the EACSL, 1996, volume 1258 of LNCS, pages 244-259. Springer, 1996. Google Scholar
  60. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Algebraic semantics for coalgebraic logics. Electronic Notes in Theoretical Computer Science, 106:219-241, 2004. Google Scholar
  61. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Ultrafilter extensions for coalgebras. In International Conference on Algebra and Coalgebra in Computer Science, pages 263-277. Springer, 2005. Google Scholar
  62. Clemens Kupke and Raul Andres Leal. Characterising behavioural equivalence: Three sides of one coin. In Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009. Proceedings, volume 5728 of LNCS, pages 97-112. Springer, 2009. Google Scholar
  63. Alexander Kurz. A co-variety-theorem for modal logic. Advances in Modal Logic, 2:367-380, 1998. Google Scholar
  64. Alexander Kurz. Specifying coalgebras with modal logic. Electronic Notes in Theoretical Computer Science, 11:56-70, 1998. Google Scholar
  65. Alexander Kurz. Logics for coalgebras and applications to computer science. PhD thesis, Ludwig-Maximilians-Universität München, 2000. Google Scholar
  66. Alexander Kurz. Modal rules are co-implications. Electronic Notes in Theoretical Computer Science, 44(1):241-253, 2001. Google Scholar
  67. Alexander Kurz. Specifying coalgebras with modal logic. Theoretical Computer Science, 260(1-2):119-138, 2001. Google Scholar
  68. Alexander Kurz and Jirí Rosicky. Operations and equations for coalgebras. Mathematical Structures in Computer Science, 15(1):149, 2005. Google Scholar
  69. Alexander Kurz and Jiří Rosicky. The Goldblatt-Thomason theorem for coalgebras. In International Conference on Algebra and Coalgebra in Computer Science, pages 342-355. Springer, 2007. Google Scholar
  70. Giulio Manzonetto and Antonino Salibra. From lambda-calculus to universal algebra and back. In Mathematical Foundations of Computer Science 2008, 33rd International Symposium, MFCS 2008. Proceedings, volume 5162 of LNCS, pages 479-490. Springer, 2008. Google Scholar
  71. Michal Marvan. On covarieties of coalgebras. Archivum Mathematicum, 21(1):51-63, 1985. Google Scholar
  72. Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. Google Scholar
  73. Lawrence S Moss. Coalgebraic logic. Annals of Pure and Applied Logic, 96(1-3):277-317, 1999. Google Scholar
  74. Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1-3):177-193, 2003. Google Scholar
  75. Boris I. Plotkin and Tanya Plotkin. Universal Algebra and Computer Science. In Fundamentals of Computation Theory, 13th International Symposium, FCT 2001. Proceedings, volume 2138 of LNCS, pages 35-44. Springer, 2001. Google Scholar
  76. Horst Reichel. An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science, 5(2):129-152, 1995. Google Scholar
  77. Grigore Roşu. A Birkhoff-like axiomatizability result for hidden algebra and coalgebra. Electronic Notes in Theoretical Computer Science, 11:176-193, 1998. Google Scholar
  78. Grigore Roşu. Equational axiomatizability for coalgebra. Theoretical Computer Science, 260(1-2):229-247, 2001. Google Scholar
  79. Jan JMM Rutten. Universal coalgebra: a theory of systems. Technical report, CWI, 1996. Google Scholar
  80. Jan JMM Rutten. Universal coalgebra: a theory of systems. Theoretical computer science, 249(1):3-80, 2000. Google Scholar
  81. Julian Salamanca. Unveiling Eilenberg-type correspondences: Birkhoff’s theorem for (finite) algebras + duality. CoRR, abs/1702.02822, 2017. Google Scholar
  82. Julian Salamanca, Adolfo Ballester-Bolinches, Marcello M. Bonsangue, Enric Cosme-Llópez, and Jan J. M. M. Rutten. Regular varieties of automata and coequations. In Mathematics of Program Construction - 12th International Conference, MPC 2015, volume 9129 of LNCS, pages 224-237. Springer, 2015. Google Scholar
  83. Julian Salamanca, Marcello Bonsangue, and Jurriaan Rot. Duality of equations and coequations via contravariant adjunctions. In Ichiro Hasuo, editor, Coalgebraic Methods in Computer Science, pages 73-93, Cham, 2016. Springer International Publishing. Google Scholar
  84. Antonino Salibra. On the algebraic models of lambda calculus. Theor. Comput. Sci., 249(1):197-240, 2000. Google Scholar
  85. Antonino Salibra and Robert Goldblatt. A finite equational axiomatization of the functional algebras for the lambda calculus. Inf. Comput., 148(1):71-130, 1999. Google Scholar
  86. Arto Salomaa. Two complete axiom systems for the algebra of regular events. J. ACM, 13(1):158-169, 1966. Google Scholar
  87. Hanamantagouda P Sankappanavar and Stanley Burris. A course in universal algebra, volume 78. Citeseer, 1981. Google Scholar
  88. Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene algebra with tests: Coequations, coinduction, and completeness. CoRR, abs/2102.08286, 2021. Google Scholar
  89. Daniel Schwencke. Coequational logic for finitary functors. Electronic Notes in Theoretical Computer Science, 203(5):243-262, 2008. Google Scholar
  90. Daniel Schwencke. Coequational logic for accessible functors. Information and Computation, 208(12):1469-1489, 2010. Google Scholar
  91. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time. CoRR, abs/1907.05920, 2019. Google Scholar
  92. Moshe Y Vardi and Pierre Wolper. An automata-theoretic approach to automatic program verification. In Proceedings of the First Symposium on Logic in Computer Science, pages 322-331. IEEE Computer Society, 1986. Google Scholar
  93. Yde Venema. Algebras and coalgebras. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 331-426. North-Holland, 2007. Google Scholar
  94. Wolfgang Wechler. Universal Algebra for Computer Scientists, volume 25 of EATCS Monographs on Theoretical Computer Science. Springer, 1992. Google Scholar
  95. Uwe Wolter. On corelations, cokernels, and coequations. Electronic Notes in Theoretical Computer Science, 33:317-336, 2000. Google Scholar
  96. James Worrell. Terminal sequences for accessible endofunctors. In Bart Jacobs and Jan J. M. M. Rutten, editors, Coalgebraic Methods in Computer Science, CMCS 1999, volume 19 of Electronic Notes in Theoretical Computer Science, pages 24-38. Elsevier, 1999. Google Scholar
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 Imprint Privacy Contact