scaling up SRSs

[H. Zantema]

On Thu, 11 Mar 2004, Claude Marche wrote:

> 
> Dear Hans,
> 
> First, apparently your subscription to the list did not work, your
> messages are rejected. I guess you don't received the messages from
> others, right ? 
Yes, I got messages from others, and I got this message twice: once directly
to my own address and once via termtools. I tried to subscribe twice, and
the second time was successful. 

> Please look at 
> 
>   http://www.lri.fr/~marche/wst2004-competition/tpdb/SRS/
> 
> there is already an example with 15 symbols: a srs representing the
> permutation group S6. I plan to add systems for S7, S8, etc, which
> will have 21, 28, etc symbols (this is why I would like to allow the
> syntax with exponents...)
> 
> I think one of the interesting issue in this competition is to see how
> tools scale up, when working on larger and larger examples.

Indeed it is interesting to see what kind of SRSs you put there. Until now
both matchbox and torpa concentrate on small SRSs: torpa typically up to 
10 or 20 rules, and matchbox mainly on single rules or at most a few. 
I applied torpa to your turing-add system, and a very simple termination
proof using only polynomials is found. I would be surprised if AProVE,
CiMe, TTT or Termptation would have problems with this example.

Scaling up to bigger systems is one possible direction, but there are
simple SRSs of only a few rules or even one rule on which all techniques 
until now fail. The same holds for term rewriting: there are applications
in which termination of hundreds of rules has to be proved, and can easily
be done by rpo. However, most examples in the Termination Problem Data Base have
only a few rules and cannot be done by rpo. I think that both for string 
rewriting and term rewriting the real challenge is not in scaling up to 
dozens or hundreds of rules, and I would not be happy with too much emphasis 
on this direction, for SRS as wel as TRS. To illustrate this by an example: 
termination of the SRS
h11 -> 1h
11hb -> 11sb
1s -> s1
bs -> bh
h1b -> t11b
1t -> t111
bt -> bh  
can be proved to be equivalent to the well-known 3n+1 problem, also
called Collatz problem or Syracuse problem, see
http://164.8.13.169/Enciklopedija/math/math/c/c433.htm
The equivalence proof is given in the full TORPA paper to be downloaded from
http://www.win.tue.nl/~hzantema/torpa.html
So apparantly one well-known big open problem in mathematics can be expressed
as a termination problem of an SRS of only 7 simple rules: why should we scale
up?

Below you find a list of 26 SRSs of one to four rules that are all terminating,
and 38 single rule SRSs that were presented by Alfons last year on WST (not all 
terminating). Could you add them to the data base?

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+

aabb -> bbbaaa

bca -> abab
b -> cc
aa -> acba

bca -> ababc
b -> cc
cd -> abca
aa -> acba

abaa -> cbaba
acb -> aabcba

acb -> baba
b -> cac
aa -> abca

ab -> ba
ba -> acb

ab -> ba
ba -> aacb

as -> sa
babs -> absa
babb -> abab
abaa -> baba

a -> bc
ab -> ba
dc -> da
ac -> ca

ab -> bba
cb -> bcc

ab -> bba
bc -> cbb
ca -> acc

a -> b
ab -> bca
b -> c
cb -> a

gc -> gfc
gfc -> gffc
gg -> gfg
ffg -> gf

ab -> baa
b -> cac
aa -> aca

ab -> baaa
ba -> aa
aa -> acb

ab -> baa
bc -> cbb
ca -> aac

ab -> baa
bc -> cb
aa -> aca

ab -> bca
bc -> cbb
ba -> acb

ab -> bca
bc -> cbb
ca -> ac

ab -> bca
bc -> cbb
ac -> cab

aab -> bbaa
ba -> acb

aab -> babca
ba -> abb
bca -> cab

aab -> bab
ba -> abb
bca -> ccaab

aba -> aabbaa
baab -> bab

ba -> ab
aaa -> baab
bbbb -> a

abb -> baa
aab -> bba

List from Alfons:

babaa -> aaababab

ababaaa -> aaaababab

babaaa -> aaaababab

babaaa -> aaabababa

bcbcaa -> aaabcbcbc

babaa -> aabbababa

babbaba -> abaabbabba

baaba -> aabbaab

aabbab -> abbaabba

baaabaa -> aaabbaaab

baababa -> aababbaab

baabba -> aabbaaabb

caabca -> aabccaabc

aabaaba -> abaabaaab

baaba -> abaabbaab

cbaba -> abababcbc

cbaa -> aabaabcbac

caba -> ababcca

cabab -> ababbabbcabca

caaba -> aabaccaab

caba -> abaacabcab

babacba -> abacbbabac

abaabb -> aababba

abbaab -> aabbaba

baabb -> aabbbaa

baaabb -> abaabba

baabab -> abaabba

baabab -> abababa

baabbb -> ababbba

bababb -> ababbba

babbab -> ababbba

bababb -> abbabba

babbbb -> abbbbba

bbabbb -> abbbbba

bbcabc -> abbcbca

bcabbc -> abcbbca

babccb -> abbccba

bacbb -> acbbbac