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

[Zantema, H.]

Here at FLOC in Seattle I presented the results of the competition at WST. In concluding I mentioned a few challeges, including aaa -> bab, bbb -> aaa.
 
As a reaction I got the following termination proof, found by Aleksey Nogin and Carl Witty. Below you find their proof, and my first remarks. The main point is that it is simple, correct and intuitive. Now our task is to polish our tools such that it can be found automatically in next year's competition.........
 
Best regards, Hans Zantema. 
 
 
 
------------------------------------------
 
Dear Claude and Hans,
In your report on Termination Competition 2006 you have mentioned that
it was not known whether the rewriting system "aaa -> bab, bbb -> aaa"
terminates. Carl Witty and I were able to come up with a termination proof.
Below is a brief outline of the proof. Please let me know if you would
like to see a more accurately written one.
Thank you,
Aleksey
-------------------------------------
Lemma 1. Each non-terminating loop will only apply "bbb -> aaa" in
context of an "a" on each side ("abbba -> aaaaa").
Proof. Consider the following metric on the input string:
- Consider all the "runs" of a's (in other words - all the non-empty
substrings of just a's that has either a b or a string boundary on each
side). For each of them, consider its length modulo 3.
   - Give 2 "points" if the length mod 3 is 1.
   - Give 1 "point", if the length mod 3 is 2.
   - Give no "points", if the length is divisible by 3.
- Also, give a "point" for each letter a in the input string.
It is easy to see that the "aaa -> bab, bbb -> aaa" RS can not decrease
this metric, so any potential non-terminating loop must keep it
constant. It is easy to see that the only way the rewrite "bbb -> aaa"
would keep it constant is when it is applied in a context where there
are 3n+1 a's on one side and 3m+2 a's on the other (for some m,n>=0) .
Hence, there must be at least on "a" on each side. QED.
Lemma 2. If there exists a non-terminating loop, there is also one where
"bbb -> aaa" is applied in the leftmost position (i.e. at the beginning
of the string).
Proof. Consider the "narrowest" possible loop - i.e. the shortest string
on which the RS would loop. Obviously, at least some rewrite in the loop
must be applied in the leftmost position (otherwise drop that position
and you'll get a narrower loop) and it is impossible to have a loop,
where only "aaa -> bab" is applied in the leftmost position (since
something needs to change the resulting "b" at the beginning of the
string back to an "a" in order for there to be a loop). QED.
Theorem. "aaa -> bab, bbb -> aaa" terminates.
Proof. Is it trivial to see that the two lemmas are in conflict with
each other - if there exists a loop, then by Lemma 2 there is also one
where "bbb -> aaa" is applied in the leftmost position, but according to
Lemma 1 a non-terminating loop can not contain an application of "bbb ->
aaa" without having at least on "a" to the left of it. QED.
 
 
---------------and here my reaction:
 
 
 
Dear Aleksey,
I considered your proof and I am convinced it is correct. Congratulations!
The counting argument can be made slightly simpler. Your weight function is always divisble by three, and if you divide it by 
3, the same argument holds. Then the weight is the number of bins needed to pack all groups of a's, with the following rules:
* every bin can contain 3 a's
* every group of a's is split up over bin's
* bins may not contain a's from different groups.
Said in other words: every group of n a's requires ceil(n/3) bins.
Now you can check that the number of bins never decreases by rewriting, and strictly increases if bbb -> aaa applies without 
a's on both sides around it. The rest of the argument can easily be given by taken a minimal size string having an infinite 
reduction.
So finally the proof can be given very short with an intuitive argument, in contrast to earlier challenges like aabb -> bbbaaa 
and  { aa -> bc, bb -> ac, cc -> ab } that have been proved to be terminating, but without such a simple intuitive argument.
Again congratulations, this is an impressive achievement!
Best regards, Hans Zantema.
 
--
Aleksey Nogin
Home Page: http://nogin.org/
E-Mail: nogin at cs.caltech.edu (office), aleksey at nogin.org (personal)
Office: Moore 04, tel: (626) 395-2200
 
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools