*To*: Ramana Kumar <rk436 at cam.ac.uk>*Subject*: Re: [isabelle] graph theory in isabelle - nominal?*From*: John Wickerson <jpw48 at cam.ac.uk>*Date*: Mon, 30 Jan 2012 07:41:03 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAMej=26a_-=mzZF_uAuuH0JcjfF-Y8QY6CdWVnDuVO-YhYEUDw@mail.gmail.com>*References*: <12454106-4B8B-4F3A-B226-A2F02EA4044B@cam.ac.uk> <CAMej=26a_-=mzZF_uAuuH0JcjfF-Y8QY6CdWVnDuVO-YhYEUDw@mail.gmail.com>

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

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

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

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

- Previous by Date: Re: [isabelle] graph theory in isabelle - nominal?
- Next by Date: Re: [isabelle] graph theory in isabelle - nominal?
- 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