Subgraph Isomorphism with backtracking

[mstn]

Context

Before applying rewrites, we need a way to find matches. This is a subgraph isomorphism problem. Here, we provide a simple implementation of VF2.

Details

• SubgraphIsomorphism can be created only via find_subgraph_isomorphism and find_subgraph_isomorphism_by methods that guarantee that it is actually a morphism. We can use it as input for rewrite function in here Rewriting for Lax Hypergraphs #20 where we may relax assertions on the candidate match.
• There are many "pruning" strategies we can apply to reduce the state space blowup. I think we should find a compromise between code readability and "best effort". For big graphs or special cases, we might even considering using a specialized external solver.
• Note: matching is order sensitive for sources and targets, I think it is ok in our context. Why? Thinking in terms of graphs representing programs: the order in which I apply arguments usually matters. 0/7 != 7/0.

To understand

• Here, we assume that matches are injective while the rewrite papers don't make this assumption. Uniqueness of the pushout complement depends only on K->L being mono. The match m needs no extra restriction for uniqueness but only for existence (gluing conditions).
• For all practical purposes, wouldn't it make sense to restrict to isomorphic m, i.e. embedding? No, counterexample: target f(a,a) where a is a wire connected to two ports and rule is f(x,x) with two wires with the same label.