Visual Language for Databases
Christian Williams
Wed Feb 14 2024
There is a visual language (see also this post) for databases, in the framework proposed by Evan & David et al., where a schema is a regular category. A data type A can be drawn as a string, and a predicate R on \Pi A_i can be drawn as a box with a list of strings.
In a database, R is a table in which each A_i is a column, and each row is a tuple (a_1,\dots, a_n) which satisfies R. This is generally the most popular way to organize data: the relation-based SQL is the most widely use database language.
Predicates are bifibered over sets, meaning that we can “push and pull” along functions.
In a database, this gives two basic operations we can do on tables:
- we can push forward along a function: f_!Q(\vec{a}) = \Sigma \vec{x}. Q(\vec{x})\land (f\vec{x}=\vec{a}),
- or we can substitute along a function: R[f](\vec{x}) = R(f\vec{x}).
Together, these two constructions give the basic database operations:
- select columns: push forward along projections, (see SQL Select)
- join tables on a column: substitute along the diagonal. (see SQL Join)
(This was described by Michael Lambert here; now we’re just showing its visual form.)
Composing these operations with other predicates, we can express the ubiquitous select-from-where query of SQL: the diagram below gives the table of tuples (a_i,\dots, a_j) satisfying \varphi which formed part of a row in R.
In particular, the predicate is often given by applying a function and then relating to some value of another data type, such as “employee.salary > $100”.
So in this visual language, we can express the standard data operations, and far more.
Once we create a visual editor for public use, people can use this intuitive interface to create schemas of their own, and explore the world in a new and fruitful way.
Cole Comfort
Mon Feb 26 2024
This looks very similar to Bonchi et al.'s graphical calculus for the linear bicategory of relations… and I suspect it may be the same.
Conceptually, this takes regular logic, the internal logic of sets and relations with the existential composition of relations… and then extends it to first order logic, the internal logic of sets relations with respect to both the usual existential composition, as well as the universal composition. By this, I mean where one regards sets and relations with these two compositions considered as a linear bicategory. This means that both compositions interact lax-Frobeniusly, categorifying a star-autonomous category
If you asked Nathan, he would say that Peirce had this idea back in the 19th century.
Christian Williams
Mon Feb 26 2024
Yes, I understand. But I think Mellies’ Bifibrational Construction of Hyperdoctrines is the most clear: rather than just defining the two opposite kinds of composition, we can notice that the universal/disjunctive fragment is precisely the fiberwise opposite of the existential/conjunctive fragment. Then because the fibers are Boolean algebras, which are star-autonomous by the negation operator, we can draw wires as oriented, and negation as reversing orientation. Universal and disjunction are then drawn as their double-negation encodings; so visual composition can always be interpreted literally via existence and conjunction. I think this is both more faithful to the logical duality, and more practical than the white/black method (though it does look cool).
Moreover, none of these works has explicit entailment; they only have the internal implication operator, and in/equalities between separate diagrams. Entailment can be drawn simply as nesting boxes from inner to outer — but none of them did this, I think just because they were already using the outward direction for negation. Yet by considering profunctors between bifibrations (my thesis, Section 2.3 “Matrix Profunctors”), we can use these “rings” between oriented wires to express both entailment and negation:
>|> means P\vdash Q
< | < means \overline{P}\vdash \overline{Q}
> | < means \overline{P}\vdash Q
< | > means P\vdash \overline{Q}
So I’ll be making a follow-up post soon, but the above is a quick summary; I think there is a canonical visual language of first-order logic, and the existing works have gotten very close. Of course, this is just what I think; all thoughts welcome.
Christian Williams
Wed Feb 28 2024
After some thought, I take it back: your white/black imagery* will be much easier for people, because it makes negation totally clear – but only if we make a visual tool in which anyone can easily construct these diagrams. If we only have pencil and paper, then I think oriented wires is practical.
*(or maybe white/grey, with just black for wires and boxes, to be easier on the eyes)
Cole Comfort
Thu Feb 29 2024
It is not my paper, but I believe that the colour-swapping is only aesthetic. It would be completely impractical to do this on a whiteboard, haha. If one draws the un-negated regular fragment as string diagrams for monoidal categories, and moreover if one draws negation as boxes, then the alternation of quantifiers can be deduced by how many boxes the formula is nested within.
Also, I think that the entailment should correspond to cut elimination. And since this is a categorification of multiplicative linear logic, I think that the cut elimination corresponds to applying the frobeniusator.
Alessandro Di Giorgio
Thu Feb 29 2024
For proofs on the whiteboard I usually mark the squares with a plus and a minus in their top corners. Of course doing it this way you kinda lose the negation-as-color-switch feature. If I have time I’d like to develop a visual editor and, actually, my big hope is to turn the contents of this paper into an interactive proof assistant