9
$\begingroup$

Higher structures in category theory lead very organically to visual or graphical interpretations in terms of string diagrams and commuting squares. However, it seems hard to implement a graphical calculus or reason about its metatheory.

I am aware of prior art like Epigram or Globular but not sure of the state of the art in the area of working with graphical calculi.

I feel like the easiest approach to get started might be to export data to external tools like Graphviz but this also feels pretty clumsy and limited.

How would I implement and reason about a graphical calculus or proof assistant?

$\endgroup$
4
  • 3
    $\begingroup$ There's also homotopy.io, but I have no idea how to answer. $\endgroup$ Aug 30, 2022 at 19:02
  • 2
    $\begingroup$ I'm enthusiastic, but "Visual Programming Languages" which, if still pursued, haven't gained wide adoption. I wonder if there might be unfortunate parallels. This paper formalizing Euclid's Elements is on my TBR list; I can't say for sure, but the abstract makes it seem relevant. $\endgroup$
    – user1168
    Aug 30, 2022 at 20:35
  • 1
    $\begingroup$ I actually tried doing this using PyQt5 / Python 3.x. If you'd like to see some screenshots or Zoom about it, ping me here or in chat. It's currently incomplete technically, and is still just a diagram editor. I was going to implement search for applicable logical rules using Python's networkx library and subgraph isomorphisms search. It actually is mostly implemented. I think though I want to try out something different though, and maybe rewrite in Qt/C++ (frontend) and D (backend kernel). Here are some old screencaptures: youtube.com/channel/UCkwSzrP8pr2uN4Mu04ktipg/videos $\endgroup$ Oct 3, 2022 at 7:20
  • 1
    $\begingroup$ My suggestion is don't work on the diagram editor (the frontend / visual part) first like I did. Think first about how you're going to handle the logical system. If you're looking for a partner in this endeavor. I'm ready to combine forces. :) Also realize, that if you limit yourself to categorical reasoning, then how will you implement diagram chasing proofs in HA in which sometimes you take elements and have to work with elementary expressions within a module? So it seems you have to not only implement categorical reasoning, but a full-fledged, general PA system. $\endgroup$ Oct 3, 2022 at 7:40

3 Answers 3

9
$\begingroup$

Your question is pretty broad.

How would I implement and reason about a graphical calculus or proof assistant?

First (almost tautologically) I think you need to carefully consider two questions:

  1. What does the visual side look like? What are the graphical requirements and how will the user interact with the graphics? On one extreme, the user is just typing text into a window and graphics change based on the text. On the other side the user has a video-game-level of interaction with the graphical display.
  2. What are the rules of the calculus? Any graphical calculus is going to have logical rules governing allowable actions and deductions. A simple calculus is no more than a puzzle like Sudoku or Rubik's cube. All you need to do is write code to make sure that users follow the rules of the calculus. A more complicated calculus would require implementing a more complicated logical kernel. Working in a functional language would likely help and connecting to existing theorem provers would be even better.

Option 1: Build a custom app

If graphics and interaction are most important to you, and the logic is relatively simple, then you may want to look into tools used by web developers and app designers. This isn't my area of expertise, but I believe they mostly use JavaScript or TypeScript, and tools like React on top of that. (Although, if you like functional programming I've heard mixed things about Scala JS which compiles Scala to JavaScript.) Leveraging existing tools and libraries might be the easiest way to make a good looking interface which you can distribute via a website.

Option 2: Lean's widgets

If the logical calculus is more important to you, then I would recommend Lean's widgets which are available in Lean 3 and Lean 4. Widgets are light-weight custom apps built into Lean which use HTML/JavaScript and show up in the infoview on the side of VSCode (and maybe Emacs?). In Lean's tactic mode, the Lean 3's goal view is a widget and gives the user some interactive ability to drill down into the terms in the goal by just clicking on them.

But widgets are much more flexible than that. Widgets have been used to make Rubik's cube and sudoku puzzles for example. As far as I can tell those examples don't have a lot of interaction with the user, except through Lean's code. Nonetheless, this could be a good first start, using Lean to develop an API for the structures and rules of the calculus and then generating pictures as the user manipulates the structures in Lean.

[Edit: Here is also a commutative diagram widget.] [Edit 2: There is a short demo of Widgets in the recent Lean users meeting.]

