# Graph rewriting

## Terminology

- Normal form
- Confluent
- Terminating

## Terminating and confluent system

When a GRS is **terminating** and **confluent**, we have the equivalence of the four 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 `Onf`

strategy should be used as 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))
```

Again, prefer the more efficient `Onf`

.

See below for an example of a non-terminating system where the equivalence does not hold.

## 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 } }
}
strat iter { Iter (S) }
strat pick_iter { Pick (Iter (S)) }
strat iter_pick { Iter (Pick (S)) }
strat onf { Onf (S) }
```

Each rule replaces one edge label with another.
For example, the rule `B2A`

removes an edge with a `B`

label and adds one with an `A`

label.

Let `G_A`

, `G_B`

, `G_C`

and `G_D`

be the four graphs with two nodes and one edge labelled `A`

, `B`

, `C`

and `D`

respectively.

The schema below shows how the four rules act on these four graphs:

### Applying `S`

to `G_B`

- The strategy
`Iter (S)`

applied to`G_B`

produces the two graphs`G_A`

and`G_D`

(i.e. the two normal forms). - 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 (in practice
**Grew**tries to detect these cases and raises an error after a given number of rule applications)

- the output of the graph

In the last three cases, the output is unpredictable, but multiple executions with the same input data will give the same output.
However, if the order of the rules in the package `S`

is changed, the behaviour may be different.