[Termination tools] Re: scaling up SRSs
Claude Marche
Claude.Marche at lri.fr
Thu Mar 11 15:32:57 CET 2004
>>>>> "Hans" == H Zantema <hzantema at win.tue.nl> writes:
Hans> 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 ?
Hans> Yes, I got messages from others, and I got this message twice: once directly
Hans> to my own address and once via termtools. I tried to subscribe twice, and
Hans> the second time was successful.
Apparently you where receiving the messages sent to the list, but your
own messages where rejected. I hope it is OK
>> 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.
Hans> Indeed it is interesting to see what kind of SRSs you put there. Until now
Hans> both matchbox and torpa concentrate on small SRSs: torpa typically up to
Hans> 10 or 20 rules, and matchbox mainly on single rules or at most a few.
Hans> I applied torpa to your turing-add system, and a very simple termination
Hans> proof using only polynomials is found. I would be surprised if AProVE,
Hans> CiMe, TTT or Termptation would have problems with this example.
What about the turing_mult ?
Hans> Scaling up to bigger systems is one possible direction, but there are
Hans> simple SRSs of only a few rules or even one rule on which all techniques
Hans> until now fail. The same holds for term rewriting: there are applications
Hans> in which termination of hundreds of rules has to be proved, and can easily
Hans> be done by rpo. However, most examples in the Termination Problem Data Base have
Hans> only a few rules and cannot be done by rpo. I think that both for string
Hans> rewriting and term rewriting the real challenge is not in scaling up to
Hans> dozens or hundreds of rules, and I would not be happy with too much emphasis
Hans> on this direction, for SRS as wel as TRS. To illustrate this by an example:
Hans> termination of the SRS
Hans> h11 -> 1h
Hans> 11hb -> 11sb
Hans> 1s -> s1
Hans> bs -> bh
Hans> h1b -> t11b
Hans> 1t -> t111
Hans> bt -> bh
Hans> can be proved to be equivalent to the well-known 3n+1 problem, also
Hans> called Collatz problem or Syracuse problem, see
Hans> http://164.8.13.169/Enciklopedija/math/math/c/c433.htm
Hans> The equivalence proof is given in the full TORPA paper to be downloaded from
Hans> http://www.win.tue.nl/~hzantema/torpa.html
Hans> So apparantly one well-known big open problem in mathematics can be expressed
Hans> as a termination problem of an SRS of only 7 simple rules: why should we scale
Hans> up?
Interesting point of view: more or less you say that we should not try to prove
termination of systems with $n$ rules before having solved all systems
with $n+1$ rules...
My point of view is that there are more and more practical
applications of automated termination techniques, for example I am
currently working on how one may prove termination of OBJ or Maude
programs. For such applications, systems are not tricky as the syracuse
problem, but they may have hundreds, thousands of rules.
So, as I said, scaling up is ONE OF the interesting issues.
Of course, I will add your srs encoding the syracuse problem in the
tpdb !
Hans> Below you find a list of 26 SRSs of one to four rules that are all terminating,
Hans> and 38 single rule SRSs that were presented by Alfons last year on WST (not all
Hans> terminating). Could you add them to the data base?
Yes, of course, new examples are always welcome
Hans> Best regards, Hans Zantema.
Hans> +--------------------------------------+-----------------------------+
Hans> | | |
Hans> | Dr Hans Zantema | Hoofdgebouw kamer 6.73 |
Hans> | Faculteit Wiskunde en Informatica | tel (040)2472749 |
Hans> | Technische Universiteit Eindhoven | fax (040)2468508 |
Hans> | Postbus 513 5600 MB Eindhoven | e-mail H.Zantema at tue.nl |
Hans> | The Netherlands | www.win.tue.nl/~hzantema |
Hans> | | |
Hans> +--------------------------------------+-----------------------------+
Hans> aabb -> bbbaaa
Hans> bca -> abab
Hans> b -> cc
Hans> aa -> acba
Hans> bca -> ababc
Hans> b -> cc
Hans> cd -> abca
Hans> aa -> acba
Hans> abaa -> cbaba
Hans> acb -> aabcba
Hans> acb -> baba
Hans> b -> cac
Hans> aa -> abca
Hans> ab -> ba
Hans> ba -> acb
Hans> ab -> ba
Hans> ba -> aacb
Hans> as -> sa
Hans> babs -> absa
Hans> babb -> abab
Hans> abaa -> baba
Hans> a -> bc
Hans> ab -> ba
Hans> dc -> da
Hans> ac -> ca
Hans> ab -> bba
Hans> cb -> bcc
Hans> ab -> bba
Hans> bc -> cbb
Hans> ca -> acc
Hans> a -> b
Hans> ab -> bca
Hans> b -> c
Hans> cb -> a
Hans> gc -> gfc
Hans> gfc -> gffc
Hans> gg -> gfg
Hans> ffg -> gf
Hans> ab -> baa
Hans> b -> cac
Hans> aa -> aca
Hans> ab -> baaa
Hans> ba -> aa
Hans> aa -> acb
Hans> ab -> baa
Hans> bc -> cbb
Hans> ca -> aac
Hans> ab -> baa
Hans> bc -> cb
Hans> aa -> aca
Hans> ab -> bca
Hans> bc -> cbb
Hans> ba -> acb
Hans> ab -> bca
Hans> bc -> cbb
Hans> ca -> ac
Hans> ab -> bca
Hans> bc -> cbb
Hans> ac -> cab
Hans> aab -> bbaa
Hans> ba -> acb
Hans> aab -> babca
Hans> ba -> abb
Hans> bca -> cab
Hans> aab -> bab
Hans> ba -> abb
Hans> bca -> ccaab
Hans> aba -> aabbaa
Hans> baab -> bab
Hans> ba -> ab
Hans> aaa -> baab
Hans> bbbb -> a
Hans> abb -> baa
Hans> aab -> bba
Hans> List from Alfons:
Hans> babaa -> aaababab
Hans> ababaaa -> aaaababab
Hans> babaaa -> aaaababab
Hans> babaaa -> aaabababa
Hans> bcbcaa -> aaabcbcbc
Hans> babaa -> aabbababa
Hans> babbaba -> abaabbabba
Hans> baaba -> aabbaab
Hans> aabbab -> abbaabba
Hans> baaabaa -> aaabbaaab
Hans> baababa -> aababbaab
Hans> baabba -> aabbaaabb
Hans> caabca -> aabccaabc
Hans> aabaaba -> abaabaaab
Hans> baaba -> abaabbaab
Hans> cbaba -> abababcbc
Hans> cbaa -> aabaabcbac
Hans> caba -> ababcca
Hans> cabab -> ababbabbcabca
Hans> caaba -> aabaccaab
Hans> caba -> abaacabcab
Hans> babacba -> abacbbabac
Hans> abaabb -> aababba
Hans> abbaab -> aabbaba
Hans> baabb -> aabbbaa
Hans> baaabb -> abaabba
Hans> baabab -> abaabba
Hans> baabab -> abababa
Hans> baabbb -> ababbba
Hans> bababb -> ababbba
Hans> babbab -> ababbba
Hans> bababb -> abbabba
Hans> babbbb -> abbbbba
Hans> bbabbb -> abbbbba
Hans> bbcabc -> abbcbca
Hans> bcabbc -> abcbbca
Hans> babccb -> abbccba
Hans> bacbb -> acbbbac
--
| Claude Marché | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490 | http://www.lri.fr/~marche/ |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85 |
| F-91405 ORSAY Cedex | faxto: +33 1 69 15 65 86 |
More information about the Termtools
mailing list