Document Open Access Logo

Relating Structure and Power: Comonadic Semantics for Computational Resources

Authors Samson Abramsky , Nihil Shah

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.2.pdf
  • Filesize: 0.51 MB
  • 17 pages

Document Identifiers

Author Details

Samson Abramsky
  • Oxford University Department of Computer Science, Wolfson Building, Parks Road, Oxford OX1 3QD, U.K.
Nihil Shah
  • Oxford University Department of Computer Science, Wolfson Building, Parks Road, Oxford OX1 3QD, U.K.

Funding

  • Abramsky, Samson: Samson Abramsky’s work was supported by EPSRC grant EP/N018745/1.

Cite As Get BibTex

Samson Abramsky and Nihil Shah. Relating Structure and Power: Comonadic Semantics for Computational Resources. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 2:1-2:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CSL.2018.2

Abstract

Combinatorial games are widely used in finite model theory, constraint satisfaction, modal logic and concurrency theory to characterize logical equivalences between structures. In particular, Ehrenfeucht-Fraïssé games, pebble games, and bisimulation games play a central role. We show how each of these types of games can be described in terms of an indexed family of comonads on the category of relational structures and homomorphisms. The index k is a resource parameter which bounds the degree of access to the underlying structure. The coKleisli categories for these comonads can be used to give syntax-free characterizations of a wide range of important logical equivalences. Moreover, the coalgebras for these indexed comonads can be used to characterize key combinatorial parameters: tree-depth for the Ehrenfeucht-Fraïssé comonad, tree-width for the pebbling comonad, and synchronization-tree depth for the modal unfolding comonad. These results pave the way for systematic connections between two major branches of the field of logic in computer science which hitherto have been almost disjoint: categorical semantics, and finite and algorithmic model theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Finite Model Theory
  • Theory of computation → Categorical semantics
Keywords
  • Finite model theory
  • combinatorial games
  • Ehrenfeucht-Fraïssé games
  • pebble games
  • bisimulation
  • comonads
  • coKleisli category
  • coalgebras of a comonad

Metrics

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

References

  1. Samson Abramsky, Rui Soares Barbosa, Nadish de Silva, and Octavio Zapata. The quantum monad on relational structures. To appear in proceedings of MFCS 2017, 2018. Google Scholar
  2. Samson Abramsky, Anuj Dawar, and Pengming Wang. The pebbling comonad in finite model theory. In Logic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pages 1-12. IEEE, 2017. Google Scholar
  3. Luca Aceto, Anna Ingolfsdottir, and Joshua Sack. Resource bisimilarity and graded bisimilarity coincide. Information Processing Letters, 111(2):68-76, 2010. Google Scholar
  4. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217-274, 1998. Google Scholar
  5. Patrick Blackburn, Maarten De Rijke, and Yde Venema. Modal Logic, volume 53. Cambridge University Press, 2002. Google Scholar
  6. E. Casanovas, P. Dellunde, and R. Jansana. On Elementary Equivalence for Equality-free Logic. Notre Dame Journal of Formal Logic, 37(3):506-522, 1996. URL: http://dx.doi.org/10.1305/ndjfl/1039886524.
  7. Ashok K Chandra and Philip M Merlin. Optimal implementation of conjunctive queries in relational data bases. In Proceedings of the Ninth Annual ACM Symposium on Theory of Computing, pages 77-90. ACM, 1977. Google Scholar
  8. Flavio Corradini, Rocco De Nicola, and Anna Labella. Graded modalities and resource bisimulation. In International Conference on Foundations of Software Technology and Theoretical Computer Science, pages 381-393. Springer, 1999. Google Scholar
  9. Bruno Courcelle. The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and computation, 85(1):12-75, 1990. Google Scholar
  10. M. de Rijke. A Note on Graded Modal Logic. Studia Logica, 64(2):271-283, 2000. Google Scholar
  11. Heinz-Dieter Ebbinghaus and Jörg Flum. Finite model theory. Springer Science &Business Media, 2005. Google Scholar
  12. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, and Tarmo Uustalu. Combining effects and coeffects via grading. ACM SIGPLAN Notices, 51(9):476-489, 2016. Google Scholar
  13. Erich Grädel. Decision procedures for guarded logics. In International Conference on Automated Deduction, pages 31-51. Springer, 1999. Google Scholar
  14. Erich Grädel and Martin Otto. The freedoms of (guarded) bisimulation. In Johan van Benthem on Logic and Information Dynamics, pages 3-31. Springer, 2014. Google Scholar
  15. Pavol Hell and Jaroslav Něsetřil. Graphs and homomorphisms. Oxford University Press, 2004. Google Scholar
  16. L. Hella. Logical hierarchies in PTIME. Information and Computation, 121:1-19, 1996. Google Scholar
  17. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In International Colloquium on Automata, Languages, and Programming, pages 299-309. Springer, 1980. Google Scholar
  18. Ton Kloks. Treewidth: computations and approximations, volume 842. Springer Science &Business Media, 1994. Google Scholar
  19. Phokion G Kolaitis and Moshe Y Vardi. On the expressive power of Datalog: tools and a case study. In Proceedings of the ninth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systems, pages 61-71. ACM, 1990. Google Scholar
  20. Phokion G Kolaitis and Moshe Y Vardi. Infinitary logics and 0-1 laws. Information and Computation, 98(2):258-294, 1992. Google Scholar
  21. Leonid Libkin. Elements of Finite Model Theory (Texts in Theoretical Computer Science. An EATCS Series). Springer, 2004. Google Scholar
  22. Saunders Mac Lane. Categories for the working mathematician, volume 5. Springer Science &Business Media, 2013. Google Scholar
  23. Ernest G Manes. Algebraic Theories, volume 26. Springer Science &Business Media, 2012. Google Scholar
  24. Robin Milner. A calculus of communicating systems. Number 92 in Lecture Notes in Comput. Science. Springer-Verlag, 1980. Google Scholar
  25. Robin Milner. Communication and concurrency, volume 84. Prentice Hall New York etc., 1989. Google Scholar
  26. Eugenio Moggi. Notions of computation and monads. Information and computation, 93(1):55-92, 1991. Google Scholar
  27. Jaroslav Nešetřil and Patrice Ossona De Mendez. Tree-depth, subgraph coloring and homomorphism bounds. European Journal of Combinatorics, 27(6):1022-1041, 2006. Google Scholar
  28. Dominic Orchard. Programming contextual computations. Technical Report UCAM-CL-TR-854, University of Cambridge, 2014. Google Scholar
  29. Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Transactions on Programming Languages and Systems (TOPLAS), 31(4):15, 2009. Google Scholar
  30. Saharon Shelah. Every two elementarily equivalent models have isomorphic ultrapowers. Israel Journal of Mathematics, 10(2):224-233, 1971. Google Scholar
  31. Tarmo Uustalu and Varmo Vene. Comonadic notions of computation. Electronic Notes in Theoretical Computer Science, 203(5):263-284, 2008. Google Scholar
  32. Jouko Väänänen. Dependence logic: A new approach to independence friendly logic, volume 70. Cambridge University Press, 2007. 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 About DROPS Imprint Privacy Contact