Publications

BibTeX

@inproceedings{10.1109/LICS56636.2023.10175751,
  author={Jakl, Tom{\'a}{\v{s}} and Marsden, Dan and Shah, Nihil},
  booktitle={2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)}, 
  title={A categorical account of composition methods in logic},
  year={2023},
  volume={},
  number={},
  pages={1-14},
  doi={10.1109/LICS56636.2023.10175751}
}

Abstract

We present a categorical theory of the composition methods in finite model theory – a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman–Vaught–Mostowski (FVM) type theorems, which characterize how logical equivalence be- haves under composition and transformation of models.
Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the positive existential fragment, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads.
We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments.

BibTeX

@Inbook{GehrkeJaklReggio2023,
  title="A {C}ook's Tour of Duality in Logic: From Quantifiers, Through Vietoris, to Measures",
  author="Gehrke, Mai and Jakl, Tom{\'a}{\v{s}} and Reggio, Luca",
  editor="Palmigiano, Alessandra and Sadrzadeh, Mehrnoosh",
  bookTitle="Samson Abramsky on Logic and Structure in Computer Science and Beyond",
  publisher="Springer International Publishing",
  year="2023",
  pages="129--158",
  isbn="978-3-031-24117-8",
  doi="10.1007/978-3-031-24117-8_4"
}

Abstract

We identify and highlight certain landmark results in Samson Abramsky’s work which we believe are fundamental to current developments and future trends. In particular, we focus on the use of (i) topological duality methods to solve problems in logic and computer science; (ii) category theory and, more particularly, free (and co-free) constructions; (iii) these tools to unify the power' andstructure’ strands in computer science.

BibTeX

@InProceedings{abramskyjaklpaine2022,
  author="Abramsky, Samson and Jakl, Tom{\'a}{\v{s}} and Paine, Thomas",
  title="Discrete Density Comonads and Graph Parameters",
  series="Lecture Notes in Computer Science",
  editor="Hansen, Helle Hvid and Zanasi, Fabio",
  booktitle="Coalgebraic Methods in Computer Science. CMCS 2022",
  year="2022",
  volume="13225",
  pages="23--44",
  publisher="Springer International Publishing",
  isbn="978-3-031-10736-8"
}

Abstract

Game comonads have brought forth a new approach to studying finite model theory categorically. By representing model comparison games semantically as comonads, they allow important logical and combinatorial properties to be exressed in terms of their Eilenberg-Moore coalgebras. As a result, a number of results from finite model theory, such as preservation theorems and homomorphism counting theorems, have been formalised and parameterised by comonads, giving rise to new results simply by varying the comonad. In this paper we study the limits of the comonadic approach in the combinatorial and homomorphism-counting aspect of the theory, regardless of whether any model comparison games are involved. We show that any standard graph parameter has a corresponding comonad, classifying the same class. This comonad is constructed via a simple Kan extension formula, making it the initial solution to this problem and, furthermore, automatically admitting a homomorphism-counting theorem.

BibTeX

@article{gehrkejaklreggio2022,
  TITLE = {{A duality theoretic view on limits of finite structures: Extended version}},
  AUTHOR = {Mai Gehrke and Tom{'a}{\v{s}} Jakl and Luca Reggio},
  URL = {https://lmcs.episciences.org/8978},
  DOI = {10.46298/lmcs-18(1:16)2022},
  JOURNAL = {{Logical Methods in Computer Science}},
  VOLUME = {{Volume 18, Issue 1}},
  YEAR = {2022},
  MONTH = Jan,
  KEYWORDS = {Computer Science - Logic in Computer Science ; Mathematics - Logic},
}

Abstract

A systematic theory of structural limits for finite models has been developed by Nesetril and Ossona de Mendez. It is based on the insight that the collection of finite structures can be embedded, via a map they call the Stone pairing, in a space of measures, where the desired limits can be computed. We show that a closely related but finer grained space of (finitely additive) measures arises – via Stone-Priestley duality and the notion of types from model theory – by enriching the expressive power of first-order logic with certain “probabilistic operators”. We provide a sound and complete calculus for this extended logic and expose the functorial nature of this construction.

The consequences are two-fold. On the one hand, we identify the logical gist of the theory of structural limits. On the other hand, our construction shows that the duality theoretic variant of the Stone pairing captures the adding of a layer of quantifiers, thus making a strong link to recent work on semiring quantifiers in logic on words. In the process, we identify the model theoretic notion of types as the unifying concept behind this link. These results contribute to bridging the strands of logic in computer science which focus on semantics and on more algorithmic and complexity related areas, respectively.

BibTeX

@inproceedings{10.1109/LICS52264.2021.9470609,
    author = {Dawar, Anuj and Jakl, Tom\'{a}\v{s} and Reggio, Luca},
    title = {Lov\'{a}sz-Type Theorems and Game Comonads},
    year = {2021},
    isbn = {9781665448956},
    publisher = {Association for Computing Machinery},
    address = {New York, NY, USA},
    doi = {10.1109/LICS52264.2021.9470609},
    booktitle = {Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science},
    articleno = {53},
    pages={1-13},
    numpages = {13}
}

Abstract

Lovász (1967) showed that two finite relational structures A and B are isomorphic if, and only if, the number of homomorphisms from C to A is the same as the number of homomorphisms from C to B for any finite structure C. Soon after, Pultr (1973) proved a categorical generalisation of this fact. We propose a new categorical formulation, which applies to any locally finite category with pushouts and a proper factorisation system. As special cases of this general theorem, we obtain two variants of Lovász’ theorem: the result by Dvořák (2010) that characterises equivalence of graphs in the k-dimensional Weisfeiler-Leman equivalence by homomorphism counts from graphs of tree-width at most k, and the result of Grohe (2020) characterising equivalence with respect to first-order logic with counting and quantifier depth k in terms of homomorphism counts from graphs of tree-depth at most k. The connection of our categorical formulation with these results is obtained by means of the game comonads of Abramsky et al. We also present a novel application to homomorphism counts in modal logic.

BibTeX

@inproceedings{FussnerJaklGhannoumSimpson2020classification,
  title={Classification of finite semigroups and categories using computational methods},
  author={Fussner, Wesley and Ghannoum, Najwa and Jakl, Tom{\'a}{\v{s}} and Simpson, Carlos},
  booktitle={Proceedings of the 5th Conference on Artificial Intelligence and Theorem Proving AITP},
  year={2020}
}

BibTeX

@InProceedings{10.1007/978-3-030-45231-5_16,
  author = "Gehrke, Mai and Jakl, Tom{\'a}{\v{s}} and Reggio, Luca",
  editor = "Goubault-Larrecq, Jean and K{\"o}nig, Barbara",
  title = "A Duality Theoretic View on Limits of Finite Structures",
  booktitle = "Foundations of Software Science and Computation Structures",
  year = "2020",
  publisher = "Springer International Publishing",
  address = "Cham",
  pages = "299--318",
  isbn = "978-3-030-45231-5"
}

Abstract

A systematic theory of structural limits for finite models has been developed by Nešetřil and Ossona de Mendez. It is based on the insight that the collection of finite structures can be embedded, via a map they call the Stone pairing, in a space of measures, where the desired limits can be computed. We show that a closely related but finer grained space of measures arises — via Stone-Priestley duality and the notion of types from model theory — by enriching the expressive power of first-order logic with certain ``probabilistic operators’’. We provide a sound and complete calculus for this extended logic and expose the functorial nature of this construction.

BibTeX

@article{jakl2020,
  author = "Tom{\'a}{\v{s}} Jakl",
  title = "Canonical extensions of locally compact frames",
  journal = "Topology and its Applications",
  volume = "273",
  pages = "106976",
  year = "2020",
  issn = "0166-8641",
  doi = "https://doi.org/10.1016/j.topol.2019.106976"
}

Abstract

Canonical extension of finitary ordered structures such as lattices, posets, proximity lattices, etc., is a certain completion which entirely describes the topological dual of the ordered structure and it does so in a purely algebraic and choice-free way. We adapt the general algebraic technique that constructs them to the theory of frames. As a result, we show that every locally compact frame embeds into a completely distributive lattice by a construction which generalises, among others, the canonical extensions for distributive lattices and proximity lattices. This construction also provides a new description of a construction by Marcel Erné. Moreover, canonical extensions of frames enable us to frame-theoretically represent monotone maps with respect to the specialisation order.

BibTeX

@article{jakljungpultr2019,
  author="Jakl, Tom{\'a}{\v{s}} and Jung, Achim and Pultr, Ale{\v{s}}",
  title="Quotients of d-Frames",
  journal="Applied Categorical Structures",
  year="2019",
  month="Jun",
  day="01",
  volume="27",
  number="3",
  pages="261--275",
  issn="1572-9095",
  doi="10.1007/s10485-018-09553-7"
}

Abstract

It is shown that every d-frame admits a complete lattice of quotients. Quotienting may be triggered by a binary relation on one of the two constituent frames, or by changes to the consistency or totality structure, but as these are linked by the reasonableness conditions of d-frames, the result in general will be that both frames are factored and both consistency and totality are increased.

BibTeX

@InProceedings{jakljung2017,
  author =    {Tom{\'a}{\v{s}} Jakl and Achim Jung},
  title =     {{Free Constructions and Coproducts of d-Frames}},
  booktitle = {7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =     {14:1--14:15},
  series =    {Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =      {978-3-95977-033-0},
  ISSN =      {1868-8969},
  year =      {2017},
  volume =    {72},
  editor =    {Filippo Bonchi and Barbara K{\"o}nig},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =   {Dagstuhl, Germany},
  doi =       {10.4230/LIPIcs.CALCO.2017.14},
  annote =    {Keywords: Free construction, d-frame, coproduct, C-ideals}
}

Abstract

A general theory of presentations for d-frames does not yet exist. We review the difficulties and give sufficient conditions for when they can be overcome. As an application we prove that the category of d-frames is closed under coproducts.

BibTeX

@article{jakljungpultr2016,
  title = "Bitopology and Four-valued Logic",
  author = "Tom{\'a}{\v{s}} Jakl and Achim Jung and Ale{\v{s}} Pultr",
  journal = "Electronic Notes in Theoretical Computer Science",
  volume = "325",
  pages = "201 - 219",
  year = "2016",
  note = "The Thirty-second Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII)",
  issn = "1571-0661",
  doi = "https://doi.org/10.1016/j.entcs.2016.09.039",
  keywords = "Bilattices, d-frames, nd-frames, bitopological spaces, four-valued logic"
}

Abstract

Bilattices and d-frames are two different kinds of structures with a four-valued interpretation. Whereas d-frames were introduced with their topological semantics in mind, the theory of bilattices has a closer connection with logic. We consider a common generalisation of both structures and show that this not only still has a clear bitopological semantics, but that it also preserves most of the original bilattice logic. Moreover, we also obtain a new bitopological interpretation for the connectives of four-valued logic.

BibTeX

@article{bbjpw2016,
  author =  {Richard N. Ball and Bernhard Banaschewski and
             Tom{\'a}{\v{s}} Jakl and Ale{\v{s}} Pultr and
             Joanne Walters-Wayland},
  title =   {Tightness relative to some (co)reflections in topology},
  journal = {Quaestiones Mathematicae},
  volume =  {39},
  number =  {3},
  pages =   {421-436},
  year  =   {2016},
  publisher = {Taylor & Francis},
  doi =       {10.2989/16073606.2015.1073191}
}

Abstract

We address what might be termed the reverse reflection problem: given a monoreflection from a category A onto a subcategory B, when is a given object b ∈ B the reflection of a proper subobject? We start with a well known specific instance of this problem, namely the fact that a compact metric space is never the Čech-Stone compactification of a proper subspace. We show that this holds also in the pointfree setting, i.e., that a compact metrizable locale is never the Čech-Stone compactification of a proper sublocale. This is a stronger result than the classical one, but not because of an increase in scope; after all, assuming weak choice principles, every compact regular locale is the topology of a compact Hausdorff space. The increased strength derives from the conclusion, for in general a space has many more sublocales than subspaces. We then extend the analysis from metric locales to the broader class of perfectly normal locales, i.e., those whose frame of open sets consists entirely of cozero elements. We include a second proof of these results which is purely algebraic in character.

At the opposite extreme from these results, we show that an extremally disconnected locale is a compactification of each of its dense sublocales. Finally, we analyze the same phenomena, also in the pointfree setting, for the 0-dimensional compact reflection and for the Lindelöf reflection.