Difference between revisions of "Public:Known Game Comonads"
m (forgot to delete from copy-paste) |
m (let's be more explicit about the logics) |
||
Line 1: | Line 1: | ||
<div style="display:none;"><math> |
<div style="display:none;"><math> |
||
\newcommand\Ck{\mathbb C_k} |
\newcommand\Ck{\mathbb C_k} |
||
\newcommand\Lk{\mathcal L_k} |
|||
\newcommand\Hom{\mathrm{Hom}} |
\newcommand\Hom{\mathrm{Hom}} |
||
\newcommand\qtq[1]{\quad\text{#1}\quad} |
\newcommand\qtq[1]{\quad\text{#1}\quad} |
||
Line 15: | Line 14: | ||
Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that |
Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that |
||
# $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists \ |
# $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists^+ \mathcal L} B$$ |
||
# $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\ |
# $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\mathcal L} B$$ |
||
# $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\ |
# $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\mathcal L^\#} B$$ |
||
where $$\exists \ |
where $$\exists^+ \mathcal L$$ is the existential-positive fragment of a certain logic $$\mathcal L$$ and $$\mathcal L^\#$$ is the extension of $$\mathcal L$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$. |
||
Line 24: | Line 23: | ||
! '''Comonad''' |
! '''Comonad''' |
||
! $$\Ck$$ |
! $$\Ck$$ |
||
! '''Logic''' |
! '''Logic''' $$\mathcal L$$ |
||
! $$\leftrightarrows_k$$ |
! $$\leftrightarrows_k$$ |
||
! $$\leftrightarrow_k$$ |
! $$\leftrightarrow_k$$ |
||
Line 32: | Line 31: | ||
| Pebbling |
| Pebbling |
||
| $$\mathbb P_k$$ |
| $$\mathbb P_k$$ |
||
| $$k$$-variable fragment of FO |
| $$k$$-variable fragment $$\mathcal L^k$$ of FO |
||
| $$\exists^+ \mathcal L^k$$ |
|||
| ✓ |
|||
| |
| $$\mathcal L^k$$ with <br> $$I$$-morphisms |
||
| |
| $$(\mathcal L^k)^\#$$ with <br> $$I$$-morphisms |
||
| tree width $${\leq} k$$ |
| tree width $${\leq} k$$ |
||
|- |
|- |
||
| Ehrenfeucht-Fraissé |
| Ehrenfeucht-Fraissé |
||
| $$\mathbb E_k$$ |
| $$\mathbb E_k$$ |
||
| quantifier rank $${\leq} k$$ fragment of FO |
| quantifier rank $${\leq} k$$ fragment $$\mathcal L_k$$ of FO |
||
| $$\exists^+ \mathcal L_k$$ |
|||
| ✓ |
|||
| |
| $$\mathcal L_k$$ with <br> $$I$$-morphisms |
||
| |
| $$(\mathcal L_k)^\#$$ with <br> $$I$$-morphisms |
||
| tree depth $${\leq} k$$ |
| tree depth $${\leq} k$$ |
||
|- |
|- |
||
| Modal (*) |
| Modal (*) |
||
| $$\mathbb M_k$$ |
| $$\mathbb M_k$$ |
||
| modal depth $${\leq} k$$ fragment of ML |
| modal depth $${\leq} k$$ fragment $$\mathcal M_k$$ of ML |
||
| $$\exists^+ \mathcal M_k$$ |
|||
| ✓ |
|||
| $$\mathcal M_k$$ |
|||
| ✓ |
|||
| $$\mathcal M_k$$ + graded modalities |
|||
| ✓ |
|||
| synchronization tree<br>depth $${\leq} k$$ |
| synchronization tree<br>depth $${\leq} k$$ |
||
|- |
|- |
||
Line 57: | Line 56: | ||
| $$\mathbb {PR}_k$$ |
| $$\mathbb {PR}_k$$ |
||
| |
| |
||
| |
| a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$ |
||
| |
| |
||
| |
| |
||
Line 65: | Line 64: | ||
| $$\mathbb {PR}_{n,k}$$ [https://www.cst.cam.ac.uk/sites/www.cst.cam.ac.uk/files/_co_resources_online_workshop_game_comonads_generalised_quantifiers_2.pdf] |
| $$\mathbb {PR}_{n,k}$$ [https://www.cst.cam.ac.uk/sites/www.cst.cam.ac.uk/files/_co_resources_online_workshop_game_comonads_generalised_quantifiers_2.pdf] |
||
| extension of $$\mathcal L^k$$ with generalised quantifiers |
| extension of $$\mathcal L^k$$ with generalised quantifiers |
||
| |
| $$\exists^+ \mathcal L^k(\mathbf Q_n^H)$$ |
||
| |
| $$\mathcal L^k(\mathbf Q_n^H)$$ |
||
| |
| $$\mathcal L^k_{\infty,\omega}(\mathbf Q_n^H)$$ |
||
| $$n$$-ary generalised tree width $${\leq} k$$ |
| $$n$$-ary generalised tree width $${\leq} k$$ |
||
|- |
|- |
||
Line 79: | Line 78: | ||
|} |
|} |
||
The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark |
The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs. Note that $$\exists^+ \mathcal M_k$$ denotes the positive $$\Box$$-free fragment of $$\mathcal M_k$$. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark logic $\mathcal L$ such that they correspond to $\equiv^{\mathcal L}$ of that logic. |
Revision as of 18:35, 15 May 2020
In this page we gather the list all comonads we've explored so far.
Convention:
- $$A \leftrightarrows_k B$$ iff there exist homomorphisms $$\Ck A \to B$$ and $$\Ck B \to A$$
- $$A \leftrightarrow_k B$$ iff there exist non-empty sets $$F\subseteq \Hom(\Ck A, B)$$ and $$G\subseteq \Hom(\Ck B, A)$$ which are locally invertible
- $$A \cong_{\mathrm{Kl}(\Ck)} B$$ iff $$A$$ and $$B$$ are isomorphic in the coKleisly category for $$\Ck$$, i.e. there exist homomorphisms $$f\colon\Ck A \to B$$ and $$g\colon\Ck B \to A$$ such that both $$f^* g^*$$ and $$g^* f^*$$ are identities
Typically, each of those equivalences corresponds to a certain logical equivalence. That is, we have that
- $$A \leftrightarrows_k B \qtq{iff} A \equiv^{\exists^+ \mathcal L} B$$
- $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\mathcal L} B$$
- $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\mathcal L^\#} B$$
where $$\exists^+ \mathcal L$$ is the existential-positive fragment of a certain logic $$\mathcal L$$ and $$\mathcal L^\#$$ is the extension of $$\mathcal L$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.
Comonad | $$\Ck$$ | Logic $$\mathcal L$$ | $$\leftrightarrows_k$$ | $$\leftrightarrow_k$$ | $$\cong_{\mathrm{Kl}(\Ck)}$$ | Coalgebras |
---|---|---|---|---|---|---|
Pebbling | $$\mathbb P_k$$ | $$k$$-variable fragment $$\mathcal L^k$$ of FO | $$\exists^+ \mathcal L^k$$ | $$\mathcal L^k$$ with $$I$$-morphisms |
$$(\mathcal L^k)^\#$$ with $$I$$-morphisms |
tree width $${\leq} k$$ |
Ehrenfeucht-Fraissé | $$\mathbb E_k$$ | quantifier rank $${\leq} k$$ fragment $$\mathcal L_k$$ of FO | $$\exists^+ \mathcal L_k$$ | $$\mathcal L_k$$ with $$I$$-morphisms |
$$(\mathcal L_k)^\#$$ with $$I$$-morphisms |
tree depth $${\leq} k$$ |
Modal (*) | $$\mathbb M_k$$ | modal depth $${\leq} k$$ fragment $$\mathcal M_k$$ of ML | $$\exists^+ \mathcal M_k$$ | $$\mathcal M_k$$ | $$\mathcal M_k$$ + graded modalities | synchronization tree depth $${\leq} k$$ |
Pebble Relation | $$\mathbb {PR}_k$$ | a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$ | path width $${\leq} k$$ | |||
"Hella's game" | $$\mathbb {PR}_{n,k}$$ [1] | extension of $$\mathcal L^k$$ with generalised quantifiers | $$\exists^+ \mathcal L^k(\mathbf Q_n^H)$$ | $$\mathcal L^k(\mathbf Q_n^H)$$ | $$\mathcal L^k_{\infty,\omega}(\mathbf Q_n^H)$$ | $$n$$-ary generalised tree width $${\leq} k$$ |
Guarded Fragment Modal (*) | GF [2] |
The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs. Note that $$\exists^+ \mathcal M_k$$ denotes the positive $$\Box$$-free fragment of $$\mathcal M_k$$. The $$\leftrightarrows_k$$, $$\leftrightarrow_k$$, and $$\cong_{\mathrm{Kl}(\Ck)}$$ columns mark logic $\mathcal L$ such that they correspond to $\equiv^{\mathcal L}$ of that logic.