Document Open Access Logo

Closure Hyperdoctrines

Authors Davide Castelnovo, Marino Miculan

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2021.12.pdf
  • Filesize: 0.85 MB
  • 21 pages

Document Identifiers

Author Details

Davide Castelnovo
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Marino Miculan
  • Department of Mathematics, Computer Science and Physics, University of Udine, Italy

Funding

  • Miculan, Marino: Supported by the Italian MIUR project PRIN 2017FTXR7S IT MATTERS (Methods and Tools for Trustworthy Smart Systems).

Cite AsGet BibTex

Davide Castelnovo and Marino Miculan. Closure Hyperdoctrines. In 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 211, pp. 12:1-12:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CALCO.2021.12

Abstract

(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we present an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Hence, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, and for the definition of new spatial logics for new applications.

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • categorical logic
  • topological semantics
  • closure operators
  • spatial logic

Metrics

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

Related Versions

References

  1. Marco Aiello, Ian Pratt-Hartmann, and Johan van Benthem, editors. Handbook of Spatial Logics. Springer, 2007. Google Scholar
  2. Michael Atiyah. Introduction to commutative algebra. CRC Press, 2018. Google Scholar
  3. Tom Avery. Codensity and the Giry monad. Journal of Pure and Applied Algebra, 220(3):1229-1251, 2016. Google Scholar
  4. Giorgio Bacci and Marino Miculan. Structural operational semantics for continuous state stochastic transition systems. Journal of Computer and System Sciences, 81(5):834-858, 2015. Google Scholar
  5. Gina Belmonte, Vincenzo Ciancia, Diego Latella, and Mieke Massink. Innovating medical image analysis via spatial logics. In From Software Engineering to Formal Methods and Tools, and Back, volume 11865 of Lecture Notes in Computer Science, pages 85-109. Springer, 2019. Google Scholar
  6. Bodil Biering. Dialectica interpretations: a categorical analysis. PhD thesis, IT University of Copenhagen, 2008. Google Scholar
  7. Francis Borceux. Handbook of categorical algebra: volume 1, Basic category theory, volume 1. Cambridge University Press, 1994. Google Scholar
  8. Luca Cardelli and Andrew D. Gordon. Anytime, anywhere: Modal logics for mobile ambients. In Proc. POPL, pages 365-377. ACM, 2000. Google Scholar
  9. Davide Castelnovo and Marino Miculan. Closure hyperdoctrines, with paths. arXiv preprint arXiv:2007.04213, 2020. Google Scholar
  10. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Specifying and verifying properties of space. In IFIP International Conference on Theoretical Computer Science, pages 222-235. Springer, 2014. Google Scholar
  11. Vincenzo Ciancia, Diego Latella, Michele Loreti, and Mieke Massink. Spatial logic and spatial model checking for closure spaces. In International School on Formal Methods for the Design of Computer, Communication and Software Systems, pages 156-201. Springer, 2016. Google Scholar
  12. Djordje Čubrić. On the semantics of the universal quantifier. Annals of Pure and Applied Logic, 87(3):209-239, 1997. Google Scholar
  13. Pietro Di Gianantonio and Marino Miculan. Unifying recursive and co-recursive definitions in sheaf categories. In Proc. FoSSaCS, volume 2987 of Lecture Notes in Computer Science, pages 136-150. Springer, 2004. Google Scholar
  14. Dikran Dikranjan and Walter Tholen. Categorical structure of closure operators: with applications to topology, algebra and discrete mathematics, volume 346. Springer, 2013. Google Scholar
  15. Georgi Dimov and Dimiter Vakarelov. Contact algebras and region-based theory of space: a proximity approach i. Fundamenta Informaticae, 74(2, 3):209-249, 2006. Google Scholar
  16. Georgi Dimov and Dimiter Vakarelov. Contact algebras and region-based theory of space: proximity approach ii. Fundamenta Informaticae, 74(2, 3):251-282, 2006. Google Scholar
  17. E Allen Emerson and Joseph Y Halpern. “sometimes” and “not never” revisited: on branching versus linear time temporal logic. Journal of the ACM (JACM), 33(1):151-178, 1986. Google Scholar
  18. Antony Galton. A generalized topological view of motion in discrete space. Theoretical Computer Science, 305(1-3):111-134, 2003. Google Scholar
  19. Michèle Giry. A categorical approach to probability theory. In Categorical aspects of topology and analysis, pages 68-85. Springer, 1982. Google Scholar
  20. John Walker Gray. Formal category theory: adjointness for 2-categories, volume 391. Springer, 2006. Google Scholar
  21. H. Peter Gumm and Tobias Schröder. Products of coalgebras. Algebra Universalis, 46:163-185, 2001. Google Scholar
  22. Jesse Hughes and Bart Jacobs. Factorization systems and fibrations: Toward a fibred birkhoff variety theorem. Electronic Notes in Theoretical Computer Science, 69:156-182, 2003. Google Scholar
  23. Bart Jacobs. Categorical logic and type theory, volume 141. Elsevier, 1999. Google Scholar
  24. Bart Jacobs. Introduction to Coalgebra, volume 59. Cambridge University Press, 2017. Google Scholar
  25. Bart Jacobs and Ana Sokolova. Exemplaric expressivity of modal logics. Journal of logic and computation, 20(5):1041-1068, 2010. Google Scholar
  26. Peter T. Johnstone. Sketches of an elephant: A topos theory compendium, volume 2. Oxford University Press, 2002. Google Scholar
  27. Gregory Maxwell Kelly. A note on relations relative to a factorization system. In Category Theory, pages 249-261. Springer, 1991. Google Scholar
  28. Anders Kock and Gonzalo E. Reyes. Doctrines in categorical logic. In Studies in Logic and the Foundations of Mathematics, volume 90, pages 283-313. Elsevier, 1977. Google Scholar
  29. Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: an overview. Theoretical Computer Science, 412(38):5070-5094, 2011. Google Scholar
  30. F. William Lawvere. Adjointness in foundations. Dialectica, 23(3-4):281-296, 1969. Google Scholar
  31. F. William Lawvere. Equality in hyperdoctrines and comprehension schema as an adjoint functor. Applications of Categorical Algebra, 17:1-14, 1970. Google Scholar
  32. Saunders MacLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Science & Business Media, 2012. Google Scholar
  33. Maria Emilia Maietti, Fabio Pasquali, and Giuseppe Rosolini. Triposes, exact completions, and Hilbert’s ε-operator. Tbilisi Mathematical Journal, 10(3):141-166, 2017. Google Scholar
  34. Maria Emilia Maietti and Giuseppe Rosolini. Quotient completion for the foundation of constructive mathematics. Logica Universalis, 7(3):371-402, 2013. Google Scholar
  35. Michael Makkai and Gonzalo E. Reyes. First order categorical logic: model-theoretical methods in the theory of topoi and related categories, volume 611. Springer, 2006. Google Scholar
  36. Marino Miculan and Giorgio Bacci. Modal logics for brane calculus. In Proc. CMSB, volume 4210 of Lecture Notes in Computer Science, pages 1-16. Springer, 2006. Google Scholar
  37. Fabio Pasquali. A co-free construction for elementary doctrines. Applied Categorical Structures, 23(1):29-41, 2015. Google Scholar
  38. Andrew M. Pitts. Categorical logic. Technical report, University of Cambridge, 1995. Google Scholar
  39. Andrew M Pitts. Tripos theory in retrospect. Mathematical structures in computer science, 12(3):265-279, 2002. Google Scholar
  40. Robert A. G. Seely. Hyperdoctrines, natural deduction and the Beck condition. Mathematical Logic Quarterly, 29(10):505-542, 1983. Google Scholar
  41. Oswald Wyler. Lecture notes on topoi and quasitopoi. World Scientific, 1991. Google Scholar
  42. Lotfi A. Zadeh. Fuzzy sets. In Fuzzy sets, fuzzy logic, and fuzzy systems: selected papers by Lotfi A Zadeh, pages 394-432. World Scientific, 1996. 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