How does confluence apply (or not) in non-terminating rewriting systems?

53 Views Asked by At

Suppose we have the rules $\{x\to Ax, x \to xB\}$. We start with letting $x$ be the empty string, and are free to apply either rule at will. This will allow us to build any string of form $A^mB^n$.

This seems to be locally confluent since applying the first rule followed by second will yield the equivalent to applying the second followed by the first; either way, after those two steps, the net result is $x\to AxB$.

Rather, this would seem to be locally confluent but for the fact that all constructions are non-terminating. My question is how situations like these are treated; I'm having a hard time tracking down anything specifically about this sort of case.

On the one hand, you could have one path which only ever uses the first rule, yielding arbitrarily many $A$s, and another which uses the second to get arbitrarily many $B$s. Depending on the sequence of rules used, there is no fixed point at which two paths must converge in a common descendant, and yet it's clear that at any finite point, any two strings constructed by these rules will have paths to a common descendant, and thus be "equal" in a meaningful way.

Is stating that every string possible in this system is equivalent in that any two can always be reduced to a single common string a fair thing to say? Are there rules or theorems about these non-terminating cases in general, or papers anyone could link me to? If someone can shed light on this type of system, or clue me into some relevant topics or resources, I will consider this answered.

(In case it's relevant, this is a simplified example I made up for this question; my actual interest in this is geared towards combinators.)

1

There are 1 best solutions below

0
On BEST ANSWER

Your system is indeed locally confluent and even generally confluent. The definitions of these concepts do not say anything about termination. As you more or less observe, for any two strings $A^ixB^j$ and $A^kxB^\ell$ the string $$A^{\max(i,k)}xB^{\max(j,\ell)}$$ is a join.

Your argumentation in the first two paragraphs shows a property even stronger than confluence, which is often called the diamond property.

If you require a system to be both confluent and terminating, then every string has a unique normal form. This seems to be the case you have in mind, but just for confluence without termination this is not the case, because derivations may not terminate.

The textbook by Book and Otto on string-rewriting systems could be good reference for further reading.