We consider the system process.

  Alphabet:

    !plus : [proc * proc] --> proc 
    !times : [proc * proc] --> proc 
    delta : [] --> proc 
    sigma : [data -> proc] --> proc 

  Rules:

    !plus(x, x) => x 
    !times(!plus(x, y), z) => !plus(!times(x, z), !times(y, z)) 
    !times(!times(x, y), z) => !times(x, !times(y, z)) 
    !plus(x, delta) => x 
    !times(delta, x) => delta 
    sigma(/\x.y) => y 
    !plus(sigma(/\x.f x), f y) => sigma(/\z.f z) 
    sigma(/\x.!plus(f x, g x)) => !plus(sigma(/\y.f y), sigma(/\z.g z)) 
    !times(sigma(/\x.f x), y) => sigma(/\z.!times(f z, y)) 

Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term.

We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0).  This leads to the following AFSM:

  Alphabet:

    !plus : [proc * proc] --> proc 
    !times : [proc * proc] --> proc 
    delta : [] --> proc 
    sigma : [data -> proc] --> proc 
    ~AP1 : [data -> proc * data] --> proc 

  Rules:

    !plus(X, X) => X 
    !times(!plus(X, Y), Z) => !plus(!times(X, Z), !times(Y, Z)) 
    !times(!times(X, Y), Z) => !times(X, !times(Y, Z)) 
    !plus(X, delta) => X 
    !times(delta, X) => delta 
    sigma(/\x.X) => X 
    !plus(sigma(/\x.~AP1(F, x)), ~AP1(F, X)) => sigma(/\y.~AP1(F, y)) 
    sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) => !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
    !times(sigma(/\x.~AP1(F, x)), X) => sigma(/\y.!times(~AP1(F, y), X)) 
    ~AP1(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  !plus(X, X) >? X 
  !times(!plus(X, Y), Z) >? !plus(!times(X, Z), !times(Y, Z)) 
  !times(!times(X, Y), Z) >? !times(X, !times(Y, Z)) 
  !plus(X, delta) >? X 
  !times(delta, X) >? delta 
  sigma(/\x.X) >? X 
  !plus(sigma(/\x.~AP1(F, x)), ~AP1(F, X)) >? sigma(/\y.~AP1(F, y)) 
  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
  !times(sigma(/\x.~AP1(F, x)), X) >? sigma(/\y.!times(~AP1(F, y), X)) 
  ~AP1(F, X) >? F X 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.1 + y1 + 2y0 
  !times = \y0y1.y0 + y1 + 2y0y1 
  delta = 0 
  sigma = \G0.G0(0) 
  ~AP1 = \G0y1.y1 + 2G0(y1) 

Using this interpretation, the requirements translate to:

  [[!plus(_x0, _x0)]] = 1 + 3x0 > x0 = [[_x0]] 
  [[!times(!plus(_x0, _x1), _x2)]] = 1 + x1 + 2x0 + 2x1x2 + 3x2 + 4x0x2 >= 1 + x1 + 2x0 + 2x1x2 + 3x2 + 4x0x2 = [[!plus(!times(_x0, _x2), !times(_x1, _x2))]] 
  [[!times(!times(_x0, _x1), _x2)]] = x0 + x1 + x2 + 2x0x1 + 2x0x2 + 2x1x2 + 4x0x1x2 >= x0 + x1 + x2 + 2x0x1 + 2x0x2 + 2x1x2 + 4x0x1x2 = [[!times(_x0, !times(_x1, _x2))]] 
  [[!plus(_x0, delta)]] = 1 + 2x0 > x0 = [[_x0]] 
  [[!times(delta, _x0)]] = x0 >= 0 = [[delta]] 
  [[sigma(/\x._x0)]] = x0 >= x0 = [[_x0]] 
  [[!plus(sigma(/\x.~AP1(_F0, x)), ~AP1(_F0, _x1))]] = 1 + x1 + 2F0(x1) + 4F0(0) > 2F0(0) = [[sigma(/\x.~AP1(_F0, x))]] 
  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = 1 + 2F1(0) + 4F0(0) >= 1 + 2F1(0) + 4F0(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 
  [[!times(sigma(/\x.~AP1(_F0, x)), _x1)]] = x1 + 2F0(0) + 4x1F0(0) >= x1 + 2F0(0) + 4x1F0(0) = [[sigma(/\x.!times(~AP1(_F0, x), _x1))]] 
  [[~AP1(_F0, _x1)]] = x1 + 2F0(x1) >= x1 + F0(x1) = [[_F0 _x1]] 

We can thus remove the following rules:

  !plus(X, X) => X 
  !plus(X, delta) => X 
  !plus(sigma(/\x.~AP1(F, x)), ~AP1(F, X)) => sigma(/\y.~AP1(F, y)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  !times(!plus(X, Y), Z) >? !plus(!times(X, Z), !times(Y, Z)) 
  !times(!times(X, Y), Z) >? !times(X, !times(Y, Z)) 
  !times(delta, X) >? delta 
  sigma(/\x.X) >? X 
  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
  !times(sigma(/\x.~AP1(F, x)), X) >? sigma(/\y.!times(~AP1(F, y), X)) 
  ~AP1(F, X) >? F X 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.1 + y0 + y1 
  !times = \y0y1.y0 + y1 + 2y0y1 
  delta = 0 
  sigma = \G0.G0(0) 
  ~AP1 = \G0y1.1 + y1 + 2G0(y1) 

Using this interpretation, the requirements translate to:

  [[!times(!plus(_x0, _x1), _x2)]] = 1 + x0 + x1 + 2x0x2 + 2x1x2 + 3x2 >= 1 + x0 + x1 + 2x0x2 + 2x1x2 + 2x2 = [[!plus(!times(_x0, _x2), !times(_x1, _x2))]] 
  [[!times(!times(_x0, _x1), _x2)]] = x0 + x1 + x2 + 2x0x1 + 2x0x2 + 2x1x2 + 4x0x1x2 >= x0 + x1 + x2 + 2x0x1 + 2x0x2 + 2x1x2 + 4x0x1x2 = [[!times(_x0, !times(_x1, _x2))]] 
  [[!times(delta, _x0)]] = x0 >= 0 = [[delta]] 
  [[sigma(/\x._x0)]] = x0 >= x0 = [[_x0]] 
  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = 3 + 2F0(0) + 2F1(0) >= 3 + 2F0(0) + 2F1(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 
  [[!times(sigma(/\x.~AP1(_F0, x)), _x1)]] = 1 + 3x1 + 2F0(0) + 4x1F0(0) >= 1 + 3x1 + 2F0(0) + 4x1F0(0) = [[sigma(/\x.!times(~AP1(_F0, x), _x1))]] 
  [[~AP1(_F0, _x1)]] = 1 + x1 + 2F0(x1) > x1 + F0(x1) = [[_F0 _x1]] 

We can thus remove the following rules:

  ~AP1(F, X) => F X 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  !times(!plus(X, Y), Z) >? !plus(!times(X, Z), !times(Y, Z)) 
  !times(!times(X, Y), Z) >? !times(X, !times(Y, Z)) 
  !times(delta, X) >? delta 
  sigma(/\x.X) >? X 
  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
  !times(sigma(/\x.~AP1(F, x)), X) >? sigma(/\y.!times(~AP1(F, y), X)) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.2 + y0 + y1 
  !times = \y0y1.y1 + 2y0 + 2y0y1 
  delta = 0 
  sigma = \G0.G0(0) 
  ~AP1 = \G0y1.y1 + 2G0(0) 

Using this interpretation, the requirements translate to:

  [[!times(!plus(_x0, _x1), _x2)]] = 4 + 2x0 + 2x0x2 + 2x1 + 2x1x2 + 5x2 > 2 + 2x0 + 2x0x2 + 2x1 + 2x1x2 + 2x2 = [[!plus(!times(_x0, _x2), !times(_x1, _x2))]] 
  [[!times(!times(_x0, _x1), _x2)]] = x2 + 2x1 + 2x1x2 + 4x0 + 4x0x1 + 4x0x1x2 + 4x0x2 >= x2 + 2x0 + 2x0x2 + 2x1 + 2x1x2 + 4x0x1 + 4x0x1x2 = [[!times(_x0, !times(_x1, _x2))]] 
  [[!times(delta, _x0)]] = x0 >= 0 = [[delta]] 
  [[sigma(/\x._x0)]] = x0 >= x0 = [[_x0]] 
  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = 2 + 2F0(0) + 2F1(0) >= 2 + 2F0(0) + 2F1(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 
  [[!times(sigma(/\x.~AP1(_F0, x)), _x1)]] = x1 + 4x1F0(0) + 4F0(0) >= x1 + 4x1F0(0) + 4F0(0) = [[sigma(/\x.!times(~AP1(_F0, x), _x1))]] 

We can thus remove the following rules:

  !times(!plus(X, Y), Z) => !plus(!times(X, Z), !times(Y, Z)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  !times(!times(X, Y), Z) >? !times(X, !times(Y, Z)) 
  !times(delta, X) >? delta 
  sigma(/\x.X) >? X 
  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
  !times(sigma(/\x.~AP1(F, x)), X) >? sigma(/\y.!times(~AP1(F, y), X)) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.y0 + y1 
  !times = \y0y1.3 + y1 + 3y0 
  delta = 0 
  sigma = \G0.G0(0) 
  ~AP1 = \G0y1.y1 + G0(0) 

Using this interpretation, the requirements translate to:

  [[!times(!times(_x0, _x1), _x2)]] = 12 + x2 + 3x1 + 9x0 > 6 + x2 + 3x0 + 3x1 = [[!times(_x0, !times(_x1, _x2))]] 
  [[!times(delta, _x0)]] = 3 + x0 > 0 = [[delta]] 
  [[sigma(/\x._x0)]] = x0 >= x0 = [[_x0]] 
  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = F0(0) + F1(0) >= F0(0) + F1(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 
  [[!times(sigma(/\x.~AP1(_F0, x)), _x1)]] = 3 + x1 + 3F0(0) >= 3 + x1 + 3F0(0) = [[sigma(/\x.!times(~AP1(_F0, x), _x1))]] 

We can thus remove the following rules:

  !times(!times(X, Y), Z) => !times(X, !times(Y, Z)) 
  !times(delta, X) => delta 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  sigma(/\x.X) >? X 
  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 
  !times(sigma(/\x.~AP1(F, x)), X) >? sigma(/\y.!times(~AP1(F, y), X)) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.2 + y0 + y1 
  !times = \y0y1.y1 + 2y0y1 + 3y0 
  sigma = \G0.2 + 2G0(0) 
  ~AP1 = \G0y1.y1 + 2G0(y1) 

Using this interpretation, the requirements translate to:

  [[sigma(/\x._x0)]] = 2 + 2x0 > x0 = [[_x0]] 
  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = 6 + 4F0(0) + 4F1(0) >= 6 + 4F0(0) + 4F1(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 
  [[!times(sigma(/\x.~AP1(_F0, x)), _x1)]] = 6 + 5x1 + 8x1F0(0) + 12F0(0) > 2 + 2x1 + 8x1F0(0) + 12F0(0) = [[sigma(/\x.!times(~AP1(_F0, x), _x1))]] 

We can thus remove the following rules:

  sigma(/\x.X) => X 
  !times(sigma(/\x.~AP1(F, x)), X) => sigma(/\y.!times(~AP1(F, y), X)) 

We use rule removal, following [Kop12, Theorem 2.23].

This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]):

  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) >? !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 

We orient these requirements with a polynomial interpretation in the natural numbers.

The following interpretation satisfies the requirements:

  !plus = \y0y1.3 + y0 + y1 
  sigma = \G0.3G0(0) 
  ~AP1 = \G0y1.y1 + G0(0) 

Using this interpretation, the requirements translate to:

  [[sigma(/\x.!plus(~AP1(_F0, x), ~AP1(_F1, x)))]] = 9 + 3F0(0) + 3F1(0) > 3 + 3F0(0) + 3F1(0) = [[!plus(sigma(/\x.~AP1(_F0, x)), sigma(/\y.~AP1(_F1, y)))]] 

We can thus remove the following rules:

  sigma(/\x.!plus(~AP1(F, x), ~AP1(G, x))) => !plus(sigma(/\y.~AP1(F, y)), sigma(/\z.~AP1(G, z))) 

All rules were succesfully removed.  Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold.


+++ Citations +++

[Kop11]  C. Kop.  Simplifying Algebraic Functional Systems.  In Proceedings of CAI 2011, volume 6742 of LNCS.  201--215, Springer, 2011.
[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.