The Logic of Hypergraphs

Abstract

A celebrated theorem of Chandra and Merlin states that Conjunctive Queries inclusion is decidable. Its proof transforms logical formulas to hypergraphs: each query has a natural model – a kind of graph – and query inclusion reduces to the existence of a graph homomorphism between natural models.

In this talk, we introduce the diagrammatic language Graphical Conjunctive Queries (GCQ) and show that it has the same expressivity as Conjunctive Queries. GCQ terms are string diagrams, and their algebraic structure allows us to derive a sound and complete axiomatisation of query inclusion, which turns out to be exactly Carboni and Walters’ notion of cartesian bicategory of relations. Our completeness proof exploits the combinatorial nature of string diagrams as (certain cospans of) hypergraphs: Chandra and Merlin’s insights inspire a theorem that relates such cospans with spans. Completeness and decidability of the (in)equational theory of GCQ follow as a corollary. Categorically speaking, our contribution is a model-theoretic completeness theorem of free cartesian bicategories (on a relational signature) for the category of sets and relations.

Date
Friday, July 2, 2021 15:00 Europe/Paris
Event
GReTA seminar
Filippo Bonchi
Filippo Bonchi
Associate Professor in Computer Science

After his Ph.D (Pisa, 2008), Filippo Bonchi has been ERCIM fellow at CWI (Amsterdam) and École polytechnique (Paris). From 2010 to 2017, he worked at École Normale Supérieure (Lyon) as CNRS researcher. In 2018, he moved back to Pisa as Associate Professor. His research interests stand in the meet of Logic, Algebra and Theoretical Computer Science, with particular focus on Coinduction, Coalgebras, String Diagrams and, more generally, Category Theory. He contributed in a large variety of topics, including Automata Theory, Programming Languages, Abstract Interpretation, Algorithms for Model Checking, Data Bases and Relational Algebra and, more recently, the compositional study of Dynamical Systems (such as Signal Flow Graphs, Petri nets, passive and non-passive Electrical circuits). He regularly serves as PC member in top-class conferences of Theoretical Computer Science and has been chairing the Conference on ALgebra and COalgebra in computer science. His paper “Hacking Non-Determinism with Induction and Coinduction” appeared as cover story for Communication of the ACM.