Comonadic semantics for guarded fragments

Abramsky, Samson; Marsden, Dan

Abstract

In previous work ([1], [2], [3]), it has been shown how a range of model comparison games which play a central role in finite model theory, including Ehrenfeucht-Fraïssé, pebbling, and bisimulation games, can be captured in terms of resource-indexed comonads on the category of relational structures. Moreover, the coalgebras for these comonads capture important combinatorial parameters such as tree-width and tree-depth.The present paper extends this analysis to quantifier-guarded fragments of first-order logic. We give a systematic account, covering atomic, loose and clique guards. In each case, we show that coKleisli morphisms capture winning strategies for Duplicator in the existential guarded bisimulation game, while back-and-forth bisimulation, and hence equivalence in the full guarded fragment, is captured by spans of open morphisms. We study the coalgebras for these comonads, and show that they correspond to guarded tree decompositions. We relate these constructions to a syntax-free setting, with a comonad on the category of hypergraphs.

Citation

Abramsky, S., & Marsden, D. (2021, June). Comonadic semantics for guarded fragments. Presented at 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Rome, Italy

• Presentation Conference Type: Edited Proceedings
• Conference Name: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Start Date: Jun 29, 2021
• End Date: Jul 2, 2021
• Acceptance Date: Jun 29, 2021
• Online Publication Date: Jul 7, 2021
• Publication Date: Jul 7, 2021
• Deposit Date: Oct 9, 2024
• Peer Reviewed: Peer Reviewed
• Pages: 231-243
• Series Title: CFP21039-POD
• Book Title: 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)
• ISBN: 9781665448963
• DOI: https://doi.org/10.1109/lics52264.2021.9470594
• Public URL: https://nottingham-repository.worktribe.com/output/40556979