Email Gateway (Aug 18 2022 at 19:01): Email Gateway (Aug 18 2022 at 19:01):From: John Wickerson <jpw48@cam.ac.uk>
Hello all,
I want to formalise a little bit of graph theory in Isabelle. (Specifically, I'm interested in directed labelled multigraphs.) In particular, I need a (disjoint) union operation on graphs. Here is a typical definition of this operation, which I've copied from a random textbook on graph theory:
Let G and H be two given graphs. The disjoint union of G and H, denoted by G \union H, is defined to be the graph with vertex set V(G) \union V(H), where V(G) and V(H) are made disjoint by renaming if necessary, and edge set E(G) \union E(H).
A couple of questions:
Is there already a theory of graphs in Isabelle? (A previous message [1] on this mailing list referred to a "HOL/Library/Graphs.thy" theory, but I couldn't find a theory at that location -- perhaps it's not there any more?)
If there isn't a pre-existing theory, and I roll my own instead, does anybody have any tips on how best to go about it? The phrase "made disjoint by renaming if necessary" smells a lot like Barendregt's variable convention for the lambda-calculus. So I'm wondering if I need Nominal Isabelle to formalise graph theory -- is that the case?
Thanks very much,
John
Email Gateway (Aug 18 2022 at 19:01):From: Ramana Kumar <rk436@cam.ac.uk>
A set-theoretic disjoint union of V(G) and V(H) might work, e.g. the graph
union has nodes (True, g) where g is in G and (False, h) where h is in H,
rather than explicit renaming.
I wouldn't think Nominal Isabelle is an obvious candidate because there's
no notion of variable binding in graphs (node names aren't variables,
they're not either free or bound, etc.). (Right?)
To make the disjoint union above work, I imagine your graphs would be a
polymorphic record where an "'a graph" has a record field that is its node
(multi)set, and nodes are elements of type "'a".
If you found a way to make renaming work instead, then the node multiset
could be non-polymorphic (e.g. a multiset of strings). For example you
could add characters to the end of all the node names in one graph as
necessary when you take a union... This could make it harder to recover the
components of a union, or prove properties about unions.
Email Gateway (Aug 18 2022 at 19:01):From: John Wickerson <jpw48@cam.ac.uk>
Hi Ramana, thanks for this. I like your suggestion of tagging nodes with True or False.
I wouldn't think Nominal Isabelle is an obvious candidate because there's no notion of variable binding in graphs (node names aren't variables, they're not either free or bound, etc.). (Right?)
Hm, well I think one could argue that, in fact, there is some sort of binding going on here, though it's rather simpler than in the lambda calculus, and is implicit. I pick names for each node in the graph, then use those names to define the graph's connectivity and assign labels to nodes or edges. But once the graph is drawn, I don't care about the names any more. So I think there's a tacit name-binding operation happening here.
John
Email Gateway (Aug 18 2022 at 19:01):From: Ramana Kumar <rk436@cam.ac.uk>
I see... you would want to identify graphs of the same shape just as we
identify alpha-equivalent lambda terms.
(And be allowed to define a function on graphs (that doesn't depend on the
names) by defining it on concrete (named) graphs, and having the system
lift it to up-to-isomorphism graphs.)
Nominal Isabelle does help with this in the case of lambda terms, but you
build the terms as an inductive data type with the binders at certain nodes.
The analogue for graphs would be to build graphs as an inductive datatype
(e.g. a constructor for a graph with n unconnected nodes, a constructor for
connecting two subgraphs at their nth and mth nodes).
Then you either leave the names out altogether, or have a binder at each
node.
The problem is that, unlike lambda terms, graphs may have more than one
largest proper subgraph, so you'd also want to quotient over different ways
of constructing the same graph.
Alternatively, you build graphs a more natural way (set of nodes + mset of
edges).
I don't know if Nominal Isabelle would deal with such a datatype correctly.
(The analogue of lambda terms in this style might be (set of (variable,
position) pairs, where a position is the number of left brackets before the
variable if you bracketed every subterm).)
But if it doesn't, you can always take the quotient type manually (and
thereby identify graphs of the same shape) with the quotient package.
It's more work than you might want, but you can at least express what you
mean.
Email Gateway (Aug 18 2022 at 19:01):From: Lars Noschinski <noschinl@in.tum.de>
I am currently developing some a theory of graphs, which can handle
directed labelled multigraphs (graphs are as a "'a set" of vertexes, a
"'b set" of edges and two projections mapping edges to their start and
end nodes).
It is not yet part of the Isabelle distribution. For the time being, you
can find it at (look at the master branch):
http://www21.in.tum.de/~noschinl/git/?p=graph-formalization.git
However, I don't provide an operation for disjoint union of graphs.
-- Lars
Email Gateway (Aug 18 2022 at 19:02):From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
My two cents worth: it might make more sense to use the quotient package than the nominal package. Your intuition is that graph equality should be naming-independent.
Define graphs as sets of pairs in some big-enough naming alphabet (naturals, strings, unspecified type 'a ...) and quotient by the equivalence relation of bijective renaming.
That should give you a new type whose notion of equality matches your intuition. You may then have a bit of work to do to define the syntax and operations you need within the new type. I've never used the quotient package and don't know how much it will help you here. I think you could, for instance, define your disjoint union operator on the pairwise representation (easy) then lift it to an operator in the graph type by showing it respects the equivalence relation (tool support desirable).
This is quite a different approach to Lars' so the relative merits should be thought about.
Yours,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 19 2024 at 08:19 UTC