## 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: Embeddings, more embeddings and Datasette Cloud - 17th September 2023
- Build an image search engine with llm-clip, chat with models with llm chat - 12th September 2023
- LLM now provides tools for working with embeddings - 4th September 2023
- Datasette 1.0a4 and 1.0a5, plus weeknotes - 30th August 2023
- Making Large Language Models work for you - 27th August 2023
- Datasette Cloud, Datasette 1.0a3, llm-mlc and more - 16th August 2023
- How I make annotated presentations - 6th August 2023
- Weeknotes: Plugins for LLM, sqlite-utils and Datasette - 5th August 2023
- Catching up on the weird world of LLMs - 3rd August 2023
- Run Llama 2 on your own Mac using LLM and Homebrew - 1st August 2023