*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] graph theory in isabelle - nominal?*From*: Ramana Kumar <rk436 at cam.ac.uk>*Date*: Mon, 30 Jan 2012 08:45:54 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <A716DCAC-864D-447B-82A6-FD66E28FBA36@cam.ac.uk>*References*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk> <CAMej=26a_-=mzZF_uAuuH0JcjfF-Y8QY6CdWVnDuVO-YhYEUDw@mail.gmail.com> <A716DCAC-864D-447B-82A6-FD66E28FBA36@cam.ac.uk>*Sender*: ramana.kumar at gmail.com

On Mon, Jan 30, 2012 at 7:41 AM, John Wickerson <jpw48 at cam.ac.uk> wrote: > > 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. 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.

**Follow-Ups**:**Re: [isabelle] graph theory in isabelle - nominal?***From:*Thomas Sewell

**References**:**[isabelle] graph theory in isabelle - nominal?***From:*John Wickerson

**Re: [isabelle] graph theory in isabelle - nominal?***From:*Ramana Kumar

**Re: [isabelle] graph theory in isabelle - nominal?***From:*John Wickerson

- Previous by Date: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Date: [isabelle] soundness of Isabelle/HOL
- Previous by Thread: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Thread: Re: [isabelle] graph theory in isabelle - nominal?
- Cl-isabelle-users January 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list