We consider the system Applicative_05__Ex6Folding.

  Alphabet:

    0 : [] --> c 
    1 : [] --> c 
    add : [] --> c -> a -> c 
    cons : [a * b] --> b 
    fold : [c -> a -> c * b * c] --> c 
    mul : [] --> c -> a -> c 
    nil : [] --> b 
    prod : [b] --> c 
    sum : [b] --> c 

  Rules:

    fold(f, nil, x) => x 
    fold(f, cons(x, y), z) => fold(f, y, f z x) 
    sum(x) => fold(add, x, 0) 
    fold(mul, x, 1) => prod(x) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

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

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

  fold(F, nil, X) >? X 
  fold(F, cons(X, Y), Z) >? fold(F, Y, F Z X) 
  sum(X) >? fold(add, X, 0) 
  fold(mul, X, 1) >? prod(X) 

We use a recursive path ordering as defined in [Kop12, Chapter 5].

Argument functions:

  [[0]] = _|_ 
  [[add]] = _|_ 
  [[cons(x_1, x_2)]] = cons(x_2, x_1) 
  [[prod(x_1)]] = x_1 

We choose Lex = {cons, fold} and Mul = {1, @_{o -> o -> o}, @_{o -> o}, mul, nil, sum}, and the following precedence: 1 > cons > mul > nil > sum > fold > @_{o -> o -> o} > @_{o -> o}

Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows:

  fold(F, nil, X) > X 
  fold(F, cons(X, Y), Z) > fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) 
  sum(X) >= fold(_|_, X, _|_) 
  fold(mul, X, 1) > X 

With these choices, we have:

  1] fold(F, nil, X) > X  because [2], by definition 
  2] fold*(F, nil, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] fold(F, cons(X, Y), Z) > fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X))  because [5], by definition 
  5] fold*(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X))  because [6], [7], [10], [11], [13] and [6], by (Stat) 
  6] F >= F  by (Meta) 
  7] cons(X, Y) > Y  because [8], by definition 
  8] cons*(X, Y) >= Y  because [9], by (Select) 
  9] Y >= Y  by (Meta) 
  10] fold*(F, cons(X, Y), Z) >= F  because [6], by (Select) 
  11] fold*(F, cons(X, Y), Z) >= Y  because [12], by (Select) 
  12] cons(X, Y) >= Y  because [8], by (Star) 
  13] fold*(F, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(F, Z), X)  because fold > @_{o -> o}, [14] and [17], by (Copy) 
  14] fold*(F, cons(X, Y), Z) >= @_{o -> o -> o}(F, Z)  because fold > @_{o -> o -> o}, [10] and [15], by (Copy) 
  15] fold*(F, cons(X, Y), Z) >= Z  because [16], by (Select) 
  16] Z >= Z  by (Meta) 
  17] fold*(F, cons(X, Y), Z) >= X  because [18], by (Select) 
  18] cons(X, Y) >= X  because [19], by (Star) 
  19] cons*(X, Y) >= X  because [20], by (Select) 
  20] X >= X  by (Meta) 

  21] sum(X) >= fold(_|_, X, _|_)  because [22], by (Star) 
  22] sum*(X) >= fold(_|_, X, _|_)  because sum > fold, [23], [24] and [26], by (Copy) 
  23] sum*(X) >= _|_  by (Bot) 
  24] sum*(X) >= X  because [25], by (Select) 
  25] X >= X  by (Meta) 
  26] sum*(X) >= _|_  by (Bot) 

  27] fold(mul, X, 1) > X  because [28], by definition 
  28] fold*(mul, X, 1) >= X  because [29], by (Select) 
  29] X >= X  by (Meta) 

We can thus remove the following rules:

  fold(F, nil, X) => X 
  fold(F, cons(X, Y), Z) => fold(F, Y, F Z X) 
  fold(mul, X, 1) => prod(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]):

  sum(X) >? fold(add, X, 0) 

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

The following interpretation satisfies the requirements:

  0 = 0 
  add = Lam[y0;y1].0 
  fold = Lam[G0;y1;y2].y1 + y2 + 2*G0(0,0) + 2*G0(y1,y2) 
  sum = Lam[y0].3 + 3*y0 

Using this interpretation, the requirements translate to:

  [[sum(_x0)]] = 3 + 3*x0 > x0 = [[fold(add, _x0, 0)]] 

We can thus remove the following rules:

  sum(X) => fold(add, X, 0) 

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 +++

[Kop12]  C. Kop.  Higher Order Termination.  PhD Thesis, 2012.