Graph rewriting
Terminology
- Normal form
- Confluent
- Terminating
Terminating and confluent system
When a GRS is terminating and confluent, we have the equivalence of the 4 strategies:
Onf (S) ≃ Iter(S) ≃ Pick (Iter (S)) ≃ Iter (Pick (S))
They all compute one graph which is the unique normal form.
In this case, the strategy Onf
should be used because it is the more efficient one.
Terminating system
When a GRS is terminating, we have the equivalence of the two strategies:
Onf (S) ≃ Pick (Iter (S))
See below for an example of non-terminating system where the equivalence does not hold.
Again, prefer the more efficient Onf
.
Example of non-terminating rewriting system
The following code described a non-terminating rewriting system:
package S {
rule B2A { pattern { e: N -[B]-> M } commands { del_edge e; add_edge N -[A]-> M } }
rule B2C { pattern { e: N -[B]-> M } commands { del_edge e; add_edge N -[C]-> M } }
rule C2B { pattern { e: N -[C]-> M } commands { del_edge e; add_edge N -[B]-> M } }
rule C2D { pattern { e: N -[C]-> M } commands { del_edge e; add_edge N -[D]-> M } }
}
Each rule replaces an edge label by another.
For instance, the rule B2A
removes and edge with an B
label and adds one with an A
label.
Let G_A
, G_B
, G_C
and G_D
the 4 graphs with 2 nodes and 1 edge labelled A
, B
, C
and D
respectively.
The schema below shows how the 4 rules act on these 4 graphs:
Applying S
to G_B
- The strategy
Iter (S)
applied toG_B
produces the 2 graphsG_A
andG_D
. - The strategy
Pick (Iter (S))
applied toG_B
may produce (unpredictably):- the graph
G_A
- the graph
G_D
- the graph
- The strategy
Iter (Pick (S))
applied toG_B
may produce (unpredictably):- the graph
G_A
- the graph
G_D
- the empty set
- the graph
- The strategy
Onf (S)
applied toG_B
may lead to (unpredictably):- the output of the graph
G_A
- the output of the graph
G_D
- a non-terminating execution
- the output of the graph
For the last three case, the output is unpredictable, but several execution with the same input data will give the same output.
But, if the order of rules in the package S
is changed, the behaviour may be different.