We consider the system restriction.

  Alphabet:

    New : [] --> (N -> A) -> A 

  Rules:

    New (/\x.y) => y 
    New (/\x.New (/\y.f x y)) => New (/\z.New (/\u.f u z)) 

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:

    New : [N -> A] --> A 
    ~AP1 : [N -> N -> A * N] --> N -> A 

  Rules:

    New(/\x.X) => X 
    New(/\x.New(/\y.~AP1(F, x) y)) => New(/\z.New(/\u.~AP1(F, u) z)) 
    ~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]):

  New(/\x.X) >? X 
  New(/\x.New(/\y.~AP1(F, x) y)) >? New(/\z.New(/\u.~AP1(F, u) z)) 
  ~AP1(F, X) >? F X 

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

The following interpretation satisfies the requirements:

  New = \G0.3 + G0(0) 
  ~AP1 = \G0y1y2.3 + y1 + G0(y1,y2) 

Using this interpretation, the requirements translate to:

  [[New(/\x._x0)]] = 3 + x0 > x0 = [[_x0]] 
  [[New(/\x.New(/\y.~AP1(_F0, x) y))]] = 9 + F0(0,0) >= 9 + F0(0,0) = [[New(/\x.New(/\y.~AP1(_F0, y) x))]] 
  [[~AP1(_F0, _x1)]] = \y0.3 + x1 + F0(x1,y0) > \y0.x1 + F0(x1,y0) = [[_F0 _x1]] 

We can thus remove the following rules:

  New(/\x.X) => X 
  ~AP1(F, X) => F X 

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, all):

  Dependency Pairs P_0:

    0] New#(/\x.New(/\y.~AP1(F, x, y))) =#> New#(/\z.New(/\u.~AP1(F, u, z)))   
    1] New#(/\x.New(/\y.~AP1(F, x, y))) =#> New#(/\z.~AP1(F, z, u))   

  Rules R_0:

    New(/\x.New(/\y.~AP1(F, x, y))) => New(/\z.New(/\u.~AP1(F, u, z))) 

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

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

We place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows:

    * 0 : 0, 1 
    * 1 :  

This graph has the following strongly connected components:

  P_1:

    New#(/\x.New(/\y.~AP1(F, x, y))) =#> New#(/\z.New(/\u.~AP1(F, u, z)))   

By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f).

Thus, the original system is terminating if (P_1, R_0, minimal, all) is finite.

We consider the dependency pair problem (P_1, R_0, minimal, all).

We will use the reduction pair processor [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  New#(/\x.New(/\y.~AP1(F, x, y))) >? New#(/\z.New(/\u.~AP1(F, u, z))) 
  New(/\x.New(/\y.~AP1(F, x, y))) >= New(/\z.New(/\u.~AP1(F, u, z))) 

Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.)

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

Argument functions:

  [[~AP1(x_1, x_2, x_3)]] = ~AP1(x_1, x_2) 

