We consider the system h61.

  Alphabet:

    app : [] --> list -> list -> list 
    cons : [] --> nat -> list -> list 
    foldl : [] --> (list -> nat -> list) -> list -> list -> list 
    iconsc : [] --> list -> nat -> list 
    nil : [] --> list 
    reverse : [] --> list -> list 
    reverse1 : [] --> list -> list 

  Rules:

    app nil x => x 
    app (cons x y) z => cons x (app y z) 
    foldl (/\x./\y.f x y) z nil => z 
    foldl (/\x./\y.f x y) z (cons u v) => foldl (/\w./\x'.f w x') (f z u) v 
    iconsc x y => cons y x 
    reverse x => foldl (/\y./\z.iconsc y z) nil x 
    reverse1 x => foldl (/\y./\z.app (cons z nil) y) nil x 

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:

    app : [list * list] --> list 
    cons : [nat * list] --> list 
    foldl : [list -> nat -> list * list * list] --> list 
    iconsc : [list * nat] --> list 
    nil : [] --> list 
    reverse : [list] --> list 
    reverse1 : [list] --> list 
    ~AP1 : [list -> nat -> list * list] --> nat -> list 

  Rules:

    app(nil, X) => X 
    app(cons(X, Y), Z) => cons(X, app(Y, Z)) 
    foldl(/\x./\y.~AP1(F, x) y, X, nil) => X 
    foldl(/\x./\y.~AP1(F, x) y, X, cons(Y, Z)) => foldl(/\z./\u.~AP1(F, z) u, ~AP1(F, X) Y, Z) 
    iconsc(X, Y) => cons(Y, X) 
    reverse(X) => foldl(/\x./\y.iconsc(x, y), nil, X) 
    reverse1(X) => foldl(/\x./\y.app(cons(y, nil), x), nil, X) 
    foldl(/\x./\y.iconsc(x, y), X, nil) => X 
    foldl(/\x./\y.iconsc(x, y), X, cons(Y, Z)) => foldl(/\z./\u.iconsc(z, u), iconsc(X, Y), Z) 
    ~AP1(F, X) => F X 

Symbol ~AP1 is an encoding for application that is only used in innocuous ways.  We can simplify the program (without losing non-termination) by removing it.  Additionally, we can remove some (now-)redundant rules.  This gives:

  Alphabet:

    app : [list * list] --> list 
    cons : [nat * list] --> list 
    foldl : [list -> nat -> list * list * list] --> list 
    iconsc : [list * nat] --> list 
    nil : [] --> list 
    reverse : [list] --> list 
    reverse1 : [list] --> list 

  Rules:

    app(nil, X) => X 
    app(cons(X, Y), Z) => cons(X, app(Y, Z)) 
    foldl(/\x./\y.X(x, y), Y, nil) => Y 
    foldl(/\x./\y.X(x, y), Y, cons(Z, U)) => foldl(/\z./\u.X(z, u), X(Y, Z), U) 
    iconsc(X, Y) => cons(Y, X) 
    reverse(X) => foldl(/\x./\y.iconsc(x, y), nil, X) 
    reverse1(X) => foldl(/\x./\y.app(cons(y, nil), x), nil, 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]):

  app(nil, X) >? X 
  app(cons(X, Y), Z) >? cons(X, app(Y, Z)) 
  foldl(/\x./\y.X(x, y), Y, nil) >? Y 
  foldl(/\x./\y.X(x, y), Y, cons(Z, U)) >? foldl(/\z./\u.X(z, u), X(Y, Z), U) 
  iconsc(X, Y) >? cons(Y, X) 
  reverse(X) >? foldl(/\x./\y.iconsc(x, y), nil, X) 
  reverse1(X) >? foldl(/\x./\y.app(cons(y, nil), x), nil, X) 

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

Argument functions:

  [[foldl(x_1, x_2, x_3)]] = foldl(x_3, x_2, x_1) 
  [[nil]] = _|_ 

