# 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 to`G_B`

produces the 2 graphs`G_A`

and`G_D`

. - The strategy
`Pick (Iter (S))`

applied to`G_B`

may produce (unpredictably):- the graph
`G_A`

- the graph
`G_D`

- the graph
- The strategy
`Iter (Pick (S))`

applied to`G_B`

may produce (unpredictably):- the graph
`G_A`

- the graph
`G_D`

- the empty set

- the graph
- The strategy
`Onf (S)`

applied to`G_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.