Anthony Bordg (Jul 26 2019 at 22:31): 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 ...
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).
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.
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.
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.
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?
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.
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."
Kevin Kappelmann (Sep 05 2019 at 10:09):Thanks Anthony! Let me say two things:
I would be in favour of using a web-based framework so that it can easily be transported between
VSCode has a webview API at hand, which could be used for this. I am not a big fan of blowing up the Isabelle distribution even more and bundle a browser. Maybe it would be worth completely migrating Isabelle to VSCode and drop jEdit first, but I have no idea about what is missing to do that besides what has been said here.
I still do not know what the requirements of category theorists are for ITPs. Why is it that they developed their own tools so far? What needs to be done so that they can do the same thing in more general-purpose ITPs? Maybe I should just read the papers and ask again...(?)
Anthony Bordg (Sep 11 2019 at 14:21):Dear Kevin,
Thanks Anthony! Let me say two things:
I would be in favour of using a web-based framework so that it can easily be transported between
- different editors (jEdit, VSCode, some potential online version of Isabelle in the future) and
- different theorem provers (most of them will use an editor that supports some sort of webview).
VSCode has a webview API at hand, which could be used for this. I am not a big fan of blowing up the Isabelle distribution even more and bundle a browser. Maybe it would be worth completely migrating Isabelle to VSCode and drop jEdit first, but I have no idea about what is missing to do that besides what has been said here.
thanks for your thoughts.
- I still do not know what the requirements of category theorists are for ITPs. Why is it that they developed their own tools so far? What needs to be done so that they can do the same thing in more general-purpose ITPs? Maybe I should just read the papers and ask again...(?quote
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.
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?
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.
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.
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.
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.
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: Jul 15 2022 at 23:21 UTC