Simon Willison’s Weblog

String rewriting systems

25th September 2002

String Rewriting Systems

These notes are from the second lecture in Dr Richardson’s Formal Systems course.

Let Σ be a finite set of symbols. Σ^* is the set of all finite length strings of symbols from Σ.

Σ = {a, b}
bbaba ∈ Σ*
(0) ∈ Σ*     (0) is a zero-length-string

A Σ rewriting rule is an expression of the form α ~> β where α, β ∈ Σ^*

Examples:
aabb ~> (0)
bba ~> ab

A Σ rewriting system is a finite set of Σ rewriting rules:

    { α1 ~> β1
P = { ...
    { αn ~> βn

Definition:

For X, Y in Σ^*:

X =>P Y
If
  X = ω1 αi ω2
Then
  Y = ω1 βi ω2
Where
  αi ~> βi ∈ P
And ω1, ω2 ∈ Σ*

Example:

                   { ba ~> ab
Σ = { a, b }   P = { bb ~> b

The string “babbaba” has four possible transformations:

ba bb a ba
    ---

babbaba =>P bababba
        =>P bababa
        =>P ababab
        =>P aabab

We will end up with “aaab”, as every application of the first rule moves the bs to the right, while the second rule eliminates them. This is a terminating formal system as it can not be infinitely derived. It is also confluent, as no matter what rule you apply you will eventually end up with the same string. Finally, it is locally confluent as any two paths from the same configuration can be brought back together when the final string is reached.

Example with Semantics: Symmetries of a Square

This example has semantics as it has relevance to the real world. A square has four corners, represented thus:

1  2
4  3

We define a set of symbols:

Σ = { F, R }

F and R are transformations that can be applied to the square—Flip and Rotate. When a square is flipped, the top right corner is swapped with the bottom left corner:

1  2   F   1  4
4  3  ==>  2  3

Rotations occur as a single 90 degree clockwise transformation:

1  2   R   4  1
4  3  ==>  3  2

A string in Σ^* is a sequance of operations, applied left-to-right. For example, RFRR means “rotate, flip, rotate, rotate”.

The set of Σ rewriting rules is as follows:

    { FF ~> (0)
P = { RRRR ~> (0)
    { FR ~> RRRF

The first two rules are obvious. The third can be demonstrated by comparing the effect of the two strings. Now let’s apply the rules to the string “RFRFR” in two different ways:

         R FR FR
           /    \
          /      \
   RRRR FF R    RF RRRR F
      |             |
      R            R FF
                    |
                    R

The two divergent branches come together at the end, showing the system to be locally confluent. We can also see that the formal system is terminating—the third rule moves Fs to the right where double flips / quadruple rotations will wipe each other out.

So... every word ω ∈ Σ^* has a normal form ω =^*> RⁱF^j where i = {0, 1, 2, 3} and j = {0, 1}

We can safely claim that our system is terminating, confluent and locally confulent.

Completeness and Correctness

We will say that our system (Σ^*, P) is correct with respect to this interpretation:

If X =>*PY then X = Y as symmetry of square.

We will say that our system (Σ^*, P) is complete with respect to this interpretation:

If X = Y as symmetry of square then X =>*PY

Correctness follows from correctness of each rule in P.

The above rules reduce any word to a normal form RⁱF^j where i = {0, 1, 2, 3} and j = {0, 1}. If these rules are not complete, two (or more) of these normal forms must represent the same symmetry. We could check if this is the case by writing out the 8 possible combinations and comparing them all (64 comparisons) but a better way to check is to look at the properties of the symmatry of a square:

There are four possible places for the first corner to end up in after a transformation of a square:

1  2    ?  ?
4  3    ?  ?

After the first corner has been placed, there are only two possibilities for positions for the second corner (depending on whether or not the square has been flipped):

1  ?
?  *

Once the second corner has been placed, the rules of symmetry mean that the remaining two corners must be placed in specific places. This gives us 2 * 4 = 8 possible configurations, which demonstrates that our formal system for representing the symmetries of a square is both correct and complete.