[Termtools] DP solution of aaa -> bab, bbb -> aaa

[Zantema, H.]

Dear colleagues,

Last night I succeeded in polishing the proof of Aleksey and Carl towards a more standard setting, only using an unusual weakly monotone interpretation in the natural numbers.
 
As a first step we do reversal. Not the usual reversal (by this symmetrical system the reversal is itself), but reversing l -> 
r to r -> l. For length preserving string rewriting systems (also term rewriting systems) this is well-known to be correct.
In my JAR paper "Termination of String Rewriting Proved Automatically" this is Lemma 3.
So we have to prove termination of the rules bab -> aaa, aaa -> bbb. We apply the dependency pair method, yielding the 
dependency pairs Bab -> Aaa and Aaa -> Bbb and a few length decreasing dependency pairs. By choosing the interpretation in which all symbols are interpreted by the successor (so essentially considering the length of strings) these length decreasing DPs are removed. 
 
Next we choose the following weakly monotone interpretation:
[A](x) = [a](x) = x+1
[B](x) = [b](x) = 3 * ceil(x/3)
So [B] and [b] means: round upwards towards a multiple of 3.
We easily check
[bab](x) = [Bab](x) = [b](x) + 3 >= x + 3 = [aaa](x) = [Aaa](x)
and
[aaa](x) = [Aaa](x) = x + 3 > [b](x) = [bbb](x) = [Bbb](x)
so the DP Aaa -> Bbb can be removed.
Now the remaining DP Bab -> Aaa is easily removed by counting B's.
Since no DP remains we have proved termination.

----------------
Some remarks about this proof.

Reversal causes that values go down instead of go up as in the original proof, which is more convenient for a proof based on 
interpretations.
The combination of DP and weakly (not strictly) monotone interpretations takes over the minimaility argument in the original 
proof.
Since all interpretations satisfy [.](x+3) = [.](x) + 3 and the system is length preserving, for the interpretations it 
suffices to check only for the values 0, 1 and 2. So
[bab](0) = 3 = [aaa](0)
[bab](1) = 6 > 4 = [aaa](1)
[bab](2) = 6 > 5 = [aaa](2)
[aaa](0) = 3 > 0 = [bbb](0)
[aaa](1) = 4 > 3 = [bbb](1)
[aaa](2) = 5 > 3 = [bbb](2)
So this proof generalizes to an easily automatable proof method for length preserving SRSs:
* apart from normal reversal, also try this kind of reversal
* in the DP setting apart from normal polynomials also try weakly monotonic functions satisfying [.](x+n) = [.](x) + n
for small values of n (2,3,4,..), and check requirements for the values 0,1,..,n-1
 
It is not clear whether it pays off, i.e., applies to more systems than only this one. Could Z086 be done by this method too?
In any case the class of length preserving SRSs is quite restricted.
 
Best regards, Hans Zantema.

 
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools