We consider the system 515.

  Alphabet:

    cons : [a * alist] --> alist 
    map : [a -> a * alist] --> alist 
    nil : [] --> alist 

  Rules:

    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    map(/\x.X(x), map(/\y.Y(y), Z)) => map(/\z.X(Y(z)), Z) 

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs.

We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative):

  Dependency Pairs P_0:

    0] map#(/\x.X(x), cons(Y, Z)) =#> X(Y)   
    1] map#(/\x.X(x), cons(Y, Z)) =#> map#(/\y.X(y), Z)   
    2] map#(/\x.X(x), cons(Y, Z)) =#> X(y)   
    3] map#(/\x.X(x), map(/\y.Y(y), Z)) =#> map#(/\z.X(Y(z)), Z)   
    4] map#(/\x.X(x), map(/\y.Y(y), Z)) =#> X(Y(z))   
    5] map#(/\x.X(x), map(/\y.Y(y), Z)) =#> Y(z) {X : 1}  

  Rules R_0:

    map(/\x.X(x), nil) => nil 
    map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
    map(/\x.X(x), map(/\y.Y(y), Z)) => map(/\z.X(Y(z)), Z) 

Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_0, minimal, formative).

The formative rules of (P_0, R_0) are R_1 ::=

  map(/\x.X(x), cons(Y, Z)) => cons(X(Y), map(/\y.X(y), Z)) 
  map(/\x.X(x), map(/\y.Y(y), Z)) => map(/\z.X(Y(z)), Z) 

By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_0, R_0, minimal, formative) by (P_0, R_1, minimal, formative).

Thus, the original system is terminating if (P_0, R_1, minimal, formative) is finite.

We consider the dependency pair problem (P_0, R_1, minimal, formative).

We will use the reduction pair processor [Kop12, Thm. 7.16].  As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70].  Thus, we must orient:

  map#(/\x.X(x), cons(Y, Z)) >? X(Y) 
  map#(/\x.X(x), cons(Y, Z)) >? map#(/\y.X(y), Z) 
  map#(/\x.X(x), cons(Y, Z)) >? X(~c0) 
  map#(/\x.X(x), map(/\y.Y(y), Z)) >? map#(/\z.X(Y(z)), Z) 
  map#(/\x.X(x), map(/\y.Y(y), Z)) >? X(Y(~c1)) 
  map#(/\x.X(x), map(/\y.Y(y), Z)) >? Y(~c2) 
  map(/\x.X(x), cons(Y, Z)) >= cons(X(Y), map(/\y.X(y), Z)) 
  map(/\x.X(x), map(/\y.Y(y), Z)) >= map(/\z.X(Y(z)), Z) 

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

The following interpretation satisfies the requirements:

  cons = \y0y1.2 + y0 + y1 
  map = \G0y1.1 + 2y1 + G0(0) + G0(y1) + 2y1G0(y1) 
  map# = \G0y1.3 + 2y1 + G0(y1) + 2y1G0(y1) 
  ~c0 = 0 
  ~c1 = 0 
  ~c2 = 0 

Using this interpretation, the requirements translate to:

  [[map#(/\x._x0(x), cons(_x1, _x2))]] = 7 + 2x1 + 2x2 + 2x1F0(2 + x1 + x2) + 2x2F0(2 + x1 + x2) + 5F0(2 + x1 + x2) > F0(x1) = [[_x0(_x1)]] 
  [[map#(/\x._x0(x), cons(_x1, _x2))]] = 7 + 2x1 + 2x2 + 2x1F0(2 + x1 + x2) + 2x2F0(2 + x1 + x2) + 5F0(2 + x1 + x2) > 3 + 2x2 + F0(x2) + 2x2F0(x2) = [[map#(/\x._x0(x), _x2)]] 
  [[map#(/\x._x0(x), cons(_x1, _x2))]] = 7 + 2x1 + 2x2 + 2x1F0(2 + x1 + x2) + 2x2F0(2 + x1 + x2) + 5F0(2 + x1 + x2) > F0(0) = [[_x0(~c0)]] 
  [[map#(/\x._x0(x), map(/\y._x1(y), _x2))]] = 5 + 4x2 + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(0) + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 2F1(0) + 2F1(x2) + 3F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 4x2F1(x2) > 3 + 2x2 + F0(F1(x2)) + 2x2F0(F1(x2)) = [[map#(/\x._x0(_x1(x)), _x2)]] 
  [[map#(/\x._x0(x), map(/\y._x1(y), _x2))]] = 5 + 4x2 + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(0) + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 2F1(0) + 2F1(x2) + 3F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 4x2F1(x2) > F0(F1(0)) = [[_x0(_x1(~c1))]] 
  [[map#(/\x._x0(x), map(/\y._x1(y), _x2))]] = 5 + 4x2 + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(0) + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 2F1(0) + 2F1(x2) + 3F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 4x2F1(x2) > F1(0) = [[_x1(~c2)]] 
  [[map(/\x._x0(x), cons(_x1, _x2))]] = 5 + 2x1 + 2x2 + F0(0) + 2x1F0(2 + x1 + x2) + 2x2F0(2 + x1 + x2) + 5F0(2 + x1 + x2) >= 3 + 2x2 + F0(0) + F0(x1) + F0(x2) + 2x2F0(x2) = [[cons(_x0(_x1), map(/\x._x0(x), _x2))]] 
  [[map(/\x._x0(x), map(/\y._x1(y), _x2))]] = 3 + 4x2 + F0(0) + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(0) + 2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 2F1(0) + 2F1(x2) + 3F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2)) + 4x2F0(1 + 2x2 + F1(0) + F1(x2) + 2x2F1(x2))F1(x2) + 4x2F1(x2) >= 1 + 2x2 + F0(F1(0)) + F0(F1(x2)) + 2x2F0(F1(x2)) = [[map(/\x._x0(_x1(x)), _x2)]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_0, R_1) by ({}, R_1).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination.


+++ Citations +++

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