## 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^{i}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 =>^{*}_{P}Y 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 =>^{*}_{P}Y

Correctness follows from correctness of each rule in P.

The above rules reduce any word to a normal form R^{i}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.

## More recent articles

- Weeknotes: a livestream, a surprise keynote and progress on Datasette Cloud billing - 2nd July 2024
- Open challenges for AI engineering - 27th June 2024
- Building search-based RAG using Claude, Datasette and Val Town - 21st June 2024
- Weeknotes: Datasette Studio and a whole lot of blogging - 19th June 2024
- Language models on the command-line - 17th June 2024
- A homepage redesign for my blog's 22nd birthday - 12th June 2024
- Thoughts on the WWDC 2024 keynote on Apple Intelligence - 10th June 2024
- Accidental prompt injection against RAG applications - 6th June 2024
- Training is not the same as chatting: ChatGPT and other LLMs don't remember everything you say - 29th May 2024
- Weeknotes: PyCon US 2024 - 28th May 2024