Showing 1–10 of 10 results for author: Reggio, L

An invitation to game comonads

Authors: Samson Abramsky, Luca Reggio

Abstract: Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fraïssé games. Remarkably, the categories of coalgebras for these comonads capture preservation of several fragments of resource-bounded logics, such as (infinitary) first-order logic with n variables or bounded quantifier rank, and corresponding combinatorial parame… ▽ More Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fraïssé games. Remarkably, the categories of coalgebras for these comonads capture preservation of several fragments of resource-bounded logics, such as (infinitary) first-order logic with n variables or bounded quantifier rank, and corresponding combinatorial parameters such as tree-width and tree-depth. In this way, game comonads provide a new bridge between categorical methods developed for semantics, and the combinatorial and algorithmic methods of resource-sensitive model theory. We give an overview of this framework and outline some of its applications, including the study of homomorphism counting results in finite model theory, and of equi-resource homomorphism preservation theorems in logic using the axiomatic setting of arboreal categories. Finally, we describe some homotopical ideas that arise naturally in the context of game comonads. △ Less

Submitted 30 June, 2024; originally announced July 2024.

Comments: 42 pages

Finitely accessible arboreal adjunctions and Hintikka formulae

Authors: Luca Reggio, Colin Riba

Abstract: Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic (with finitely many variables) can be captured by transferrin… ▽ More Arboreal categories provide an axiomatic framework in which abstract notions of bisimilarity and back-and-forth games can be defined. They act on extensional categories, typically consisting of relational structures, via arboreal adjunctions. In the examples, equivalence of structures in various fragments of infinitary first-order logic (with finitely many variables) can be captured by transferring bisimilarity along the adjunction. In most applications, the categories involved are locally finitely presentable and the adjunctions finitely accessible. Drawing on this insight, we identify the expressive power of this class of adjunctions. We show that the ranks of back-and-forth games in the arboreal category are definable by formulae à la Hintikka. Thus, the relation between extensional objects induced by bisimilarity is always coarser than equivalence in infinitary first-order logic. Our approach relies on Gabriel-Ulmer duality for locally finitely presentable categories, and Hodges' word-constructions. △ Less

Submitted 25 April, 2023; originally announced April 2023.

Comments: 33 pages

Polyadic Sets and Homomorphism Counting

Authors: Luca Reggio

Abstract: A classical result due to Lovasz (1967) shows that the isomorphism type of a graph is determined by homomorphism counts. That is, graphs G and H are isomorphic whenever the number of homomorphisms from K to G is the same as the number of homomorphisms from K to H for all graphs K. Variants of this result, for various classes of finite structures, have been exploited in a wide range of research fie… ▽ More A classical result due to Lovasz (1967) shows that the isomorphism type of a graph is determined by homomorphism counts. That is, graphs G and H are isomorphic whenever the number of homomorphisms from K to G is the same as the number of homomorphisms from K to H for all graphs K. Variants of this result, for various classes of finite structures, have been exploited in a wide range of research fields, including graph theory and finite model theory. We provide a categorical approach to homomorphism counting based on the concept of polyadic (finite) set. The latter is a special case of the notion of polyadic space introduced by Joyal (1971) and related, via duality, to Boolean hyperdoctrines in categorical logic. We also obtain new homomorphism counting results applicable to a number of infinite structures, such as finitely branching trees and profinite algebras. △ Less

Submitted 11 November, 2021; v1 submitted 21 October, 2021; originally announced October 2021.

Comments: 40 pages. v3: Minor changes. Presentation improved

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)

Arboreal Categories: An Axiomatic Theory of Resources

Authors: Samson Abramsky, Luca Reggio

