Logic Enriched over a Quantale (slides) - HackMD

<style type="text/css"> .reveal ul { display: block; } .reveal ol { display: block; } .reveal { font-size: 24px; /* 20 of 24px */ } .reveal p { text-align: left; margin-top: 25px; margin-bottom: 25px; /* 0 or 25px */ } .custom-space { display: block; margin-top: 50px; /* Less space than <br> */ } .reveal h1, .reveal h2, .reveal h3, .reveal h4, .reveal h5, .reveal h6 { text-transform: none; /* no forced upper case in headings*/ } .reveal .slides section h1:after, /* not doing much*/ .reveal .slides section h2:after, .reveal .slides section h3:after { content: ''; flex-grow: 1; /* This will make the pseudo-element grow */ display: block; /* Converts the pseudo-element to a block, allowing it to be sized */ } </style> ## Logic Enriched over a Quantale <br> #### Glasgow, CALCO, June 16, 2025 <br> ###### Alexander Kurz ###### Chapman University <br> --- ## Introduction <br> 1. A Review of Coalgebraic Logic 2. Examples of Quantale Categories 3. Quantale Enriched Category Theory 2. Paramterizing CL by a Quantale --- ## 1. A Review of Coalgebraic Logic $$\newcommand{\cont}{{\bf I}}$$ --- ![image](https://hackmd.io/_uploads/H1s0VTK7xg.png)  --- ### Abstract Logic $(L,\delta)$ <br> ![image](https://hackmd.io/_uploads/Bk8duq3mlx.png) --- ### Concrete Logics $L_T\stackrel{\rm def}=PTSA$, $A$ finite defines an "abstract logic" $(L_T,\delta_T)$ **[Theorem](https://arxiv.org/pdf/1207.2732)**: $L_T$ has a presentation by predicate liftings and rank-1 axioms. More generally, a functor $L$ on a variety has a presentation iff $L$ preserves sifted colimits iff it is determined by finitely generated free algebras. A presentation turns an abstract logic into a concrete logic. The theorem states (roughly) that "all" abstract logics have a presentation. For any $T:\sf Set\to Set$, a concrete logic representing $(L_T,\delta_T)$ - respects bisismilarity - is complete - is expressive for finitary $T$ --- ### One-Step Properties Properties of logics that can be characterized category theoretically: ![image](https://hackmd.io/_uploads/rk9rTdhQeg.png) --- ### Order-Enriched CL <br> Quantale enriched coalgebraic logic has order-enriched coalgebraic logic as a special case. In the order enriched setting, the paradigmatic adjunction, instead of $\sf Set$ and $\sf BooleanAlgebra$, is the one of $\sf Poset$ and $\sf DistributiveLattice$. That case is well-behaved and much of CL generalizes, see eg [BKV 2015](https://arxiv.org/pdf/1402.5922). --- ## 2. Quantale Categories --- ### Quantales <br> **Def:** A **quantale** $(\Omega,\sqsubseteq, e,\cdot)$ is a monoid in the category of complete join semi-lattices. Multiplication is **residuated**, that is there are "implications" $\rhd$ and $\lhd$ such that: $$\quad a\le c \ {\color{magenta}\lhd}\ b \ \ \Leftrightarrow \ \ a\,{\color{magenta}\cdot}\, b \le c \ \ \Leftrightarrow \ \ b\le a \ {\color{magenta}\rhd}\ c$$ (if the quantale is commutative, then $a\lhd b=b\rhd a$) <br> **Def:** An **$\Omega$-category** $X$ is a category enriched over $\Omega$, that is, we have \begin{align*} e&\sqsubseteq X(x,x) & \text{ identity, reflexivity} \\[1ex] X(x,y)\cdot X(y,z) & \sqsubseteq X(x,z) & \text{ composition, transitivity} \end{align*} --- ### Examples <br> - Metric spaces, Distances, Truth Values - Multi-relational structures - Non-determinstic Automata - Graphs with shortest paths --- ### Distances <br> Elements of a quantale can be interpreted as "distances". For example, a category enriched over the *Lawvere Quantale* $\Omega=([0,\infty], \ge, 0, +)$ is a generalized metric space: \begin{align*} 0&= X(x,x) & \text{ reflexivity} \\[1ex] X(x,y) + X(y,z) & \ge X(x,z) & \text{ triangle inequality} \end{align*} (Distance may be not symmetric.) --- ### Truth Values <br> The elements of a quantale can be interpreted as "truth-values". Distance interpretation and the truth-value interpretation have opposite "natural order": Distance $0$ is "true" (top) and distance $\infty$ is "false" (bottom). For example, for the Lawvere Quantale, there is an order-reversing bijection $$[0,\infty] \to [0,1]$$ mapping addition to multiplication and $0\mapsto 1$, $\infty\mapsto 0$. The truth-value interpretation is common in fuzzy logic. --- ### Similarity Spaces <br> $\Omega=\mathbb N\cup\{\infty\}$ in the natural order with minimum as multiplication A non-symmetric $\Omega$-category is the set $W$ of finite and infinte words over an alphabet with $$W(w,v)$$ so that $W(w,v)=\infty$ if $w$ a prefix of $v$ and, otherwise, $W(w,v)=n$ the smallest $n$ that distinguishes $w_n$ and $v_n$. In this case, $\Omega$-categories are equivalent to ultrametric spaces. --- ### Constraint Solving Elements are sets of unsolved constraints. ![image](https://hackmd.io/_uploads/H1zUINp7gx.png) From Schiendorfer etal. [MiniBrass: Soft constraints for MiniZinc](https://link.springer.com/content/pdf/10.1007/s10601-018-9289-2.pdf). 2018 --- So far the quantales have been - **integral** (neutral element is top) and - **commutative**. These are common properties for distances and for truth-values. --- ### Multi-relational Structures Pictures from [Residuated Lattices of Size up to 6](https://math.chapman.edu/~jipsen/finitestructures/rlattices/RLlist3.pdf), N Galatos, P Jipsen - 2017. 2 relations: ![image](https://hackmd.io/_uploads/H1AplihXlg.png =200x) - [Gaifman 89]: causality > time - Lukasiewicz 3-chain - [Gaifman, Pratt 87]: prosset model, strict time > non-strict time Every quantale category can be interpreted as a multi-relational structure. The multi-relational structure corresponding to a generalized metric space $X$ is a [uniformity](https://en.wikipedia.org/wiki/Uniform_space#Entourage_definition): - For every $\epsilon\in[0,\infty]$ the relation $R_\epsilon =\{(x,y) \mid X(x,y)\le\epsilon\}$. --- ### The Smallest Non-Commutative Examples <br> ![image](https://hackmd.io/_uploads/SJej9snXex.png =330x) $\quad\quad$ ![image](https://hackmd.io/_uploads/Hysa9o2Qlg.png) --- ### Generalized Automata <br> $\mathcal P(\Sigma^\ast)$ is the free quantale over the set (alphabet) $\Sigma$. A $\mathcal P(\Sigma^\ast)$-category $X$ is a non-determinstic automaton: The hom $X(x,y)$ is the language of words $w\in X(x,y)$ such that there is a transition $$x\stackrel w\longrightarrow y$$ This generalises to automata over non-free monoids: If $M$ is a monoid then $\mathcal PM$ is the free quantale over $M$. --- ### Graphs with Shortest Paths Let $X$ be an $\Omega$-category. $X$ is a graph with edges labelled by elements from $\Omega$. The distance from $s$ to $t$ is the shortest path from $s$ to $t$: $$X(s,t) = \bigvee_x X(s,x)\cdot X(x,t)$$ In the distance interpretation: $\bigvee$ is infimum; $\cdot$ is $+$; $\sqsubseteq$ is "longer-equal"; $\rhd,\lhd$ are "minus": ![image](https://hackmd.io/_uploads/rJZAT6ENxe.png) Shortest paths construct the free $\Omega$-category over an $\Omega$-graph.  --- ### Quantale-Valued Matrices <br> Let $X$ be an $\Omega$-category. $X$ is a matrix with elements from $\Omega$. Using multiplication and joins, shortest path can be computed with the [Floyd-Warshall algorithm](https://en.wikipedia.org/wiki/Floyd%E2%80%93Warshall_algorithm). --- ## 3. Quantale Enriched Category Theory --- ### Relational Calculus A **weighted relation**, data-base table, formal context, monotone relation, profunctor, distributor, bimodule, $(X\times A)$-matrix, weakening relation, stable relation: $$\cont:X^o\times A \to \Omega$$ $$\color{magenta}{\cont: X\looparrowright A}$$ Presheaves, column vectors, **weighted downsets** $$\phi: X\looparrowright 1 \text{ are the elements of } \mathcal DX$$ Co-presheaves, row vectors, **weighted upsets** $$\psi: 1\looparrowright A \text{ are the elements of } \mathcal UA$$ Downsets and upsets are related by the "Isbell adjunction" ![image](https://hackmd.io/_uploads/HJh98IZgxe.png) --- ### "Bicategory" of Relations $\sf Rel$ <br> The category $\sf Rel$ of weighted relations is residuated with ![image](https://hackmd.io/_uploads/rkXM6-JVee.png)   Explicitely: $$ (R\blacktriangleright T) (y,z)=\bigwedge_{x\in X}R(x,y)\rhd T(x,z) \quad\quad (T\blacktriangleleft S)(x,y)=\bigwedge_{z\in Z} T(x,z) \lhd S(y,z) $$ $$(R\bullet S)(x,z) = \bigvee_y R(x,y)\cdot S(y,z)$$  --- ### Weighted (Co)Limits ![image](https://hackmd.io/_uploads/HyqT0T-exg.png) $$ B(\color{magenta}{{\rm colim}_\phi G},b) = \phi\blacktriangleright B(G,b) \quad\quad\quad\quad B(b, \color{magenta}{{\rm lim}_\psi G}) = B(b,G)\blacktriangleleft\psi $$ In the special case $D=1$ and $r$ the weight, "tensor" $\star$ and "power" $\uparrow$ are given by: $$ B(\color{magenta}{g\star r},b)=r \rhd B(g,b) \quad\quad\quad\quad B(b,\color{magenta}{g \uparrow r})= B(b,g)\lhd r $$ In [metric space examples](https://ir.cwi.nl/pub/4744/) where $r\in [0,\infty]$ and for "predicates" $g:X\to[0,\infty]$ we have - $g\star r\quad$ is $\quad g+r\quad$ (shift down) - $g \uparrow r\quad$ is $\quad g-r\quad$ (shift up) --- ## 4. Paramterizing CL by a Quantale --- ### Extending Functors to Quantale Categories All type constructors on sets can be extended to $\Omega\text{-cat}$ because the discrete functor $\sf Set\to \Omega\text{-cat}$ is dense in the $\Omega$-enriched sense. Every $T:\sf Set\to Set$ (and every $T:\sf Set\to \Omega\text{-cat}$) has an extension $$\overline T:\Omega\text{-cat}\to\Omega\text{-cat}$$ (The proof assumes commutativity, but I dont know whether this is necessary.) <br> For example, the extension of the powerset - to posets is the convex powerset with the Egli-Milner order. - ordered by inclusion is the upset functor with the backward simulation order. - ordered by reverse inclusion is downset with forward simulation. - to metric spaces is the compact powerset with the Hausdorff metric. <br> ([BKV 2019](https://arxiv.org/pdf/1809.02229) for commutative quantales, [DK 2017](https://drops.dagstuhl.de/storage/00lipics/lipics-vol072-calco2017/LIPIcs.CALCO.2017.9/LIPIcs.CALCO.2017.9.pdf) has poset examples) --- ### Relation Lifting Every relation $R: X\looparrowright Y$ can be tabulated as a cospan using the "collage" $\mathbf R$ of $R$ $$X\stackrel p \longrightarrow \mathbf R\stackrel q\longleftarrow Y$$ Conversely, every cospan gives rise to a relation $X\looparrowright Y$ $$\lambda x.\lambda y. \mathbf R(px,qy)$$ Functors $T:\Omega\text{-cat}\to \Omega\text{-cat}$ can be extended to relations $$\widehat T: Rel(\Omega)\to Rel(\Omega)$$ by applying them to the tabulating cospan: $$\lambda x.\lambda y. T\mathbf R(Tpx,Tqy)$$ ([Worrell 2000](https://scholar.google.com/scholar?hl=en&as_sdt=0%2C5&q=worrell+Coinduction+for+recursive+data+types%3A+partial+orders%2C+metric+spaces+and+%CE%A9-categories.&btnG=)) --- ### Cospan Bisimilarity Let $T:\Omega\text{-cat}\to\Omega\text{-cat}$. A relation $R: X\looparrowright Y$ is a **cospan bisimulation** if the unique function $\mathbf R\to T \mathbf R$ that makes the diagram $$ \begin{array}{} X & \rightarrow & \mathbf R & \leftarrow & Y\\ \downarrow &&\downarrow && \downarrow \\ TX & \rightarrow & \overline T \mathbf R & \leftarrow & TY \end{array} $$ commute is an $\Omega\text{-cat}$ morphism. --- ### Cospan Bisimilarity for Sets As an aside, cospan bisimilarity can be made to work for sets. Let $T:\sf Set\to Set$ and $\overline T$ its extension to posets. A relation $R\subseteq X\times Y$ is a **cospan bisimulation** if the unique function $\mathbf R\to T \mathbf R$ that makes the diagram $$ \begin{array}{} X & \rightarrow & \mathbf R & \leftarrow & Y\\ \downarrow &&\downarrow && \downarrow \\ TX & \rightarrow & \overline T \mathbf R & \leftarrow & TY \end{array} $$ commute is an $\Omega\text{-cat}$ morphism. --- ### Moss's Cover Modality For every functor $T:\Omega\text{-cat}\to\Omega\text{-cat}$ a set of formulas $\mathcal L$ and a modal operator $\nabla$ such that $$T\mathcal L\stackrel\nabla\longrightarrow\mathcal L$$ The semantics of $\nabla$ is defined as the relation lifting of the satisfaction relation ${\Vdash}:\mathcal L\looparrowright X$. Moss's theorem that the $\nabla$-logic is invariant under bisimulation generalizes to the $\Omega$-enriched setting. ([BKPV 2013](https://arxiv.org/pdf/1307.4682) assumes that $\Omega$ is commutative.) This shows one way to generalize coalgebraic logic for arbitrary commutative quantales. But it leaves open the question how to generalize the base logic. --- ### 2-Valued Modal Logic **Kripke models**: $\quad(X,R,V)$ $\quad X$ a set, $\quad R:X\times X\to {\color{magenta}2}$, $\quad V:X\times {\sf AtProp} \to {\color{magenta}2}$ **Language**: $\quad\mathcal L$ $\quad$ Boolean logic plus $\quad$ modal operators $\quad \Box p$, $\quad p\in {\sf AtProp}$ **Semantics**: $\quad {\Vdash} : X\times \mathcal L \to {\color{magenta}2}$ $\quad x\Vdash \Box p \ \ \Leftrightarrow \ \ \text{for all } y\in X, \text{ if } xRy \text{ then } y\Vdash p$ **Proof System**: $$ \begin{align} \Box\top &= \top\\ \Box(p\wedge q) &= \Box p \wedge \Box q \end{align} $$ --- ### Quantale-Valued Modal Logic **Kripke models**: $\quad(X,R,V)$ $\quad X$ an ${\color{magenta}\Omega\text{-cat}}$, $\quad R:X\times X\to {\color{magenta}\Omega}$, $\quad V:X\times {\sf AtProp} \to {\color{magenta}\Omega}$ **Language**: meets and joins plus modal operators $\quad \Box p$, $\quad p\in {\sf AtProp}$, $\quad$ plus <font color=magenta>tensor</font> and <font color=magenta>power</font> (and possibly constants for elements in $\Omega$). **Semantics**: $\quad {\Vdash} : X\times \mathcal L \to {\color{magenta}\Omega}$ $$ x\Vdash \Box p \ = \ {\color{magenta}\bigwedge}_{y\in X} \ \{ xRy \ {\color{magenta}\rhd} \ y\Vdash p \} $$ **Proof Theory:** $\quad {\vdash} : \mathcal L \times \mathcal L \to {\color{magenta}\Omega}$ $$ \frac { \phi \vdash_{\color{magenta}{\omega}} \chi \quad\quad \chi\vdash_{\color{magenta}{\omega'}}\psi} { \phi \vdash_{\color{magenta}{\omega \cdot \omega'}} \psi } $$ --- ### Duality ![image](https://hackmd.io/_uploads/rJzFLBpXlx.png) The algebras for the monad $\Omega^{\Omega^-}$ embody a logic for $\Omega\text{-cat}$. The monad $\Omega^{\Omega^-}$ is isomorphic to $\mathcal D\mathcal U$. There is a distributive law $\mathcal U\mathcal D \to \mathcal D\mathcal U$. This distributive law specializes to the one known for lattices but is difficult to spell out syntactically in terms of choice functions for a general $\Omega$. ([[BK 2016]](https://inria.hal.science/hal-01446037/file/418352_1_En_9_Chapter.pdf) assumes commutativity.) --- ### Completions of $\Omega$-categories --- ### Mac Neille Completion of a Relation $\cont:X\looparrowright A$ <br> $$\mathcal DX(\phi,\phi')=\phi\blacktriangleright\phi' \quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad \mathcal UA(\psi,\psi')=\psi \blacktriangleleft \psi'$$ ![image](https://hackmd.io/_uploads/H15WVIWxlg.png) --- ![image](https://hackmd.io/_uploads/H15WVIWxlg.png =800x) - ${\sf Collage}(\cont)\to\mathcal M(\cont)$ preserves limits and colimits. - The colimit of $X\to\mathcal M(\cont)$ weighted by $\phi\in\mathcal DX$ is $\phi\blacktriangleright\cont$. - The limit of $A\to\mathcal M(\cont)$ weighted by $\psi\in\mathcal UA$ is $\cont\blacktriangleleft\psi$. - $(\phi,\psi)\in\mathcal M(\cont)$ is the colimit of $X\to\mathcal M(\cont)$ weighted by $\phi$ and the limit of $A\to\mathcal M(\cont)$ weighted by $\psi$. --- ### Canonical Extension The canonical extension $C^\delta$ of a quantale space $C$, parameterised by "filters" $F\subseteq\mathcal UC$ and "ideals" $I\subseteq\mathcal DC$, is the MacNeille completion of the relation $\cont:F\looparrowright I$ given by $$ \cont (f,i) = \bigsqcup_c f(c)\cdot i(c). $$ ![image](https://hackmd.io/_uploads/BJvAd0Wegl.png) --- ![image](https://hackmd.io/_uploads/BJvAd0Wegl.png) \begin{gather*} {\rm lim}_f\,[-] = \bar f \quad\quad {\rm colim}_i\,[-] = \bar i \\ (\phi,\psi) = {\rm colim}_\phi\, \bar{()} = {\rm lim}_\psi\, \bar{()} \end{gather*} **Theorem:** - **(Density)** Every $\kappa\in C^\delta$ is the colimit of a limit of $C$ and the limit of a colimit of $C$. - **(Compactness)** $C^\delta(\lim_f [-],{\rm colim}_{i}[-])=\cont (f,i).$ --- ## Conclusions The aim of this research program is to add to the parameter $$T:\sf Spa\to Spa$$ of coalgebraic logic another dimension, namely a quantale $$\Omega$$ There are a number of encouraging results. It is not always clear which results can be expected to generalize to the non-commutative case. The distributive law between the upset and the downset monad can be difficult to characterize syntactically. There are many applications of many-valued logics in particular in semantics of programming languages and in fuzzy logic. The connections to the general framework sketched in this talk need to be worked out. --- ### Coauthors <br> Octavian Babus Adriana Balan Marta Bilkova Fredrik Dahlqvist Giuseppe Greco Daniela Petrisan Wolfgang Poiger Bruno Teheux Apostolos Tzimoulis Jiri Velebil --- ## Selected Quantale References 1. F.W. Lawvere. Metric spaces, generalized logic and closed categories. 1973. 1. R. Betti and S. Kasangian. A quasi-universal realization of automata, 1982. 1. Jan Rutten. Elements of generalized ultrametric domain theory. 1995. 1. Jan Rutten. Weighted colimits and formal balls in generalized metric spaces. 1998. 1. Casley, Crew, Meseguer, Pratt. Temporal structures. 2005. 1. George Metcalfe. Fundamentals of fuzzy logic. 2005. 1. Isar Stubbe. Categorical structures enriched in a quantaloid. 2005. 1. Dusko Pavlovic. Quantitative concept analysis. 2012. 1. Simon Willerton. Tight spans, Isbell completions and semi-tropical modules. 2013. 1. Richard Garner. Topological functors as total categories. 2014 1. Galatos, Jipsen. Residuated lattices up to size 6. 2017. 1. Hofmann, Stubbe. Topology from enrichment: the case of partial metrics. 2018 1. Schiendorfer, Knapp, Anders, Reif. MiniBrass: soft constraints for MiniZinc. 2018.