Rewriting for Lax Hypergraphs

[mstn]

Context

Implemented the general case (non-monic match)

• Bonchi, Filippo, et al."String diagram rewrite theory I: Rewriting with Frobenius structure." Journal of the ACM (JACM) 69.2 (2022): 1-58.

Details

• I create a NodeEdgeMap which is not a graph morphism; it’s just a pair of functions on node and edge indices. It’s an intermediary, lightweight structure that doesn’t carry domain/codomain hypergraphs (to avoid cloning). The intent is to use it inside constructions that enforce the necessary compatibility, but it isn’t meant as a standalone, validated morphism.
• Rules and the morphisms of the final pushout are Span where apex is always discrete. Span components are borrowed because I wanted to avoid cloning and also because a span is just a pattern that I use with read only operations, e.g. computing pushout.
• I was planning to use the two functions for deleting that I implemented but it turned out that a more "categorical" way is possible and closer to the papers. I don't see any drawbacks in the categorical approach, but let me know.
• rewrite(g: &Hypergraph<O, A>, rule: &Span<'_, O, A>, candidate: &NodeEdgeMap) -> Vec<Hypergraph<O, A>> where candidate is the match computed by a sub-graph isomorphism algorithm and we assume that is well defined for g and rule otherwise we panic. We return all the possible rewrites, perhaps we could considering streaming or limit the number of results if state space is too big.
• Data structures for partitions and union find for representing equivalence relations. We enumerate all partitions (even if we return only those compatible with the match), perhaps we should apply some pruning.
• Built a macro for tests to simplify the construction of fixtures.