Abstract: Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intri… ▽ More Game comonads provide a categorical syntax-free approach to finite model theory, and their Eilenberg-Moore coalgebras typically encode important combinatorial parameters of structures. In this paper, we develop a framework whereby the essential properties of these categories of coalgebras are captured in a purely axiomatic fashion. To this end, we introduce arboreal categories, which have an intrinsic process structure, allowing dynamic notions such as bisimulation and back-and-forth games, and resource notions such as number of rounds of a game, to be defined. These are related to extensional or "static" structures via arboreal covers, which are resource-indexed comonadic adjunctions. These ideas are developed in a general, axiomatic setting, and applied to relational structures, where the comonadic constructions for pebbling, Ehrenfeucht-Fraïssé and modal bisimulation games recently introduced by Abramsky et al. are recovered, showing that many of the fundamental notions of finite model theory and descriptive complexity arise from instances of arboreal covers. △ Less

Submitted 9 August, 2023; v1 submitted 16 February, 2021; originally announced February 2021.

Journal ref: Logical Methods in Computer Science, Volume 19, Issue 3 (August 10, 2023) lmcs:9839

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

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

Quantifiers on languages and codensity monads

Authors: Mai Gehrke, Daniela Petrisan, Luca Reggio

Abstract: This paper contributes to the techniques of topo-algebraic recognition for languages beyond the regular setting as they relate to logic on words. In particular, we provide a general construction on recognisers corresponding to adding one layer of various kinds of quantifiers and prove a corresponding Reutenauer-type theorem. Our main tools are codensity monads and duality theory. Our construction… ▽ More This paper contributes to the techniques of topo-algebraic recognition for languages beyond the regular setting as they relate to logic on words. In particular, we provide a general construction on recognisers corresponding to adding one layer of various kinds of quantifiers and prove a corresponding Reutenauer-type theorem. Our main tools are codensity monads and duality theory. Our construction hinges on a measure-theoretic characterisation of the profinite monad of the free S-semimodule monad for finite and commutative semirings S, which generalises our earlier insight that the Vietoris monad on Boolean spaces is the codensity monad of the finite powerset functor. △ Less

Submitted 22 May, 2019; v1 submitted 28 February, 2017; originally announced February 2017.

Comments: 30 pages. Presentation improved and details of several proofs added. The main results are unchanged

ACM Class: F.1.1; F.4.1; F.4.3

Journal ref: Math. Struct. Comp. Sci. 30 (2020) 1054-1088

The Schützenberger product for syntactic spaces

Authors: Mai Gehrke, Daniela Petrisan, Luca Reggio

Abstract: Starting from Boolean algebras of languages closed under quotients and using duality theoretic insights, we derive the notion of Boolean spaces with internal monoids as recognisers for arbitrary formal languages of finite words over finite alphabets. This leads to a setting that is well-suited for applying existing tools from Stone duality as applied in semantics. The main focus of the paper is th… ▽ More Starting from Boolean algebras of languages closed under quotients and using duality theoretic insights, we derive the notion of Boolean spaces with internal monoids as recognisers for arbitrary formal languages of finite words over finite alphabets. This leads to a setting that is well-suited for applying existing tools from Stone duality as applied in semantics. The main focus of the paper is the development of topo-algebraic constructions pertinent to the treatment of languages given by logic formulas. In particular, using the standard semantic view of quantification as projection, we derive a notion of Schützenberger product for Boolean spaces with internal monoids. This makes heavy use of the Vietoris construction, and its dual functor, which is central to the coalgebraic treatment of classical modal logic. We show that the unary Schützenberger product for spaces, when applied to a recogniser for the language associated to a formula with a free first-order variable, yields a recogniser for the language of all models of the corresponding existentially quantified formula. Further, we generalise global and local versions of the theorems of Schützenberger and Reutenauer characterising the languages recognised by the binary Schützenberger product. Finally, we provide an equational characterisation of Boolean algebras obtained by local Schützenberger product with the one element space based on an Egli-Milner type condition on generalised factorisations of ultrafilters on words. △ Less

Submitted 27 March, 2016; originally announced March 2016.

Comments: 21 pages

ACM Class: F.1.1; F.4.1; F.4.3