Rewriting with "universal quantification" in patterns

[kris-brown]

Often we want to say things like "match all incoming edges (and their sources) to a vertex" and other things that cannot be expressed as a single homomorphism from a single C-Set. There are a couple ideas for how to address this:

1.) An ad hoc (but straightforward) solution is to represent a pattern L as a map L --> U where U is the universally-quantified part. This can be interpreted as a multispan with L as the apex and multiple copies of U for the legs that we will take the colimit of. (For n=0 it's just L, n=1 it's just U, n=2 as the pushout of L with two U's, etc.) We can interpret these rules as dynamically considering at runtime what is the highest n for which a match exists, or perhaps other constraints (e.g. max(n) such that n > 3 and n < 9) are part of the rule definition. This is straightforward because the rewriting is still done with vanilla rewriting of C-Sets, with just the pattern determined at runtime.

2.) "Graph Rewriting in Span-Categories" (2010, Löwe) represents a pattern as E -> U -> L (existentially quantified, universally quantified, and the overall pattern) and represents matches as spans G <- X -> L satisfying a certain property. Rewrites are computed using final pullback complements.

3.) "A relation-algebraic approach to graph structure transformation" (2001, Kahl) has another approach that tries to address a similar problem.

[kris-brown]

This is now addressed with PBPO+ rewriting support