The pebbling comonad in finite model theory
Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential kpebble games h...
| Main Authors: | , , |
|---|---|
| Format: | Conference item |
| Published: |
IEEE
2017
|
| _version_ | 1826269022047436800 |
|---|---|
| author | Abramsky, S Dawar, A Wang, P |
| author_facet | Abramsky, S Dawar, A Wang, P |
| author_sort | Abramsky, S |
| collection | OXFORD |
| description | Pebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential kpebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: • Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. • Symmetric games corresponding to equivalence in full k-variable logic are also characterized. • The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. • Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Furer- ¨ Immerman construction. • The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation. |
| first_indexed | 2024-03-06T21:18:33Z |
| format | Conference item |
| id | oxford-uuid:40a3dfc2-2b15-4a0d-ae2b-fcbbc06db125 |
| institution | University of Oxford |
| last_indexed | 2024-03-06T21:18:33Z |
| publishDate | 2017 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:40a3dfc2-2b15-4a0d-ae2b-fcbbc06db1252022-03-26T14:39:05ZThe pebbling comonad in finite model theoryConference itemhttp://purl.org/coar/resource_type/c_5794uuid:40a3dfc2-2b15-4a0d-ae2b-fcbbc06db125Symplectic Elements at OxfordIEEE2017Abramsky, SDawar, AWang, PPebble games are a powerful tool in the study of finite model theory, constraint satisfaction and database theory. Monads and comonads are basic notions of category theory which are widely used in semantics of computation and in modern functional programming. We show that existential kpebble games have a natural comonadic formulation. Winning strategies for Duplicator in the k-pebble game for structures A and B are equivalent to morphisms from A to B in the coKleisli category for this comonad. This leads on to comonadic characterisations of a number of central concepts in Finite Model Theory: • Isomorphism in the co-Kleisli category characterises elementary equivalence in the k-variable logic with counting quantifiers. • Symmetric games corresponding to equivalence in full k-variable logic are also characterized. • The treewidth of a structure A is characterised in terms of its coalgebra number: the least k for which there is a coalgebra structure on A for the k-pebbling comonad. • Co-Kleisli morphisms are used to characterize strong consistency, and to give an account of a Cai-Furer- ¨ Immerman construction. • The k-pebbling comonad is also used to give semantics to a novel modal operator. These results lay the basis for some new and promising connections between two areas within logic in computer science which have largely been disjoint: (1) finite and algorithmic model theory, and (2) semantics and categorical structures of computation. |
| spellingShingle | Abramsky, S Dawar, A Wang, P The pebbling comonad in finite model theory |
| title | The pebbling comonad in finite model theory |
| title_full | The pebbling comonad in finite model theory |
| title_fullStr | The pebbling comonad in finite model theory |
| title_full_unstemmed | The pebbling comonad in finite model theory |
| title_short | The pebbling comonad in finite model theory |
| title_sort | pebbling comonad in finite model theory |
| work_keys_str_mv | AT abramskys thepebblingcomonadinfinitemodeltheory AT dawara thepebblingcomonadinfinitemodeltheory AT wangp thepebblingcomonadinfinitemodeltheory AT abramskys pebblingcomonadinfinitemodeltheory AT dawara pebblingcomonadinfinitemodeltheory AT wangp pebblingcomonadinfinitemodeltheory |