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

[Zantema, H.]

-----Original Message-----
From: Johannes Waldmann [mailto:waldmann at imn.htwk-leipzig.de] 


piece-wise linear functions. there should be a way to automatize that.
(and it's not specific to length-preserving systems.)
-- 

Indeed, I did some first attempts in TORPA.

It turns out that the reversal trick is not essential: for the original
system TORPA yields

TORPA test version is applied to
a a a  -> b a b ,
b b b  -> a a a ,
[G] Dependency pair transformation:
  a a a  ->= b a b 
  b b b  ->= a a a 
  A a a  -> B a b 
  A a a  -> A b 
  A a a  -> B 
  B b b  -> A a a 
  B b b  -> A a 
  B b b  -> A 
[A] Choose polynomial interpretation   a b A B: lambda x.x+1
remove: A a a  -> A b 
remove: A a a  -> B 
remove: B b b  -> A a 
remove: B b b  -> A 
Choose weakly monotone interpretation:
a: lambda x.x+2
b: lambda x.3*(x div 3)+3
A: lambda x.x+2
B: lambda x.3*(x div 3)+2
remove: A a a  -> B a b 
[A] Choose polynomial interpretation   B: lambda x.x+1,  rest identity
remove: B b b  -> A a a 
Relatively terminating since no strict rules remain.


It also works for non-length-preserving variants for which other periods
than 3 are required:

TORPA test version is applied to
b b b  -> a a a a a ,
a a a a a  -> b a a b ,
[G] Dependency pair transformation:
  b b b  ->= a a a a a 
  a a a a a  ->= b a a b 
  B b b  -> A a a a a 
  B b b  -> A a a a 
  B b b  -> A a a 
  B b b  -> A a 
  B b b  -> A 
  A a a a a  -> B a a b 
  A a a a a  -> A a b 
  A a a a a  -> A b 
  A a a a a  -> B 
Choose weakly monotone interpretation:
b: lambda x.5*(x div 5)+5
a: lambda x.x+2
B: lambda x.5*(x div 5)+2
A: lambda x.5*(x div 5)+2
remove: B b b  -> A a a 
remove: B b b  -> A a 
remove: B b b  -> A 
remove: A a a a a  -> B 
Choose weakly monotone interpretation:
b: lambda x.5*(x div 5)+5
a: lambda x.x+2
B: lambda x.5*(x div 5)+2
A: lambda x.x+0
remove: B b b  -> A a a a 
remove: A a a a a  -> B a a b 
remove: A a a a a  -> A a b 
remove: A a a a a  -> A b 
[A] Choose polynomial interpretation   B: lambda x.x+1,  rest identity
remove: B b b  -> A a a a a 
Relatively terminating since no strict rules remain.



An important observation is that for all interpretation functions and
their compositions it holds that f(x+n) = f(x)+n for all x, where n is
the period (in these examples 3 and 5). Hence for checking [l](x) >= / >
[r](x)  for all x it suffices to check this for x = 0,1,..,n-1.

Best regards, Hans Zantema.
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools