[ad_1]
:::info
This paper is available on arxiv under CC BY-SA 4.0 DEED license.
Authors:
(1) Tomáš Jakl, Czech Academy of Sciences and Czech Technical University;
(2) Dan Marsden, School of Computer Science University of Nottingham;
(3) Nihil Shah, Department of Computer Science University of Oxford.
:::
Table of Links
- Abstract & Introduction
- Prelimenaries
- FVM Theorems for Positive Existential Fragments
- FVM Theorems for Counting Logic
- FVM Theorems for The Full Logic
- Abstract FVM Theorems for Products
- Adding Equality and Other Enrichment
- Conclusions, Acknowledgments & References
- Appendix A FVM theorems for coproducts
- Appendix B Proofs Omitted from Section III
- Appendix C Proofs Omitted from Section IV
- Appendix D Proofs Omitted from Section V
- Appendix E Proofs Omitted from Section VI
- Appendix F Proofs Omitted from Section VII
VIII. CONCLUSION
We presented a categorical approach to the composition method, and specifically Feferman–Vaught–Mostowski theorems. We exploit game comonads to encapsulate the logics and their model comparison games. Surprising connections to classical constructions in category theory, and especially the monad theory of bilinear maps emerged from this approach, cf. Section V-A.
\
For finite model theorists, our work provides a novel highlevel account of many FVM theorems, abstracting away from individual logics and constructions. Furthermore, concrete instances of these theorems are verified purely semantically, by finding a suitable collection homomorphisms forming a Kleisli law satisfying (S2’), instead of the usual delicate verification that strategies of model comparison games compose. For game comonads, we provide a much needed tool that enables us to handle logical relationships between structures as they are transformed or viewed in terms of different logics.
\
The FVM results in this paper, combined with judicious use of the techniques described in Section VII can be pushed significantly further. FVM theorems and the compositional method are of particular significance in the setting of monadic second-order (MSO) logic [49]. Exploiting the results we have presented for the composition method, a follow up paper will give a comonadic semantics for MSO, and develop a semantic account of Courcelle’s algorithmic meta-theorems [5].
\
The original theorem of Feferman–Vaught [3] is very flexible, including incorporating structure on the indices of families of models to be combined by an operation, as well as the models themselves. This aspect is currently outside the scope of our comonadic methods. An ad-hoc adaptation of our approach also gives a proof of the FVM theorem for free amalgamations, but this does not follow directly from our theorems. Developing these extensions is left to future work.
\
The present work bears some resemblance to Turi and Plotkin’s bialgebraic semantics [50], a categorical model of structural operational semantics (SOS) [51]. Turi and Plotkin noticed that the SOS rules assigning behaviour to syntax could be abstracted as a certain distributive law λ. An algebra encodes the composition operations of the syntax, and a coalgebra the behaviour. If this pair is suitably compatible with λ, forming a so-called λ-bialgebra, then crucially bisimulation is a congruence with respect to the composition operations. Both bialgebraic semantics and our work presented in this paper give a categorical account of well-behaved composition operations, with the interaction between composition and observable behaviour mediated by some form of distributive law. There are also essential differences: bialgebraic semantics typically focuses on assigning behaviour to syntax, whereas FVM theorems encompass operations on models. Our FVM theorems are parametric in a choice of logic or observable behaviour, while the notion of bisimulation in bialgebraic semantics is fixed by the coalgebra signature functor. The natural presence of positive existential and counting quantifier variants of FVM theorems, and the incorporation of resource parameters, do not seem to have a direct analogue in bialgebraic semantics. The similarities are intriguing, and exploring the relationship between bialgebraic semantics and our approach to FVM theorems is left to future work.
\
Acknowledgements: We would like to thank Clemens Berger for suggesting the connection with parametric adjoints and Nathanael Arkor for his suggestions on terminology. We are also grateful to the members of the EPSRC project “Resources and co-resources” for their feedback.
\
REFERENCES
[1] L. Libkin, Elements of finite model theory. Springer, 2004, vol. 41.
\
[2] A. Mostowski, “On direct products of theories,” The Journal of Symbolic Logic, vol. 17, no. 1, pp. 1–31, 1952.
\
[3] S. Feferman and R. L. Vaught, “The first-order properties of algebraic systems,” Fundamenta Mathematicae, vol. 47, 1959.
\
[4] J. A. Makowsky, “Algorithmic uses of the Feferman–Vaught theorem,” Annals of Pure and Applied Logic, vol. 126, no. 1-3, pp. 159–213, 2004.
\
[5] B. Courcelle and J. Engelfriet, Graph structure and monadic secondorder logic: a language-theoretic approach. Cambridge University Press, 2012, vol. 138.
\
[6] A. Ehrenfeucht, “An application of games to the completeness problem for formalized theories,” Fundamenta mathematicae, vol. 49, no. 129- 141, p. 13, 1960.
\
[7] R. Fraïssé, “Sur quelques classifications des relations, basées sur des isomorphismes restreints,” Publications Scientifiques de l’Université d’Alger. Série A (mathématiques), vol. 2, pp. 273–295, 1955.
\
[8] P. G. Kolaitis and M. Y. Vardi, “Infinitary logics and 0–1 laws,” Information and computation, vol. 98, no. 2, pp. 258–294, 1992.
\
[9] M. Hennessy and R. Milner, “On observing nondeterminism and concurrency,” in International Colloquium on Automata, Languages, and Programming. Springer, 1980, pp. 299–309.
\
[10] S. Abramsky, A. Dawar, and P. Wang, “The pebbling comonad in finite model theory,” in 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. IEEE Computer Society, 2017, pp. 1–12.
\
[11] S. Abramsky and N. Shah, “Relating structure and power: Comonadic semantics for computational resources,” Journal of Logic and Computation, vol. 31, no. 6, pp. 1390–1428, 2021.
\
[12] E. Moggi, “Computational lambda-calculus and monads,” in Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 1989, pp. 14–23.
\
[13] ——, “Notions of computation and monads,” Information and Computation, vol. 93, no. 1, pp. 55–92, 1991.
\
[14] E. G. Manes, Algebraic theories. Springer Science, 1976, vol. 26.
\
[15] S. Abramsky and D. Marsden, “Comonadic semantics for guarded fragments,” in 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 – July 2, 2021. IEEE, 2021, pp. 1–13.
\
[16] A. Ó. Conghaile and A. Dawar, “Game comonads & generalised quantifiers,” in 29th EACSL Annual Conference on Computer Science Logic, CSL 2021, January 25-28, 2021, Ljubljana, Slovenia (Virtual Conference), ser. LIPIcs, C. Baier and J. Goubault-Larrecq, Eds., vol. 183. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, pp. 16:1–16:17.
\
[17] Y. Montacute and N. Shah, “The pebble-relation comonad in finite model theory,” in LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 – 5, 2022, C. Baier and D. Fisman, Eds. ACM, 2022, pp. 13:1–13:11. [Online]. Available: https://doi.org/10.1145/3531130.3533335
\
[18] T. Paine, “A pebbling comonad for finite rank and variable logic, and an application to the equirank-variable homomorphism preservation theorem,” in Proceedings of the 36th Conference on the Mathematical Foundations of Programming Semantics, MFPS 2020, Online, October 1, 2020, ser. Electronic Notes in Theoretical Computer Science, P. Johann, Ed., vol. 352. Elsevier, 2020, pp. 191–209.
\
[19] A. Dawar, T. Jakl, and L. Reggio, “Lovász-type theorems and game comonads,” in 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 – July 2, 2021. IEEE, 2021, pp. 1–13.
\
[20] S. Abramsky and D. Marsden, “Comonadic semantics for hybrid logic,” in 47th International Symposium on Mathematical Foundations of Computer Science, MFCS 2022, August 22-26, 2022, Vienna, Austria, ser. LIPIcs, S. Szeider, R. Ganian, and A. Silva, Eds., vol. 241. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2022, pp. 7:1–7:14.
\
[21] L. Reggio, “Polyadic sets and homomorphism counting,” Advances in Mathematics, vol. 410, p. 108712, 2022.
\
[22] S. Abramsky, “Structure and power: an emerging landscape,” Fundam. Informaticae, vol. 186, no. 1-4, pp. 1–26, 2022.
\
[23] S. Abramsky and L. Reggio, “Arboreal categories and resources,” in 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), ser. LIPIcs, N. Bansal, E. Merelli, and J. Worrell, Eds., vol. 198. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2021, pp. 115:1–115:20.
\
[24] H. Ebbinghaus and J. Flum, Finite model theory, ser. Perspectives in Mathematical Logic. Springer, 1995.
\
[25] E. G. Manes and P. Mulry, “Monad compositions I: general constructions and recursive distributive laws,” Theory and Applications of Categories, vol. 18, no. 7, pp. 172–208, 2007.
\
[26] A. Kock, “Bilinearity and cartesian closed monads,” Mathematica Scandinavica, vol. 29, no. 2, pp. 161–174, 1971.
\
[27] T. Jakl, D. Marsden, and N. Shah, “Generalizations of bilinear maps,” 2022, technical report, arXiv preprint. [Online]. Available: https://arxiv.org/abs/2205.05382
\
[28] A. Dawar, S. Severini, and O. Zapata, “Pebble games and cospectral graphs,” Electronic Notes in Discrete Mathematics, vol. 61, pp. 323– 329, 2017.
\
[29] S. Abramsky and N. Tzevelekos, “Introduction to categories and categorical logic,” in New structures for physics. Springer, 2010, pp. 3–94.
\
[30] S. Awodey, Category theory. Oxford University Press, 2010.
\
[31] C. Stirling, Modal and temporal properties of processes. Springer Science & Business Media, 2001.
\
[32] A. W. Roscoe, Understanding concurrent systems. Springer Science & Business Media, 2010.
\
[33] H. Kleisli, “Every standard construction is induced by a pair of adjoint functors,” Proceedings of the American Mathematical Society, vol. 16, no. 3, pp. 544–546, 1965.
\
[34] B. Jacobs, “Semantics of weakening and contraction,” Annals of Pure and Applied Logic, vol. 69, no. 1, pp. 73–106, 1994.
\
[35] S. Abramsky, T. Jakl, and T. Paine, “Discrete density comonads and graph parameters,” in Coalgebraic Methods in Computer Science – 16th IFIP WG 1.3 International Workshop, CMCS 2022, Colocated with ETAPS 2022, Munich, Germany, April 2-3, 2022, Proceedings, ser. Lecture Notes in Computer Science, H. H. Hansen and F. Zanasi, Eds., vol. 13225. Springer, 2022, pp. 23–44. [Online]. Available: https://doi.org/10.1007/978-3-031-10736-8_2
\
[36] P. T. Johnstone, “Adjoint lifting theorems for categories of algebras,” Bulletin of the London Mathematical Society, vol. 7, no. 3, pp. 294– 297, 1975.
\
[37] A. Kock, “Closed categories generated by commutative monads,” Journal of the Australian Mathematical Society, vol. 12, no. 4, pp. 405–424, 1971.
\
[38] G. Seal, “Tensors, monads and actions,” Theory and Applications of Categories, vol. 28, no. 15, pp. 403–434, 2013.
\
[39] F. E. Linton, “Coequalizers in categories of algebras,” in Seminar on triples and categorical homology theory. Springer, 1969, pp. 75–90.
\
[40] R. Street, “The petit topos of globular sets,” Journal of Pure and Applied Algebra, vol. 154, no. 1-3, pp. 299–315, 2000.
\
[41] M. Weber, “Generic morphisms, parametric representations and weakly cartesian monads,” Theory and Applications of Categories, vol. 13, no. 14, pp. 191–234, 2004.
\
[42] ——, “Familial 2-functors and parametric right adjoints,” Theory and Applications of Categories, vol. 18, no. 22, pp. 665–732, 2007.
\
[43] C. Berger, P.-A. Mellies, and M. Weber, “Monads with arities and their associated theories,” Journal of Pure and Applied Algebra, vol. 216, no. 8-9, pp. 2029–2048, 2012.
\
[44] T. Altenkirch, J. Chapman, and T. Uustalu, “Monads need not be endofunctors,” in International Conference on Foundations of Software Science and Computational Structures. Springer, 2010, pp. 297–311.
\
[45] P. J. Freyd and G. M. Kelly, “Categories of continuous functors, I,” Journal of Pure and Applied Algebra, vol. 2, no. 3, pp. 169–191, 1972.
\
[46] B. Bednarczyk and M. Urbanczyk, “Comonadic semantics for description logics games,” in Proceedings of the 35th International Workshop on Description Logics (DL 2022) co-located with Federated Logic Conference (FLoC 2022), Haifa, Israel, August 7th to 10th, 2022, ser. CEUR Workshop Proceedings, O. Arieli, M. Homola, J. C. Jung, and M. Mugnier, Eds., vol. 3263. CEUR-WS.org, 2022. [Online]. Available: http://ceur-ws.org/Vol-3263/paper-5.pdf
\
[47] M. Bojanczyk, “Separator logic and star-free expressions ´ for graphs,” 2021, arXiv preprint. [Online]. Available: https://arxiv.org/abs/2107.13953
\
[48] N. Schirrmacher, S. Siebertz, and A. Vigny, “First-Order Logic with Connectivity Operators,” in 30th EACSL Annual Conference on Computer Science Logic (CSL 2022), ser. Leibniz International Proceedings in Informatics (LIPIcs), F. Manea and A. Simpson, Eds., vol. 216. Dagstuhl, Germany: Schloss Dagstuhl – LeibnizZentrum für Informatik, 2022, pp. 34:1–34:17. [Online]. Available: https://drops.dagstuhl.de/opus/volltexte/2022/15754
\
[49] Y. Gurevich, “Monadic second-order theories,” in Model-theoretic logics, J. Barwise and S. Feferman, Eds. Cambridge University Press, 1985, pp. 479–506.
\
[50] D. Turi and G. Plotkin, “Towards a mathematical operational semantics,” in Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science. IEEE, 1997, pp. 280–291.
\
[51] G.D.Plotkin, “A structural approach to operational semantics,” Aarhus University, Tech. Rep. DAIMI FN-19, 1981.
\
[52] J. Adámek, J. Adamek, J. Rosicky et al., Locally presentable and accessible categories. Cambridge University Press, 1994, vol. 189.
[ad_2]
Source link