Difference between revisions of "Public:Known Game Comonads"
m (adding Pebble Relation Comonad) |
m (adding GF Comonad) |
||
Line 18: | Line 18: | ||
# $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B$$ |
# $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B$$ |
||
# $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B$$ |
# $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B$$ |
||
where $$\exists \Lk$$ is the existential-positive fragment of $$\Lk$$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$. |
where $$\exists \Lk$$ is the existential-positive fragment of a certain logic $$\Lk$$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$. |
||
Line 24: | Line 24: | ||
! '''Comonad''' |
! '''Comonad''' |
||
! $$\Ck$$ |
! $$\Ck$$ |
||
! '''Logic''' |
|||
! $$\Lk$$ |
|||
! $$\leftrightarrows_k$$ |
! $$\leftrightarrows_k$$ |
||
! $$\leftrightarrow_k$$ |
! $$\leftrightarrow_k$$ |
||
Line 54: | Line 54: | ||
| synchronization tree<br>depth $${\leq} k$$ |
| synchronization tree<br>depth $${\leq} k$$ |
||
|- |
|- |
||
| Pebble Relation |
| [[Pebble Relation Comonad|Pebble Relation]] |
||
| $$\mathbb {PR}_k$$ |
| $$\mathbb {PR}_k$$ |
||
| |
| |
||
| ✓ wrt a fragment $$M^k$$ of $$\exists^+ |
| ✓ wrt a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$ |
||
| |
| |
||
| |
| |
||
| path width $${\leq} k$$ |
| path width $${\leq} k$$ |
||
|- |
|||
| "Hella's game" |
|||
| $$\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 |
|||
| for $$\exists^+ \mathcal L^k(\mathbf Q_n^H)$$ |
|||
| for $$\mathcal L^k(\mathbf Q_n^H)$$ |
|||
| for $$\mathcal L^k_{\infty,\omega}(\mathbf Q_n^H)$$ |
|||
| $$n$$-ary generalised tree width $${\leq} k$$ |
|||
|- |
|||
| Guarded Fragment Modal (*) |
|||
| GF [https://www.cst.cam.ac.uk/sites/www.cst.cam.ac.uk/files/guards.pdf] |
|||
| modal depth $${\leq} k$$ fragment of ML |
|||
| |
|||
| |
|||
| |
|||
| |
|||
|} |
|} |
||
Revision as of 18:16, 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 \Lk} B$$
- $$A \leftrightarrow_k B \qtq{iff} A \equiv^{\Lk} B$$
- $$A \cong_{\mathrm{Kl}(\Ck)} B \qtq{iff} A \equiv^{\Lk^\#} B$$
where $$\exists \Lk$$ is the existential-positive fragment of a certain logic $$\Lk$$ and $$\Lk^\#$$ is the extension of $$\Lk$$ by adding counting quantifiers $$\exists_{{\geq} n}$$ and $$\exists_{{\leq} n}$$.
Comonad | $$\Ck$$ | Logic | $$\leftrightarrows_k$$ | $$\leftrightarrow_k$$ | $$\cong_{\mathrm{Kl}(\Ck)}$$ | Coalgebras |
---|---|---|---|---|---|---|
Pebbling | $$\mathbb P_k$$ | $$k$$-variable fragment of FO | ✓ | ✓ with $$I$$-morphisms |
✓ with $$I$$-morphisms |
tree width $${\leq} k$$ |
Ehrenfeucht-Fraissé | $$\mathbb E_k$$ | quantifier rank $${\leq} k$$ fragment of FO | ✓ | ✓ with $$I$$-morphisms |
✓ with $$I$$-morphisms |
tree depth $${\leq} k$$ |
Modal (*) | $$\mathbb M_k$$ | modal depth $${\leq} k$$ fragment of ML | ✓ | ✓ | ✓ | synchronization tree depth $${\leq} k$$ |
Pebble Relation | $$\mathbb {PR}_k$$ | ✓ wrt 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 | for $$\exists^+ \mathcal L^k(\mathbf Q_n^H)$$ | for $$\mathcal L^k(\mathbf Q_n^H)$$ | for $$\mathcal L^k_{\infty,\omega}(\mathbf Q_n^H)$$ | $$n$$-ary generalised tree width $${\leq} k$$ |
Guarded Fragment Modal (*) | GF [2] | modal depth $${\leq} k$$ fragment of ML |
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 whether the equivalence in (1), (2), resp. (3) above holds.