Conjunctive Query

definition theorem example program

A conjunctive query over a relational schema is a formula built from relation atoms with only conjunction and existential quantification (and equality):

$$Q(x_1,\dots ,x_k)\leftarrow R_1({\vec{x}}_1),\dots ,R_n({\vec{x}}_n),$$

read “the tuples $(x_1,\dots ,x_k)$ for which there exist values of the remaining (bound) variables making every atom true”. These are the select–project–join queries of SQL, the bodies of Datalog rules, and the patterns of e-matching. Logically they are the regular fragment of first-order logic ($=,\top ,\wedge ,\exists$); categorically they are the morphisms of a cartesian bicategory of relations, drawn as string diagrams.

Sources: Chandra & Merlin, Optimal implementation of conjunctive queries in relational data bases, STOC 1977; Bonchi, Seeber & Sobociński, Graphical Conjunctive Queries, CSL 2018, arXiv:1804.07626 (notes) Definitions 1, 3, 4, 6, 16, 19, Propositions 2, 8, 9, Theorems 17, 31, 37; Fong & Spivak, Regular and relational categories: Revisiting ‘Cartesian bicategories I’, arXiv:1909.00069 (notes); Zhang, Wang, Willsey & Tatlock arXiv:2108.02290 (notes) §2 (conjunctive queries, AGM bound, worst-case optimal joins); 7 Sketches Ch. 6 and Undirected Wiring Diagram for the operadic picture.

Chandra–Merlin: containment is a homomorphism

Every conjunctive query $Q$ has a canonical database $D_Q$: one element per variable, one tuple per atom. Evaluating $Q$ on a database $D$ is the same as finding homomorphisms $D_Q\to D$ (the images of the head variables are the answers). From this:

Chandra–Merlin (1977). $Q_1\subseteq Q_2$ — every answer of $Q_1$ is an answer of $Q_2$, on every database — iff there is a homomorphism $D_{Q_2}\to D_{Q_1}$ that fixes the head variables.

So containment and equivalence of conjunctive queries are decidable (NP-complete), and every query has a unique minimal equivalent — its core. This is the Yoneda Lemma in miniature: a query is the representable functor $\mathrm{Hom}(D_Q,-)$, and inclusions of representables are maps the other way. Bonchi, Seeber and Sobociński make the analogy exact (Theorem 37 is literally a “preorder-enriched Yoneda” argument).

Graphical conjunctive queries

Bonchi et al. give a diagrammatic syntax, GCQ, whose terms are string diagrams built from relation symbols, copying and discarding (the comonoid), and their mirror images (the monoid that joins wires, i.e. equality and existential quantification). GCQ has the same expressive power as the usual calculus (Propositions 8–9), and inclusion of queries is axiomatised exactly by the laws of a cartesian bicategory:

Theorem 17. The precongruence generated by the cartesian bicategory axioms (Definition 16) coincides with semantic query inclusion.

Completeness goes through hypergraphs: diagrams are cospans of hypergraphs (Theorem 31, compare Double-Pushout Rewriting), and query inclusion reduces to the existence of a homomorphism between them — Chandra–Merlin, recovered categorically. The authors describe the resulting triangle — logic, combinatorics, categories — as the conjunctive-query counterpart of the Curry-Howard-Lambek Correspondence.

Evaluating them

Evaluation is a sequence of joins. The AGM bound bounds the output size by a fractional edge cover of the query hypergraph, and worst-case optimal join algorithms (generic join, leapfrog triejoin) meet it — which binary join plans cannot for cyclic queries such as the triangle query. Relational e-matching applies exactly this to e-graph pattern matching (E-Graph).

Sophia

Most queries in Sophia’s cookbook — “which tests cover this definition”, “find duplicated logic across languages”, e-matching a rewrite rule against stored terms — are conjunctive; the transitive ones (“what breaks if I change this”) add recursion and become Datalog (Least Fixed Point). See Query Cookbook.

JuliaLeanHaskell

Docs: Wiring diagrams · C-set morphisms · Graphs · ACSets API

using Catlab
# A database: a directed graph, i.e. one binary relation E(src, tgt).
G = @acset Graph begin V = 4; E = 4; src = [1, 2, 3, 3]; tgt = [2, 3, 4, 3] end
# The conjunctive query  Q(x, z) ← E(x, y), E(y, z)  as an undirected wiring diagram.
twostep = @relation (x = x, z = z) begin
    E(src = x, tgt = y)
    E(src = y, tgt = z)
end
ans = query(G, twostep)                      # a table: one column per head variable
sort(collect(zip(ans.x, ans.z)))   # [(1, 3), (2, 3), (2, 4), (3, 3), (3, 4)]
# Chandra–Merlin: Q1 ⊆ Q2 iff there is a homomorphism body(Q2) → body(Q1) fixing the head variables.
# Q2(x) ← E(x, y)            "x has an out-edge"
# Q1(x) ← E(x, y), E(y, y)   "x has an out-edge to a vertex with a self-loop"
body2 = @acset Graph begin V = 2; E = 1; src = [1]; tgt = [2] end
body1 = @acset Graph begin V = 2; E = 2; src = [1, 2]; tgt = [2, 2] end
!isnothing(homomorphism(body2, body1; initial = (V = Dict(1 => 1),)))   # true: Q1 ⊆ Q2
isnothing(homomorphism(body1, body2; initial = (V = Dict(1 => 1),)))    # true: Q2 ⊄ Q1 (no self-loop to map to)

import Mathlib
-- A conjunctive query is a formula with ∧ and ∃ only. Relational composition is the basic one:
def relComp {α β γ : Type*} (R : α → β → Prop) (S : β → γ → Prop) : α → γ → Prop :=
  fun x z => ∃ y, R x y ∧ S y z
 
-- Chandra–Merlin, the easy direction: a homomorphism of query bodies (here y ↦ y) gives containment.
-- Q1(x) ← E(x, y), E(y, y)   is contained in   Q2(x) ← E(x, y)
example {α : Type*} (E : α → α → Prop) (x : α) : (∃ y, E x y ∧ E y y) → ∃ y, E x y :=
  fun ⟨y, h, _⟩ => ⟨y, h⟩
 
-- composition of relations is associative: the two bracketings are equivalent queries
example {α : Type*} (R S T : α → α → Prop) (x w : α) :
    relComp (relComp R S) T x w ↔ relComp R (relComp S T) x w :=
  ⟨fun ⟨z, ⟨y, h1, h2⟩, h3⟩ => ⟨y, h1, z, h2, h3⟩, fun ⟨y, h1, z, h2, h3⟩ => ⟨z, ⟨y, h1, h2⟩, h3⟩⟩

-- Evaluating Q(x, z) <- E(x, y), E(y, z) by a nested-loop join
edges :: [(Int, Int)]
edges = [(1, 2), (2, 3), (3, 4), (3, 3)]
 
twostep :: [(Int, Int)]
twostep = [ (x, z) | (x, y) <- edges, (y', z) <- edges, y == y' ]
 
main :: IO ()
main = print twostep   -- [(1,3),(2,4),(2,3),(3,4),(3,3)]