## 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

- Three major LLM releases in 24 hours (plus weeknotes) - 10th April 2024
- Building files-to-prompt entirely using Claude 3 Opus - 8th April 2024
- Running OCR against PDFs and images directly in your browser - 30th March 2024
- llm cmd undo last git commit - a new plugin for LLM - 26th March 2024
- Building and testing C extensions for SQLite with ChatGPT Code Interpreter - 23rd March 2024
- Claude and ChatGPT for ad-hoc sidequests - 22nd March 2024
- Weeknotes: the aftermath of NICAR - 16th March 2024
- The GPT-4 barrier has finally been broken - 8th March 2024
- Prompt injection and jailbreaking are not the same thing - 5th March 2024
- Interesting ideas in Observable Framework - 3rd March 2024