Showing 1–12 of 12 results for author: Jakl, T

A categorical account of composition methods in logic (extended version)

Authors: Tomáš Jakl, Dan Marsden, Nihil Shah

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 behaves under composition and transformation of mod… ▽ More 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 behaves 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 existential and positive existential fragments, 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. This is an extended version of the LiCS 2023 conference paper of the same name. △ Less

Submitted 30 April, 2024; originally announced May 2024.

Comments: This is an extended version of arXiv:2304.10196 which, apart from providing full proofs of all statements, takes a more categorical point of view to tell the whole story. In particular, we highlight and explain the underlying categorical constructions in detail

Canonical extensions via fitted sublocales

Authors: Tomáš Jakl, Anna Laura Suarez

Abstract: We build on a recent result stating that the frame $\mathsf{SE}(L)$ of strongly exact filters for a frame $L$ is anti-isomorphic to the coframe $\mathsf{S}_o(L)$ of fitted sublocales. The collection $\mathsf{E}(L)$ of exact filters of $L$ is known to be a sublocale of this frame. We consider several other subcollections of $\mathsf{SE}(L)$: the collections $\mathcal{J}(\mathsf{CP}(L))$ and… ▽ More We build on a recent result stating that the frame $\mathsf{SE}(L)$ of strongly exact filters for a frame $L$ is anti-isomorphic to the coframe $\mathsf{S}_o(L)$ of fitted sublocales. The collection $\mathsf{E}(L)$ of exact filters of $L$ is known to be a sublocale of this frame. We consider several other subcollections of $\mathsf{SE}(L)$: the collections $\mathcal{J}(\mathsf{CP}(L))$ and $\mathcal{J}(\mathsf{SO}(L))$ of intersections of completely prime and Scott-open filters, respectively, and the collection $\mathsf{R}(L)$ of regular elements of the frame of filters. We show that all of these are sublocales of $\mathsf{SE}(L)$, and as such they correspond to subcolocales of $\mathsf{S}_o(L)$, which all turn out to have a concise description. By using the theory of polarities of Birkhoff, one can show that all of the structures mentioned above enjoy universal properties which are variations of that of the canonical extension. We also show how some of these subcollections can be described as polarities and give three new equivalent definitions of subfitness in terms of the lattice of filters. △ Less

Submitted 28 April, 2024; originally announced April 2024.

A categorical account of composition methods in logic

Authors: Tomáš Jakl, Dan Marsden, Nihil Shah

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 behaves under composition and transformation of model… ▽ More 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 behaves 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. △ Less

Submitted 24 April, 2023; v1 submitted 20 April, 2023; originally announced April 2023.

Discrete density comonads and graph parameters

Authors: Samson Abramsky, Tomáš Jakl, Thomas Paine

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 theore… ▽ More 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. △ Less

Submitted 25 May, 2022; v1 submitted 13 May, 2022; originally announced May 2022.

A game comonadic account of Courcelle and Feferman-Vaught-Mostowski theorems

Authors: Tomáš Jakl, Dan Marsden, Nihil Shah

Abstract: Game comonads, introduced by Abramsky, Dawar and Wang, and developed by Abramsky and Shah, give a categorical semantics for model comparison games. We present an axiomatic account of Feferman-Vaught-Mostowski (FVM) composition theorems within the game comonad framework, parameterized by the model comparison game. In a uniform way, we produce compositionality results for the logic in question, and… ▽ More Game comonads, introduced by Abramsky, Dawar and Wang, and developed by Abramsky and Shah, give a categorical semantics for model comparison games. We present an axiomatic account of Feferman-Vaught-Mostowski (FVM) composition theorems within the game comonad framework, parameterized by the model comparison game. In a uniform way, we produce compositionality results for the logic in question, and its positive existential and counting quantifier variants. Secondly, we extend game comonads to the second order setting, specifically in the case of Monadic Second Order (MSO) logic. We then generalize our FVM theorems to the second order case. We conclude with an abstract formulation of Courcelle's algorithmic meta-theorem, exploiting our earlier developments. This is instantiated to recover well-known bounded tree-width and bounded clique-width Courcelle theorems for MSO on graphs. △ Less

Submitted 11 May, 2022; originally announced May 2022.

Generalizations of Bilinear Maps -- Technical Report

Authors: Tomáš Jakl, Dan Marsden, Nihil Shah

Abstract: Bilinear maps and their classifying tensor products are well-known in the theory of linear algebra, and their generalization to algebras of commutative monads is a classical result of monad theory. Motivated by constructions needed in categorical approaches to finite model theory, we generalize the notion of bimorphism much further. To illustrate these maps are mathematically natural notions, we s… ▽ More Bilinear maps and their classifying tensor products are well-known in the theory of linear algebra, and their generalization to algebras of commutative monads is a classical result of monad theory. Motivated by constructions needed in categorical approaches to finite model theory, we generalize the notion of bimorphism much further. To illustrate these maps are mathematically natural notions, we show that many common axioms in category theory can be phrased as certain morphisms being bimorphisms. We also show that much of the established theory of bimorphisms goes through in much greater generality. Our results carefully identify which assumptions are needed for the different components of the theory, including when good properties hold globally, or can at least be established locally. We include a brief string diagrammatic account of the bimorphism axiom, and conclude by recovering a simple proof of a classical theorem, emphasizing the efficacy of the bimorphism perspective. △ Less

Submitted 11 May, 2022; originally announced May 2022.

Lovász-Type Theorems and Game Comonads

Authors: Anuj Dawar, Tomáš Jakl, Luca Reggio

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 an… ▽ More 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. △ Less

Submitted 7 May, 2021; originally announced May 2021.

Comments: 23 pages. To appear in the Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2021)

A duality theoretic view on limits of finite structures: Extended version

Authors: Mai Gehrke, Tomáš Jakl, Luca Reggio

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 -- v… ▽ More 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. △ Less

Submitted 17 January, 2022; v1 submitted 17 December, 2020; originally announced December 2020.

Comments: arXiv admin note: text overlap with arXiv:1907.04036

Journal ref: Logical Methods in Computer Science, Volume 18, Issue 1 (January 19, 2022) lmcs:6996

A Cook's tour of duality in logic: from quantifiers, through Vietoris, to measures

Authors: Mai Gehrke, Tomas Jakl, Luca Reggio

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' and `struc… ▽ More 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' and `structure' strands in computer science. △ Less

Submitted 30 July, 2020; originally announced July 2020.

Comments: 29 pages

Canonical extensions of locally compact frames

Authors: Tomáš Jakl

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 e… ▽ More 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. △ Less

Submitted 8 October, 2019; originally announced October 2019.

MSC Class: 06D22; 06B35; 06B23

A duality theoretic view on limits of finite structures

Authors: Mai Gehrke, Tomáš Jakl, Luca Reggio

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 measures arises --- via Stone-Priestley… ▽ More 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 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. △ Less

Submitted 7 January, 2020; v1 submitted 9 July, 2019; originally announced July 2019.

Comments: 19 pages

Free constructions and coproducts of d-frames

Authors: Tomáš Jakl, Achim Jung

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. 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. △ Less

Submitted 23 April, 2017; v1 submitted 13 April, 2017; originally announced April 2017.