nLab Ehrenfeucht-Fraïssé comonad

Contents

Contents

Idea

The Ehrenfeucht-Fraïssé comonad is a comonad introduced by Samson Abramsky and Nihil Shah? in Abramsky-Shah 2018, to study Ehrenfeucht-Fraïssé games.

If (σ)\mathcal{R}(\sigma) denotes the set of σ\sigma-structures, for σ\sigma a relational signature, there is a comonad 𝔼 k\mathbb{E}_k on (σ)\mathcal{R}(\sigma), where

  • The elements of 𝔼 k𝒜\mathbb{E}_k\mathcal{A} are finite nonempty sequences in 𝒜\mathcal{A}
  • CoKleisli morphisms 𝔼 k𝒜\mathbb{E}_k \mathcal{A} \to \mathcal{B} correspond to winning strateges for duplicator in the existential Ehrenfeucht-Fraïssé game of length kk, played from 𝒜\mathcal{A} to \mathcal{B}, i.e the one where spoiler only plays in 𝒜\mathcal{A}, duplicator only plays in \mathcal{B}, and the two substructures are only required to satisfy the same formulas from the positive existential fragment. The correspondence between strategies and coKleisli morphisms is that, given a sequence of choices by Spoiler a 1,a n𝒜a_1, \dots a_n \in \mathcal{A}, f(a 1,a n)f(a_1, \dots a_n) \in \mathcal{B} is the choice by Duplicator (supposed to correspond to a na_n.

There are also a description of the “proper” Ehrenfeucht-Fraïssé game in terms of this comonad, see Abramsky-Shah 2018 for more details.

Definition

Let (σ)\mathcal{R}(\sigma) be as above.

  • The underlying set of 𝔼 k(𝒜)\mathbb{E}_k(\mathcal{A}), given a σ\sigma-structure 𝒜\mathcal{A}, is, as noted above, the set of nonempty sequences a 1,a na_1, \dots a_n with nkn \leq k.
  • The action on functions is defined in the obvious way, 𝔼 k(f)(a 1,a n)=(f(a 1),f(a n))\mathbb{E}_k(f)(a_1, \dots a_n) = (f(a_1), \dots f(a_n)).
  • The counit is defined by ϵ(a 1,a n)=a n\epsilon(a_1, \dots a_n) = a_n
  • Given a relation symbol RσR \in \sigma, R(s 1,s m)R(s_1, \dots s_m) if and only if
    • For each i,ji,j, either s is_i is a prefix of s js_j and vice versa
    • And R(ϵ(s 1),,ϵ(s m))R(\epsilon(s_1), \dots, \epsilon(s_m)).
  • The comultiplication δ:𝔼 k(𝒜)𝔼 k𝔼 k𝒜\delta: \mathbb{E}_k(\mathcal{A}) \to \mathbb{E}_k\mathbb{E}_k\mathcal{A} is given by δ(a 1,a n)=((a 1),(a 1,a 2),(a 1,a n))\delta(a_1, \dots a_n) = ((a_1), (a_1,a_2), \dots (a_1, \dots a_n)), i.e by taking the sequence of prefixes of the sequence.

References

Similar game comonads, for other logic fragments:

  • Samson Abramsky, Anuj Dawar, and Pengming Wang. The pebbling comonad in finite model theory. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2017 (arXiv:1704.05124)
  • Samson Abramsky and Dan Marsden. Comonadic semantics for guarded fragments. 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE, 2021. (arXiv:2008.11094)
  • Adam Ó Conghaile and Anuj Dawar. Game Comonads & Generalised Quantifiers. 29th EACSL Annual Conference on Computer Science Logic. 2021. (arXiv:2006.16039)
  • Yoàv Montacute and Nihil Shah. The pebble-relation comonad in finite model theory. Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. 2022. (arXiv:2110.08196)

A survey on game comonads and their usage:

Last revised on June 21, 2024 at 08:04:28. See the history of this page for a list of all contributions to it.