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



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




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