Stream: New Members & Projects

Topic: diagrammatic reasoning


view this post on Zulip Anthony Bordg (Jul 26 2019 at 22:31):

Is it possible to add diagrammatic support in Isabelle to reason formally with diagrams ?
I mean categorical diagrams for mathematics, quantum circuits for quantum computing, neural networks for machine learning ...

view this post on Zulip Josh Chen (Jul 29 2019 at 15:48):

Are you thinking actual diagrams, or more of the kind of thing done in the formalization of graph theory, for instance? The second sounds doable, although the first is what would be really fantastic, though I don't see that happening very quickly.

In any case, a formalization of something along the lines of say string diagrams for symmetric monoidal categories would be really nice, or more work on knot theory (there's already some stuff done, but I think a lot remains).

view this post on Zulip Anthony Bordg (Jul 29 2019 at 15:53):

Ok, since you're the second one today to ask for more details (the first one was Makarius), I'm going to write a few lines to give some details.

view this post on Zulip Anthony Bordg (Jul 29 2019 at 16:34):

I mean actual diagrams.
Specialised proof assistants like Globular, @Mateja Jamnik 's iCon and Quantomatic (for some flavour of higher categories, ontologies, string diagrams, respectively) use diagrammatic reasoning. However, none of the general-purpose proof assistants has these diagrammatic capabilities. Of course, no one wants to work with 4 or more proof assistants depending on the kind of work at hand. So, there is a need for a general-purpose proof assistant with diagrammatic support. Isabelle could be an ideal candidate for this work (with its simple, yet powerful, type theory).
As I said previously, there is a variety of possible diagrammatic supports, categorical diagrams for mathematics, neural networks for machine learning, quantum circuits for quantum computing ... Such diagrammatic support on top of isabelle/HOL would be terrific, but it may be very complicated . However, to have at least a framework, inside the generic Isabelle platform, dedicated to a specific topic like machine learning for instance and supporting neural networks as inputs to reason formally on them would be a very nice achievement.

ps: @Mateja Jamnik's Diamond was the first diagrammatic prover.

view this post on Zulip Josh Chen (Sep 04 2019 at 13:33):

The category theorists are starting to think about this: this https://arxiv.org/abs/1908.10660 is an ideas paper (somewhat light on technical details) that's being presented at SYCO in Birmingham right now.

view this post on Zulip Kevin Kappelmann (Sep 04 2019 at 13:53):

I am quite distant from (higher) category theory (I just know a little about it due to a course I took at the quantum group in Oxford that developed globular). I was wondering a few times before why these tools were written from scratch and not as some sort of plugin for existing ITPs. Maybe you have some more insight regarding these kind of provers and would be so kind to elaborate in simple terms what they try to accomplish and how they could be moved closer to ITPs like Isabelle?

view this post on Zulip Kevin Kappelmann (Sep 04 2019 at 13:55):

More generally speaking, I would like to see easy diagrammatic reasoning in ITPs (and would be willing to help to achieve that), so feel free to bombard me with (not too technical) information.

view this post on Zulip Anthony Bordg (Sep 04 2019 at 18:25):

@Kevin Kappelmann
I share Makarius's research (with his permission):

"My research so far: the main GUI platform where substantial diagram
editors already exists is HTML/CSS/JS, e.g. see
https://modeling-languages.com/javascript-drawing-libraries-diagrams
One could use something like that within Isabelle/VSCode and its builtin
Chromium browser window, or one could try with Chromium embedded into
Java/AWT/Swing for Isabelle/jEdit (see
https://bitbucket.org/chromiumembedded/java-cef). The latter project
might be worth some serious inspection, but I did not do anything myself
yet.
Chromium is another centralized infrastructure (by Google), but the
browser world seems to converge towards that. A bundled/embedded browser
within Isabelle/jEdit might work out in the quality we are used to already."

view this post on Zulip Kevin Kappelmann (Sep 05 2019 at 10:09):

Thanks Anthony! Let me say two things:

view this post on Zulip Anthony Bordg (Sep 11 2019 at 14:21):

Dear Kevin,

Thanks Anthony! Let me say two things:

thanks for your thoughts.

Have you ever tried to prove the commutativity of a diagram in an ITP ? It's painful.
However, it's still unclear what exactly a new user-interface should include.

view this post on Zulip Kevin Kappelmann (Sep 12 2019 at 13:05):

Have you ever tried to prove the commutativity of a diagram in an ITP ? It's painful.
However, it's still unclear what exactly a new user-interface should include.

I'm afraid, I haven't had the "pleasure" so far ;) Have you tried it in different ITPs already? If so, which one would you say is doing the best job at the moment? And if you do not mind giving me a brief summary before I get my hands dirty, what are the pain points of diagrammatic reasoning in general-purpose ITPs at the moment?

view this post on Zulip Josh Chen (Sep 12 2019 at 22:34):

what are the pain points of diagrammatic reasoning in general-purpose ITPs at the moment?

...there are no diagrams. ;)

But really, the same kind of pain that happens when you try to give a proof in topology in words only, without drawing pictures. You don't even need to use an ITP to see the problem: just try giving coherence conditions for higher categories by explicitly writing the algebraic equations with all the gory unitors/associators/commutators, instead of using commutative diagrams.

view this post on Zulip Kevin Kappelmann (Sep 13 2019 at 12:31):

Alright, I see the point. I also just had a glimpse at the category theory library of Lean. It does indeed look painful to state, manipulate, and just keeping track of things.

view this post on Zulip Anthony Bordg (Sep 16 2019 at 08:20):

Alright, I see the point. I also just had a glimpse at the category theory library of Lean. It does indeed look painful to state, manipulate, and just keeping track of things.

It was my experience too when I formalized monoidal categories in Coq.
Also, from the point of view of the reader it's not very legible without diagrams.

view this post on Zulip Anthony Bordg (Sep 22 2019 at 17:54):

@Kevin Kappelmann @Josh Chen
It might be difficult to input diagrams and reason formally on them, but a useful and more doable first step would be the following. Whenever it's relevant the user should be able to attach to his statement a diagram, so that the reader would be able to click on some icon associated with the statement and display the corresponding diagram.
JupyterLab for instance has nice visualization tools.

view this post on Zulip Kevin Kappelmann (Sep 22 2019 at 19:42):

Kevin Kappelmann Josh Chen
It might be difficult to input diagrams and reason formally on them, but a useful and more doable first step would be the following. Whenever it's relevant the user should be able to attach to his statement a diagram, so that the reader would be able to click on some icon associated with the statement and display the corresponding diagram.
JupyterLab for instance has nice visualization tools.

That sounds like a good first step indeed. I do not know if there is already some way to attach additional information to a definition/theorem in isabelle(?)


Last updated: Oct 12 2024 at 20:18 UTC