On the other hand, I think widgets do support a much stronger level of interaction. They use HTML and JavaScript (and Lean 4's widgets also use React?), so one should be able to make interactive interfaces if I understand correctly.

A big advantage of working in Lean, is that it is a language already designed for the logical side of things. It is functional and strongly typed and designed for theorem proving (Lean 4 is implemented in Lean 4). It could just be used as a programming language to build the widget backend, or you could even embed your logic into Lean's math libraries. For example, a graphical diagram chasing proof could generate a valid proof in Lean's category theory library (compare this question). You could also use Lean's tactic automation for automatically solving problems in your calculus.

$\endgroup$
1
  • 2
    $\begingroup$ Good practical suggestions and info. Time to learn Lean $\endgroup$
    – user1168
    Sep 1, 2022 at 1:31
5
$\begingroup$

A graphical proof assistant for higher categories under active development is homotopy.io, which follows the tradition of Globular. The underlying notion of higher structure used by homotopy.io is that of an associative $n$-category, which generalises string diagrams to higher dimensions.

There has been progress on the metatheory of homotopy.io such as a recent normalisation result, proving that homotopy.io indeed allows to talk about spaces is an open problem however as far as I know.

$\endgroup$
2
$\begingroup$

I've thought a lot about your question for about 5 years now. My current approach after tonight's brainstorm session is something like this:

enter image description here

What I did was flip to some small definition or theorem in my Topos Theory book by Johnstone, and there's one that goes:

Corollary. A topos is balanced (i.e. a morphism which is both mono and epi is an isomorphism).

So, I thought about how I would represent this definition in a general way so that the approach applies to many other definitions / theorems.

Here are some notes about the image:

The $C:\text{Cat}$ and the $f: \text{Mor}(C)$ are like logic gates on a mosfet transistor. Current can only flow if the gate is activated.

So the definition in usual text form is something like:

$$ \forall C:\text{Cat}, (C \text{ is balanced} \iff \forall f\in \text{Mor}(C), (f \text{ is mono & epi} \iff f \text{ is an isomorphism})) $$

Now the grey arrows disappear when the user views this definition visually. For example, the "and" node contains two pointers, one to the "f mono" node and one to the "f epi" node. So when you present this to the user you get something more like:

f mono
f epi  <=f:Mor(C)=>  f isom

But I expanded to the internal workings of the involved data structures for us, in that image.

Now the green text is probably just that: text strings. You parse out variables from them using a regex definition of variable or use a parser generator to define your variable syntax.

Internally, how this works is, when the user asserts that $C$ is a category, the first gate in the image gets activated, so if in addition they say that $C$ is balanced, then a signal (just a function call) triggers the definition expansion node (the stuff on the right) to activate. So then if in addition, if asserted or derived, somewhere along the line that $f$ is a morphism in $C$, as well as being mono and epi, then the conclusion is that $f$ is an isomorphism.

If you were to collect a bunch of these definitions and theorems into a single C++ driven graph, then activation of the relevant graph nodes would trigger an "electrical storm" through the graph, kind of like how our brains work.

That I think would be a very performant search method for searching for "what results if I assume X, Y, and Z"?


So given this design, what your visual graph needs to represent, and what you wont' find in current graph visualization architectures is Node-to-Node, Arrow-to-Node, and Arrow-to-Arrow connections. However, since you're already wanting to support categorical constructions, you'd need to support these connection types anyway! So you have the Commutative Diagram side of things, but you retrofit your diagram editor so that you can also visualize the logic engine nodes.

What's interesting about this approach, is that there exists only one node (unique) with the content $f \text{ epi}$ for example. You don't have one for each possible variable $f$, you use DeBruijn-like indexing in order to get a canonical form for the expression.

I still haven't figured out how to implement this myself, with all the variable substitution tracking that has to happen. Let's work together on this, or brainstorm even further.


One last thing, you should probably also support nesting of arrows and nodes within other nodes as well as node boxes at the $\implies$ and $\iff$ gates. You could probably do it without nesting as well. But then you definitely would need Arrow-to-Node and Arrow-to-Arrow connections.

$\endgroup$
1
  • 1
    $\begingroup$ First you would need a fast-enough graph canonization algorithm implemented such as Laszlo Babai's algorithm to handle look-up of CD graphs / expressions. Also note that you can fake node-to-arrow, etc connections (by making arrows into nodes with unique input / ouput pointers) as well as nesting of nodes (using a parent pointer) using a usual directed graph. I think this is the best way, because I have no idea how you'd adapt graph canonization to these more general types of graphs. Laszlo Babai's paper: par.nsf.gov/servlets/purl/10179675. $\endgroup$ Oct 3, 2022 at 19:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.