We consider the system iterative.

  Alphabet:

    a : [] --> o 
    b : [] --> o 
    f : [o * o -> o] --> o 
    g : [o * o * o -> o] --> o 

  Rules:

    g(x, y, h) => f(f(x, h), h) 
    f(x, h) => b 
    b => a 
    f(b, /\x.g(x, x, h)) => g(f(a, /\y.g(y, y, h)), f(b, /\z.b), h) 

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]):

  g(X, Y, F) >? f(f(X, F), F) 
  f(X, F) >? b 
  b >? a 
  f(b, /\x.g(x, x, F)) >? g(f(a, /\y.g(y, y, F)), f(b, /\z.b), F) 

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

Argument functions:

  [[a]] = _|_ 

We choose Lex = {} and Mul = {b, f, g}, and the following precedence: g > f > b

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

  g(X, Y, F) >= f(f(X, F), F) 
  f(X, F) >= b 
  b > _|_ 
  f(b, /\x.g(x, x, F)) > g(f(_|_, /\x.g(x, x, F)), f(b, /\y.b), F) 

With these choices, we have:

  1] g(X, Y, F) >= f(f(X, F), F)  because [2], by (Star) 
  2] g*(X, Y, F) >= f(f(X, F), F)  because g > f, [3] and [6], by (Copy) 
  3] g*(X, Y, F) >= f(X, F)  because g > f, [4] and [6], by (Copy) 
  4] g*(X, Y, F) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] g*(X, Y, F) >= F  because [7], by (Select) 
  7] F >= F  by (Meta) 

  8] f(X, F) >= b  because [9], by (Star) 
  9] f*(X, F) >= b  because f > b, by (Copy) 

  10] b > _|_  because [11], by definition 
  11] b* >= _|_  by (Bot) 

  12] f(b, /\x.g(x, x, F)) > g(f(_|_, /\x.g(x, x, F)), f(b, /\y.b), F)  because [13], by definition 
  13] f*(b, /\x.g(x, x, F)) >= g(f(_|_, /\x.g(x, x, F)), f(b, /\y.b), F)  because [14], by (Select) 
  14] g(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F) >= g(f(_|_, /\x.g(x, x, F)), f(b, /\y.b), F)  because g in Mul, [15], [22] and [26], by (Fun) 
  15] f*(b, /\x.g(x, x, F)) >= f(b, /\x.b)  because [16], by (Select) 
  16] g(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F) >= f(b, /\x.b)  because [17], by (Star) 
  17] g*(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F) >= f(b, /\x.b)  because g > f, [18] and [20], by (Copy) 
  18] g*(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F) >= b  because [19], by (Select) 
  19] f*(b, /\x.g(x, x, F)) >= b  because f > b, by (Copy) 
  20] g*(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F) >= /\x.b  because [21], by (F-Abs) 
  21] g*(f*(b, /\x.g(x, x, F)), f*(b, /\y.g(y, y, F)), F, z) >= b  because g > b, by (Copy) 
  22] f*(b, /\x.g(x, x, F)) >= f(_|_, /\x.g(x, x, F))  because f in Mul, [10] and [23], by (Stat) 
  23] /\y.g(y, y, F) >= /\y.g(y, y, F)  because [24], by (Abs) 
  24] g(x, x, F) >= g(x, x, F)  because g in Mul, [25], [25] and [26], by (Fun) 
  25] x >= x  by (Var) 
  26] F >= F  by (Meta) 

We can thus remove the following rules:

  b => a 
  f(b, /\x.g(x, x, F)) => g(f(a, /\y.g(y, y, F)), f(b, /\z.b), F) 

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

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

  g(X, Y, F) >? f(f(X, F), F) 
  f(X, F) >? b 

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

Argument functions:

  [[b]] = _|_ 

We choose Lex = {} and Mul = {f, g}, and the following precedence: g > f

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

  g(X, Y, F) > f(f(X, F), F) 
  f(X, F) > _|_ 

With these choices, we have:

  1] g(X, Y, F) > f(f(X, F), F)  because [2], by definition 
  2] g*(X, Y, F) >= f(f(X, F), F)  because g > f, [3] and [6], by (Copy) 
  3] g*(X, Y, F) >= f(X, F)  because g > f, [4] and [6], by (Copy) 
  4] g*(X, Y, F) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] g*(X, Y, F) >= F  because [7], by (Select) 
  7] F >= F  by (Meta) 

  8] f(X, F) > _|_  because [9], by definition 
  9] f*(X, F) >= _|_  by (Bot) 

We can thus remove the following rules:

  g(X, Y, F) => f(f(X, F), F) 
  f(X, F) => b 

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.