As a follow up to Double Pushouts on Graphs I was trying to understand how things work when we add labels.
This caused me some confusion, because I was wondering "which label does the edge get, when two nodes are merged?" The mistaken assumption in that question is that the edges get merged as well when their endpoints are merged. But, to make the construction work, we have to operate with multigraphs that allow multiple edges between vertices.
(I ran into this when I was trying to test my Soffit code and realized I didn't know what label the edge should get.)
Here's a pushout on labelled graphs:
As far as my project goes, I need to think about whether this complexity is worth it. (Previously my input format did not need to name edges, which simplifies things a lot.) Other options:
- Keep graphs simple, but live with ambigous rules in which the edge could get either of the original labels.
- Disallow matches that would create such a condition.