Rewrite Systems
Chapter Forty-Six
Syllabus topic Module 1, "Rewrite systems"
Pages 150 to 153 of 378
In one line
A rewrite system is a set of rules that replace one piece of a string with another, applied over and over until nothing applies.
In the wording you can write in an examination: a string rewriting system, also called a semi-Thue system, is a finite alphabet together with a finite set of rules each of which replaces one string by another. A string to which no rule applies is in normal form. The system terminates if every string reaches a normal form after finitely many steps, and it is confluent if whenever two different sequences of rewrites are possible from one string, they can be continued so as to reach the same string.
The vocabulary
A rule. A pair of strings, written left rewrites to right. Unlike a grammar production, neither side has to contain a special category symbol: a rewrite system works on plain strings.
A step. Find an occurrence of some rule's left side in the string, and replace it by that rule's right side.
Normal form. A string with no occurrence of any rule's left side. The computation is over.
Termination. Every string reaches a normal form. Not guaranteed: a rule set can loop.
Confluence. If two different steps are possible, the two results can be brought back together. Where it holds, the normal form does not depend on which step you took.
Convergence. Terminating and confluent together. A convergent system gives every string exactly one normal form, which is the property you want if the system is meant to compute a function.
Both properties, demonstrated
RULES = [("ab", "ba"), ("ba", "ab")]
def step(s, rules):
for i in range(len(s)):
for left, right in rules:
if s.startswith(left, i):
return s[:i] + right + s[i + len(left):], (left, right, i)
return None, None
def normalise(s, rules, limit=8):
trail = [s]
for _ in range(limit):
nxt, used = step(s, rules)
if nxt is None:
return trail, "normal form reached"
s = nxt
trail.append(s)
return trail, "gave up after %d steps: this rule set does not terminate" % limit
print("rule set A: ab -> ba and ba -> ab")
trail, why = normalise("ab", RULES)
print(" " + " -> ".join(trail))
print(" " + why)
print()
SORTER = [("ba", "ab")]
print("rule set B: ba -> ab only")
for start in ("ba", "bba", "bab", "bbaa", "abab"):
trail, why = normalise(start, SORTER, limit=12)
print(" %-6s %-34s %s" % (start, " -> ".join(trail), why))rule set A: ab -> ba and ba -> ab
ab -> ba -> ab -> ba -> ab -> ba -> ab -> ba -> ab
gave up after 8 steps: this rule set does not terminate
rule set B: ba -> ab only
ba ba -> ab normal form reached
bba bba -> bab -> abb normal form reached
bab bab -> abb normal form reached
bbaa bbaa -> baba -> abba -> abab -> aabb normal form reached
abab abab -> aabb normal form reachedRewrite Systems
Reading the two rule sets
Rule set A does not terminate, and the reason is visible in the trail: the two rules undo each other. A rewrite system can loop, and nothing in the notation prevents it.
Rule set B terminates, and it sorts. Every normal form has its a's before its b's. The termination argument is a good one to know: each application of the rule moves one a one place to the left, and the total of the positions of the a's is a whole number that strictly decreases and cannot go below zero. Exhibiting a quantity that strictly decreases is how termination is proved.
Rule set B is also confluent. Whatever order the rewrites are done in, the result is the same string: all the a's, then all the b's. So it is convergent, and it computes a function.
The Aṣṭādhyāyī as a rewrite system
This is the positive characterisation [Context-Free Grammar, and Whether Pāṇini Wrote One] promised.
The strings are forms under derivation. A root plus affixes, with markers.
The rules are the vidhi rules. Each replaces one element by another in a stated context.
A normal form is a finished word. No further rule applies.
And there is a strategy. This is the part that makes it different from rule set B above, and it is the important part.
Why a strategy changes everything
Rule set B is confluent, so it needs no strategy: any order gives the same answer. Most interesting rewrite systems are not confluent, and then the order decides the result.
Pāṇini's system is not confluent. Two rules can apply and give different words, and only one of them is Sanskrit. So a strategy is not an optimisation; it is part of the specification.
The strategy is the precedence order. Apavāda, nitya, antaraṅga, paratva, as [Rule Precedence: The Four Principles] sets out, with prohibitions and asiddhatva outside the queue.
A rewrite system plus a deterministic strategy computes a function. Given a root and a meaning, exactly one sequence of rewrites is licensed, so exactly one form results. That is what the grammar is for, and it is why the tradition invested so heavily in the precedence rules rather than in making the rules non-overlapping.
| A convergent rewrite system | The Aṣṭādhyāyī | |
|---|---|---|
| Confluent | yes, by assumption | no |
| Needs a strategy | no | yes, and the strategy is stated |
| What the strategy is for | efficiency, at most | correctness |
| Result if the strategy is ignored | the same normal form | a different form, which is not Sanskrit |
| Termination | must be proved | assumed by the tradition, and not proved |
Rewrite Systems
Termination, and the honest gap
The last row is a real gap and it should be stated.
Nothing in the tradition proves the grammar terminates. No argument is offered that a derivation cannot loop. The evidence is that derivations in practice finish, which is the same evidence rule set A appeared to have until somebody tried "ab".
The asiddhatva mechanism helps. By making phase two invisible to phase one, 8.2.1 prevents a class of loops in which a phase-one rule keeps re-firing because a phase-two rule keeps undoing its work. That is a structural reason to expect termination, and it is the nearest thing to an argument the system provides.
But it is not a proof, and a chapter that claimed otherwise would be overstating. What can be said is that the mechanism exists and that it forecloses the obvious failure mode.
What a rewrite system is NOT
It is not a grammar in the Chomsky sense. It has no start symbol and no non-terminals, and it need not define a set of strings. A grammar generates; a rewrite system transforms.
It is not deterministic by itself. Which occurrence of which rule to rewrite is a choice, and the notation does not make it.
It is not guaranteed to do anything. Termination and confluence are properties to be established, not features of the notation.
Quick revision
- A string rewriting system is an alphabet plus rules replacing one string by another. A step applies one rule at one occurrence.
- Normal form: no rule applies. Termination: every string reaches one. Confluence: different orders can be brought back together. Convergent: both.
- Rule set A, ab to ba and ba to ab, loops. Rule set B, ba to ab only, terminates and sorts, and the termination proof exhibits a strictly decreasing quantity.
- The Aṣṭādhyāyī is a rewrite system over forms, and it is NOT confluent, so its strategy is part of its correctness and not an optimisation.
- The strategy is the four precedence principles, with prohibition and asiddhatva outside the queue.
- Termination is not proved by the tradition. Asiddhatva forecloses the obvious loop and is not a proof.
Test yourself
1. Define normal form, termination and confluence.
A normal form is a string to which no rule applies. A system terminates if every string reaches a normal form in finitely many steps. It is confluent if whenever two different rewrites are possible from a string, the two results can be continued to a common string.
2. Prove that the rule "ba rewrites to ab" terminates.
Each application moves one a one position to the left, so the sum of the positions of the a's strictly decreases with every step. It is a non-negative whole number, so it cannot decrease for ever, and the system must halt.
Rewrite Systems
3. Why is Pāṇini's strategy part of his specification rather than an optimisation?
Because his rule set is not confluent: two applicable rules can yield different forms and only one is correct. So the order of application determines the answer, and the precedence principles are what fix the answer.
4. What does asiddhatva contribute to termination, and what does it not?
By making the later phase invisible to the earlier one, it prevents a loop in which an earlier rule re-fires because a later rule keeps undoing its work. It does not amount to a proof that no derivation loops, and the tradition offers none.
The rest of this subject
These notes are cut from the University's printed syllabus. Open the syllabus itself for the same subject.