We choose Lex = {foldl} and Mul = {app, cons, iconsc, reverse, reverse1}, and the following precedence: reverse > iconsc > reverse1 > app > cons > foldl

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

  app(_|_, X) > X 
  app(cons(X, Y), Z) >= cons(X, app(Y, Z)) 
  foldl(/\x./\y.X(x, y), Y, _|_) > Y 
  foldl(/\x./\y.X(x, y), Y, cons(Z, U)) > foldl(/\x./\y.X(x, y), X(Y, Z), U) 
  iconsc(X, Y) > cons(Y, X) 
  reverse(X) >= foldl(/\x./\y.iconsc(x, y), _|_, X) 
  reverse1(X) >= foldl(/\x./\y.app(cons(y, _|_), x), _|_, X) 

With these choices, we have:

  1] app(_|_, X) > X  because [2], by definition 
  2] app*(_|_, X) >= X  because [3], by (Select) 
  3] X >= X  by (Meta) 

  4] app(cons(X, Y), Z) >= cons(X, app(Y, Z))  because [5], by (Star) 
  5] app*(cons(X, Y), Z) >= cons(X, app(Y, Z))  because app > cons, [6] and [10], by (Copy) 
  6] app*(cons(X, Y), Z) >= X  because [7], by (Select) 
  7] cons(X, Y) >= X  because [8], by (Star) 
  8] cons*(X, Y) >= X  because [9], by (Select) 
  9] X >= X  by (Meta) 
  10] app*(cons(X, Y), Z) >= app(Y, Z)  because app in Mul, [11] and [14], by (Stat) 
  11] cons(X, Y) > Y  because [12], by definition 
  12] cons*(X, Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 
  14] Z >= Z  by (Meta) 

  15] foldl(/\x./\y.X(x, y), Y, _|_) > Y  because [16], by definition 
  16] foldl*(/\x./\y.X(x, y), Y, _|_) >= Y  because [17], by (Select) 
  17] Y >= Y  by (Meta) 

  18] foldl(/\x./\y.X(x, y), Y, cons(Z, U)) > foldl(/\x./\y.X(x, y), X(Y, Z), U)  because [19], by definition 
  19] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= foldl(/\x./\y.X(x, y), X(Y, Z), U)  because [20], [23], [30] and [38], by (Stat) 
  20] cons(Z, U) > U  because [21], by definition 
  21] cons*(Z, U) >= U  because [22], by (Select) 
  22] U >= U  by (Meta) 
  23] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= /\x./\y.X(x, y)  because [24], by (F-Abs) 
  24] foldl*(/\x./\y.X(x, y), Y, cons(Z, U), z) >= /\x.X(z, x)  because [25], by (Select) 
  25] /\x.X(foldl*(/\y./\v.X(y, v), Y, cons(Z, U), z), x) >= /\x.X(z, x)  because [26], by (Abs) 
  26] X(foldl*(/\x./\y.X(x, y), Y, cons(Z, U), z), u) >= X(z, u)  because [27] and [29], by (Meta) 
  27] foldl*(/\x./\y.X(x, y), Y, cons(Z, U), z) >= z  because [28], by (Select) 
  28] z >= z  by (Var) 
  29] u >= u  by (Var) 
  30] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= X(Y, Z)  because [31], by (Select) 
  31] X(foldl*(/\x./\y.X(x, y), Y, cons(Z, U)), foldl*(/\v./\w.X(v, w), Y, cons(Z, U))) >= X(Y, Z)  because [32] and [34], by (Meta) 
  32] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= Y  because [33], by (Select) 
  33] Y >= Y  by (Meta) 
  34] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= Z  because [35], by (Select) 
  35] cons(Z, U) >= Z  because [36], by (Star) 
  36] cons*(Z, U) >= Z  because [37], by (Select) 
  37] Z >= Z  by (Meta) 
  38] foldl*(/\x./\y.X(x, y), Y, cons(Z, U)) >= U  because [39], by (Select) 
  39] cons(Z, U) >= U  because [21], by (Star) 

  40] iconsc(X, Y) > cons(Y, X)  because [41], by definition 
  41] iconsc*(X, Y) >= cons(Y, X)  because iconsc > cons, [42] and [44], by (Copy) 
  42] iconsc*(X, Y) >= Y  because [43], by (Select) 
  43] Y >= Y  by (Meta) 
  44] iconsc*(X, Y) >= X  because [45], by (Select) 
  45] X >= X  by (Meta) 

  46] reverse(X) >= foldl(/\x./\y.iconsc(x, y), _|_, X)  because [47], by (Star) 
  47] reverse*(X) >= foldl(/\x./\y.iconsc(x, y), _|_, X)  because reverse > foldl, [48], [55] and [56], by (Copy) 
  48] reverse*(X) >= /\y./\z.iconsc(y, z)  because [49], by (F-Abs) 
  49] reverse*(X, x) >= /\z.iconsc(x, z)  because [50], by (F-Abs) 
  50] reverse*(X, x, y) >= iconsc(x, y)  because reverse > iconsc, [51] and [53], by (Copy) 
  51] reverse*(X, x, y) >= x  because [52], by (Select) 
  52] x >= x  by (Var) 
  53] reverse*(X, x, y) >= y  because [54], by (Select) 
  54] y >= y  by (Var) 
  55] reverse*(X) >= _|_  by (Bot) 
  56] reverse*(X) >= X  because [57], by (Select) 
  57] X >= X  by (Meta) 

  58] reverse1(X) >= foldl(/\x./\y.app(cons(y, _|_), x), _|_, X)  because [59], by (Star) 
  59] reverse1*(X) >= foldl(/\x./\y.app(cons(y, _|_), x), _|_, X)  because reverse1 > foldl, [60], [69] and [70], by (Copy) 
  60] reverse1*(X) >= /\y./\z.app(cons(z, _|_), y)  because [61], by (F-Abs) 
  61] reverse1*(X, x) >= /\z.app(cons(z, _|_), x)  because [62], by (F-Abs) 
  62] reverse1*(X, x, y) >= app(cons(y, _|_), x)  because reverse1 > app, [63] and [67], by (Copy) 
  63] reverse1*(X, x, y) >= cons(y, _|_)  because reverse1 > cons, [64] and [66], by (Copy) 
  64] reverse1*(X, x, y) >= y  because [65], by (Select) 
  65] y >= y  by (Var) 
  66] reverse1*(X, x, y) >= _|_  by (Bot) 
  67] reverse1*(X, x, y) >= x  because [68], by (Select) 
  68] x >= x  by (Var) 
  69] reverse1*(X) >= _|_  by (Bot) 
  70] reverse1*(X) >= X  because [71], by (Select) 
  71] X >= X  by (Meta) 

