Showing a property for a set of rewriting rules

Question

Let $\to$ be a relation over the set of binary strings of 0 and 1. $\to$ is defined by the following rules:

R1. $x10y \to x0001y $

R2. $x01y \to x1y $

R3. $x11y \to x0000y $

R4. $x00y \to x0y$

Where $x,y$ are arbitrary strings. The relation is interpreted as a rewriting system, mapping strings to stirings.

The exercise I am trying to solve ask for a function $f$ mapping strings of 0 and 1 into naturals such that $ x \to y $ implies $f (x) > f(y)$.

If the rewriting system would not have rules R1 and R3 one could simply take the lenght of the input string as the function f.

However it seems hard to find a function that yields the required inequality considering also the rules R1 and R4 that amplify the initial string.

Anyone happens to see such a function?

Edit: After the comment of Peter I would be interested in knowing if there is any easy way to prove that the rewriting system is locally confluent. That is, if a -> b and a -> c then b ⇝ d and c ⇝ d

Answer 1

Here maybe an answer that doesn't really give any more insight to the problem, but as I see it, I is only suppose to show, that there are only finitely many possibilities to rewrite a string.

Taking a string wie will assign a natural number to each digit and the value of the string will be the sum of the assigned natural numbers. We will first count the number of 1's to the left of that digit, say the number is $n$, and then assign $4^n$ to the digit.

Let us now prove that $x\to y$ indeed implies $f(x)>f(y)$. For this we will consider $x10y$ and so on, hence let $x$ include $n$ 1's. Then $$ f(x10y) - f(x0001y) = 4^{n+1} - 3\cdot 4^n = 4^n,$$ $$ f(x11y) - f(x0000y) = 4^n + 4^{n+1} - 4\cdot 4^n = 4^n,$$ $$ f(x01y) - f(x1y) = 4^n,$$ $$ f(x00y) - f(x0y) = 4^n.$$

My answer seems to have a strong similarity to the one given by quanta, but is carried out more explicitely.

Answer 2

Too long for a comment. Community wiki since it doesn't really answer the original question.

Here is a way to view string rewriting systems. The rules define a relation on the set of strings. I usually write a→b if one can get from a to b by applying one of the rules and a⇝b if one can get from a to b by applying a bunch of rules in succession (so ⇝ is the reflexive, transitive closure of →).

For example, 10 → 0001 → 01 → 1 first using R1 with x and y empty, next using R4 with x empty and y=01, and finally using R2 with x and y empty. Once we are comfortable using the rules, we would just write 10 ⇝ 1.

Notice that we must be "done" since none of the four rules can apply to just "1". We call a string a final form if no rule applies to it. Group theorists like final forms, and so we want our rewriting systems to at least have the property that every string has a final form, that is, for every string a, there is a final form b, such that a⇝b. More practically though we want to know that no matter how we choose to apply the rules, we always end up at a final form. Stated more negatively: there is no infinite sequence of words a1→a2→a3→…. Such a system is called locally noetherian or terminating. Actual group theorists are very demanding. They don't want a string to have more than one final form. More positively, if a,b,c are strings such that a⇝b and a⇝c, then there must be a string d such that b⇝d and c⇝d. In other words, if I go to b and you go to c, we are not lost, we can both meet at d. Such a system is called confluent. In a confluent system, a string has at most one final form. In a locally noetherian system, a string has at least one final form. Hence group theorists demand a locally noetherian confluent system so that every string has a unique final form.

How does one check the noetherian condition? This can be really tricky. You could have infinite loops, or you could have infinitely growing strings. I believe in general this is a very hard and open area of computer science. One great way to do this is to show that the rules "make things simpler." If the "complexity" of strings can be quantified by f as natural numbers, and if rules decrease the complexity (as measured by f), then of course every sequence of rules must stop: if f(a) = 37, then you cannot apply more than 37 rules for sure!

Group theorists use a slightly more general (I think) crutch. Instead of assigning each string a number, we just compare to strings and decide which one is simpler. We call ≺ a reduction ordering if (1) ≺ is a total order on the set of strings, (2) a ≺ b implies xay ≺ xby for all strings a,b,x,y, and (3) there is no infinite descending sequence of strings a1 ≻ a2 ≻ a3 ≻ a4 ≻ ….

If every rule xLy → xRy satisfies L ≻ R, then the rewriting system is terminating. Additionally, under these hypotheses to check confluence under these hypotheses is a little easier: instead of checking all a⇝b and a⇝c, one need only check all a→b and a→c, still only searching for a d such that b⇝d and c⇝d.

A rewriting system is reduced if the right hand sides of the rules are all final forms.

If a⇝b then there is some sense in which a and b are equivalent. We can define an equivalence relation ↭ as the symmetric, transitive closure of ⇝. In other words, a↭b means there is a sequence of strings a1, a2, …, an such that a1⇝a2, a3⇝a2, a3⇝a4, … an⇝b, so that by some sort of back-and-forth application of rules we can get from a to b. If a system is confluent and terminating, then each word is ↭equivalent to exactly one final form.

This gives us a way to go from terminating, confluent rewriting systems to equivalence relations with distinguished representatives. Notice that if the system is terminating and confluent, then replacing the right hand sides by their final forms does not affect the equivalence relation.

If we have a reduction ordering ≺, then the final form of a string is the unique smallest member of the ↭ equivalence class containing that string. This lets us go from an equivalence relation with distinguished representative (using ≺) back to a reduced, terminating, confluent rewriting system: The left hand sides are all strings that are not final forms but such that every proper substring is a final form, and the right hand sides are the final form. The result system is reduced, terminating (using ≺), and confluent (using the equivalence relation).

A standard use case is for finitely presented groups. The relations are turned into rules, but in group theory one is allowed to use the rules in either order. This is not good for algorithms, and so one looks for equivalent relations such that rules define a terminating confluent (and hopefully reduced) rewriting system. The type of ordering suggested in the answers here is used for extensions of groups given by rewriting systems. One has a group G with normal subgroup N such that both N and G/N are given by rewriting systems with reduction orderings ≺. One wants a reduction ordering on G that plays well with the reduction orderings on N and G/N. This is called the wreath product ordering. Basically you sort the quotient part first by ignoring the normal subgroup completely. If the two strings are the same, then one compares the intervening normal subgroup parts lexicographically (from the right in our example) using ≺ for N to compare corresponding terms.

In the original question, the "1" corresponds to the quotient group. We define a ≺ b if b has strictly more 1s than a does. If they have the same number of 1s, then look at the sequence of intervening runs of 0s. Compare the two strings right to left. Then a ≺ b if, in the first position where the runs are different lengths, the run in a is smaller than the run in b. If all the runs are the same length, then by definition the two strings are the same. Since the orderings on the strings of 1s (counting) and the ordering on the strings of 0s (counting) are both reduction orderings, this construction (their wreath product) is also a reduction ordering. Hence the system is terminating.

Note that a system might have the property that it is not terminating, while its reduction is terminating. In group theory this doesn't matter, since they determine the same equivalence relation and we want the terminating version.