Re: [isabelle] graph theory in isabelle - nominal?



On Sun, Jan 29, 2012 at 1:24 PM, John Wickerson <jpw48 at cam.ac.uk> wrote:

> > 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).
>
> 2. 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?
>

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.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.