Difference between revisions of "Public:Known Game Comonads"
m |
|||
Line 69: | Line 69: | ||
| $$n$$-ary generalised tree width $${\leq} k$$ |
| $$n$$-ary generalised tree width $${\leq} k$$ |
||
|- |
|- |
||
| [[Guarded Quantifier Comonads|Guarded quantifier]] |
|||
| Guarded Fragment |
|||
| $$\mathbb G^{\mathfrak g}_{k}$$ [https://www.cst.cam.ac.uk/sites/www.cst.cam.ac.uk/files/guards.pdf] |
| $$\mathbb G^{\mathfrak g}_{k}$$ [https://www.cst.cam.ac.uk/sites/www.cst.cam.ac.uk/files/guards.pdf] |
||
| $$\mathfrak g$$-guarded logic w/ width $$\leq k$$ |
| $$\mathfrak g$$-guarded logic w/ width $$\leq k$$ |
||
Line 77: | Line 77: | ||
| guarded treewidth |
| guarded treewidth |
||
|- |
|- |
||
| Loosely guarded |
| Loosely guarded |
||
| $$\mathbb{LG}_{k}$$ |
| $$\mathbb{LG}_{k}$$ |
||
| $$k$$-conjunct guarded logic |
| $$k$$-conjunct guarded logic |
Revision as of 12:56, 21 March 2021
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 exists a span of open pathwise embeddings $$R \to \Ck A$$ and $$R \to \Ck B$$
- $$A \cong_{\mathrm{Kl}(\Ck)} B$$ iff $$A$$ and $$B$$ are isomorphic in the coKleisli 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 FOL | $$\exists^+ \mathcal L^k$$ | $$\mathcal L^k$$ (wrt $$I$$-morphisms) | $$(\mathcal L^k)^\#$$ (wrt $$I$$-morphisms) | tree width $${<} k$$ |
Ehrenfeucht-Fraissé | $$\mathbb E_k$$ | quantifier rank $${\leq} k$$ fragment $$\mathcal L_k$$ of FOL | $$\exists^+ \mathcal L_k$$ | $$\mathcal L_k$$ (wrt $$I$$-morphisms) | $$(\mathcal L_k)^\#$$ (wrt $$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 trees, depth $${\leq} k$$ |
Pebble Relation | $$\mathbb {PR}_k$$ | $$k$$-variable logic, restricted $$\wedge$$ | a fragment $$M^k$$ of $$\exists^+ \mathcal L^k$$ | ?? | ?? | path width $${<} k$$ |
"Hella's game" | $$\mathbb H_{n,k}$$ [1] | extension of $$\mathcal L^k$$ with generalised quantifiers | $$\exists^+ \mathcal L^k(\mathcal Q_n^H)$$ | $$\mathcal L^k(\mathcal Q_n^H)$$ | $$\mathcal L^k_{\infty,\omega}(\mathcal{Q}_{n})$$ | $$n$$-ary generalised tree width $${\leq} k$$ |
Guarded quantifier | $$\mathbb G^{\mathfrak g}_{k}$$ [2] | $$\mathfrak g$$-guarded logic w/ width $$\leq k$$ | (identified) | (identified) | ?? | guarded treewidth |
Loosely guarded | $$\mathbb{LG}_{k}$$ | $$k$$-conjunct guarded logic | (identified) | ?? | ?? | hypertree-width |
Hypergraph comonad |
The comonads marked with ``(*)`` denote the comonads over the category of pointed labeled graphs with unary predicates. 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. Note that \(I\)-morphisms are simply homomorphisms w.r.t. an extended signature, see I-morphisms page.