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



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.




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