We can thus remove the following rules:

  app(nil, X) => X 
  foldl(/\x./\y.X(x, y), Y, nil) => Y 
  foldl(/\x./\y.X(x, y), Y, cons(Z, U)) => foldl(/\z./\u.X(z, u), X(Y, Z), U) 
  iconsc(X, Y) => cons(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]):

  app(cons(X, Y), Z) >? cons(X, app(Y, Z)) 
  reverse(X) >? foldl(/\x./\y.iconsc(x, y), nil, X) 
  reverse1(X) >? foldl(/\x./\y.app(cons(y, nil), x), nil, X) 

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

The following interpretation satisfies the requirements:

  app = \y0y1.y1 + 2y0 
  cons = \y0y1.1 + y0 + y1 
  foldl = \G0y1y2.y1 + y2 + G0(0,0) 
  iconsc = \y0y1.y0 + y1 
  nil = 0 
  reverse = \y0.3 + 3y0 
  reverse1 = \y0.3 + 3y0 

Using this interpretation, the requirements translate to:

  [[app(cons(_x0, _x1), _x2)]] = 2 + x2 + 2x0 + 2x1 > 1 + x0 + x2 + 2x1 = [[cons(_x0, app(_x1, _x2))]] 
  [[reverse(_x0)]] = 3 + 3x0 > x0 = [[foldl(/\x./\y.iconsc(x, y), nil, _x0)]] 
  [[reverse1(_x0)]] = 3 + 3x0 > 2 + x0 = [[foldl(/\x./\y.app(cons(y, nil), x), nil, _x0)]] 

We can thus remove the following rules:

  app(cons(X, Y), Z) => cons(X, app(Y, Z)) 
  reverse(X) => foldl(/\x./\y.iconsc(x, y), nil, X) 
  reverse1(X) => foldl(/\x./\y.app(cons(y, nil), x), nil, X) 

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.