In the single-pushout approach to graph rewriting, many nodes in a pattern graph can be matched to a single node of a target graph.
My question is if there is a notion of graph rewriting where the inverse is true: that a single node in the pattern graph can match to many nodes of the target graph. For example, the pattern graph $A \rightarrow B$ should be able to match a subgraph isomorphic to $X \rightarrow Y \leftarrow Z$, with the mapping $A \mapsto \{ X, Z \}, B \mapsto \{Y$}. I'm especially interested in a definition where $A \mapsto \{X\}, B \mapsto \{ Y\}$ would not be a valid match for any graph that contains $X \rightarrow Y \leftarrow Z$ as a subgraph.
As an example application, consider the problem of for-loop desugaring. This for-loop:
for (int i = 0; i < n; i++) {
if ( i % 3 == 0) {
printf("Divisible by 3\n");
continue;
}
printf("%d\n", i);
}
desugars to:
int i = 0;
while (i < n) {
if (i % 3 == 0) {
printf("Divisible by 3\n");
i++;
continue;
}
printf("%d\n", i);
i++;
}
A key part of this desugaring -- that the "step" part of the for loop be inserted at the end of the loop and before every "continue" statement -- is most easily expressed as a rewrite on the control-flow graph, where that statement is inserted before every predecessor of the condition (except for before the loop runs).