Mathematician uses category theory to explain how diagrams prove equations
How to prove equations using diagrams, part 1
E-graphs, the equality graphs behind tools like egg and egglog, are usually taught through union-find and implementation details. Evan Patterson asks what is really going on abstractly. He proposes initial functors as the key to diagrammatic equational reasoning, showing how pullbacks and extensions along them preserve solution sets, then works through examples like pasting commutative squares and a monoid presentation.
The diagrammatic and visual nature of e-graphs, so apparent in the interactive egglog demo, will suggest to any category theorist that categorical ideas may be implicitly at work.
- henearkr
Very interesting!!
A nitpick, for a J-shaped diagram D, J is the "index category" or the "scheme" of D, not the "shape" like written in the article.
- boldslogan
man ive recently stumbled on this concept of functor or nonsymbolic logic and such. don't suppose you have any suggestions to look at?