We choose Lex = {} and Mul = {New, New#, ~AP1}, and the following precedence: ~AP1 > New# > New

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

  New#(/\x.New(/\y.~AP1(F, x))) > New#(/\x.New(/\y.~AP1(F, y))) 
  New(/\x.New(/\y.~AP1(F, x))) >= New(/\x.New(/\y.~AP1(F, y))) 

With these choices, we have:

  1] New#(/\x.New(/\y.~AP1(F, x))) > New#(/\x.New(/\y.~AP1(F, y)))  because [2], by definition 
  2] New#*(/\x.New(/\y.~AP1(F, x))) >= New#(/\x.New(/\y.~AP1(F, y)))  because [3], by (Select) 
  3] New(/\x.~AP1(F, New#*(/\y.New(/\z.~AP1(F, y))))) >= New#(/\x.New(/\y.~AP1(F, y)))  because [4], by (Star) 
  4] New*(/\x.~AP1(F, New#*(/\y.New(/\z.~AP1(F, y))))) >= New#(/\x.New(/\y.~AP1(F, y)))  because [5], by (Select) 
  5] ~AP1(F, New#*(/\x.New(/\y.~AP1(F, x)))) >= New#(/\x.New(/\y.~AP1(F, y)))  because [6], by (Star) 
  6] ~AP1*(F, New#*(/\x.New(/\y.~AP1(F, x)))) >= New#(/\x.New(/\y.~AP1(F, y)))  because ~AP1 > New# and [7], by (Copy) 
  7] ~AP1*(F, New#*(/\x.New(/\y.~AP1(F, x)))) >= /\x.New(/\y.~AP1(F, y))  because [8], by (F-Abs) 
  8] ~AP1*(F, New#*(/\x.New(/\y.~AP1(F, x))), z) >= New(/\x.~AP1(F, x))  because [9], by (Select) 
  9] New#*(/\x.New(/\y.~AP1(F, x))) >= New(/\x.~AP1(F, x))  because New# > New and [10], by (Copy) 
  10] New#*(/\x.New(/\y.~AP1(F, x))) >= /\x.~AP1(F, x)  because [11], by (Select) 
  11] /\x.New(/\u.~AP1(F, x)) >= /\x.~AP1(F, x)  because [12], by (Abs) 
  12] New(/\x.~AP1(F, y)) >= ~AP1(F, y)  because [13], by (Star) 
  13] New*(/\x.~AP1(F, y)) >= ~AP1(F, y)  because [14], by (Select) 
  14] ~AP1(F, y) >= ~AP1(F, y)  because ~AP1 in Mul, [15] and [16], by (Fun) 
  15] F >= F  by (Meta) 
  16] y >= y  by (Var) 

  17] New(/\x.New(/\y.~AP1(F, x))) >= New(/\x.New(/\y.~AP1(F, y)))  because [18], by (Star) 
  18] New*(/\x.New(/\y.~AP1(F, x))) >= New(/\x.New(/\y.~AP1(F, y)))  because [19], by (Select) 
  19] New(/\x.~AP1(F, New*(/\y.New(/\z.~AP1(F, y))))) >= New(/\x.New(/\y.~AP1(F, y)))  because [20], by (Star) 
  20] New*(/\x.~AP1(F, New*(/\y.New(/\z.~AP1(F, y))))) >= New(/\x.New(/\y.~AP1(F, y)))  because [21], by (Select) 
  21] ~AP1(F, New*(/\x.New(/\y.~AP1(F, x)))) >= New(/\x.New(/\y.~AP1(F, y)))  because [22], by (Star) 
  22] ~AP1*(F, New*(/\x.New(/\y.~AP1(F, x)))) >= New(/\x.New(/\y.~AP1(F, y)))  because ~AP1 > New and [23], by (Copy) 
  23] ~AP1*(F, New*(/\x.New(/\y.~AP1(F, x)))) >= /\x.New(/\y.~AP1(F, y))  because [24], by (F-Abs) 
  24] ~AP1*(F, New*(/\x.New(/\y.~AP1(F, x))), z) >= New(/\x.~AP1(F, x))  because [25], by (Select) 
  25] New*(/\x.New(/\y.~AP1(F, x))) >= New(/\x.~AP1(F, x))  because New in Mul and [26], by (Stat) 
  26] /\x.New(/\y.~AP1(F, x)) > /\x.~AP1(F, x)  because [27], by definition 
  27] /\x.New*(/\u.~AP1(F, x)) >= /\x.~AP1(F, x)  because [28], by (Abs) 
  28] New*(/\x.~AP1(F, y)) >= ~AP1(F, y)  because [29], by (Select) 
  29] ~AP1(F, y) >= ~AP1(F, y)  because ~AP1 in Mul, [15] and [30], by (Fun) 
  30] y >= y  by (Var) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, R_0) by ({}, R_0).  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 +++

[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.