We consider the system 09ex.

  Alphabet:

    c : [] --> ((C -> L) -> L) -> C 
    d : [] --> C 
    ex : [] --> C -> L 
    nil : [] --> L 

  Rules:

    ex d => nil 
    ex (c (/\f.g f)) => g ex 

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:

    c : [(C -> L) -> L] --> C 
    d : [] --> C 
    ex : [] --> C -> L 
    nil : [] --> L 
    ~AP1 : [(C -> L) -> L * C -> L] --> L 

  Rules:

    ex d => nil 
    ex c(/\f.~AP1(F, f)) => ~AP1(F, ex) 
    ~AP1(F, G) => F G 

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

After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, all):

  Dependency Pairs P_0:

    0] ex c(/\f.~AP1(F, f)) =#> ~AP1#(F, ex)   
    1] ex c(/\f.~AP1(F, f)) =#> ex#   
    2] ~AP1#(F, G) =#> F(G)   

  Rules R_0:

    ex d => nil 
    ex c(/\f.~AP1(F, f)) => ~AP1(F, ex) 
    ~AP1(F, G) => F G 

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 : 2 
    * 1 :  
    * 2 : 0, 1, 2 

This graph has the following strongly connected components:

  P_1:

    ex c(/\f.~AP1(F, f)) =#> ~AP1#(F, ex)   
    ~AP1#(F, G) =#> F(G)   

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:

  ex c(/\f.~AP1(F, f)) >? ~AP1#(F, ex) 
  ~AP1#(F, G) >? F(G) 
  ex d >= nil 
  ex c(/\f.~AP1(F, f)) >= ~AP1(F, ex) 
  ~AP1(F, G) >= F G 
  ~AP1(F, G) >= ~AP1#(F, G) 

We apply [Kop12, Thm. 6.75] and use the following argument functions:

  pi( ~AP1#(F, G) ) = #argfun-~AP1##(F G) 

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:

  [[ex]] = _|_ 
  [[nil]] = _|_ 

We choose Lex = {@_{(o -> o) -> o}} and Mul = {#argfun-~AP1##, @_{o -> o}, c, d, ~AP1, ~AP1#}, and the following precedence: d > ~AP1# > c > ~AP1 > @_{(o -> o) -> o} > @_{o -> o} > #argfun-~AP1##

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

  @_{o -> o}(_|_, c(/\f.~AP1(F, f))) > #argfun-~AP1##(@_{(o -> o) -> o}(F, _|_)) 
  #argfun-~AP1##(@_{(o -> o) -> o}(F, G)) > @_{(o -> o) -> o}(F, G) 
  @_{o -> o}(_|_, d) >= _|_ 
  @_{o -> o}(_|_, c(/\f.~AP1(F, f))) >= ~AP1(F, _|_) 
  ~AP1(F, G) >= @_{(o -> o) -> o}(F, G) 
  ~AP1(F, G) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, G)) 

With these choices, we have:

  1] @_{o -> o}(_|_, c(/\f.~AP1(F, f))) > #argfun-~AP1##(@_{(o -> o) -> o}(F, _|_))  because [2], by definition 
  2] @_{o -> o}*(_|_, c(/\f.~AP1(F, f))) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, _|_))  because [3], by (Select) 
  3] c(/\f.~AP1(F, f)) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, _|_))  because [4], by (Star) 
  4] c*(/\f.~AP1(F, f)) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, _|_))  because c > #argfun-~AP1## and [5], by (Copy) 
  5] c*(/\f.~AP1(F, f)) >= @_{(o -> o) -> o}(F, _|_)  because c > @_{(o -> o) -> o}, [6] and [9], by (Copy) 
  6] c*(/\f.~AP1(F, f)) >= F  because [7], by (Select) 
  7] /\f.~AP1(F, f) >= F  because [8], by (Eta)[Kop13:2] 
  8] F >= F  by (Meta) 
  9] c*(/\f.~AP1(F, f)) >= _|_  by (Bot) 

  10] #argfun-~AP1##(@_{(o -> o) -> o}(F, G)) > @_{(o -> o) -> o}(F, G)  because [11], by definition 
  11] #argfun-~AP1##*(@_{(o -> o) -> o}(F, G)) >= @_{(o -> o) -> o}(F, G)  because [12], by (Select) 
  12] @_{(o -> o) -> o}(F, G) >= @_{(o -> o) -> o}(F, G)  because [13] and [14], by (Fun) 
  13] F >= F  by (Meta) 
  14] G >= G  by (Meta) 

  15] @_{o -> o}(_|_, d) >= _|_  by (Bot) 

  16] @_{o -> o}(_|_, c(/\f.~AP1(F, f))) >= ~AP1(F, _|_)  because [17], by (Star) 
  17] @_{o -> o}*(_|_, c(/\f.~AP1(F, f))) >= ~AP1(F, _|_)  because [18], by (Select) 
  18] c(/\f.~AP1(F, f)) >= ~AP1(F, _|_)  because [19], by (Star) 
  19] c*(/\f.~AP1(F, f)) >= ~AP1(F, _|_)  because c > ~AP1, [6] and [9], by (Copy) 

  20] ~AP1(F, G) >= @_{(o -> o) -> o}(F, G)  because [21], by (Star) 
  21] ~AP1*(F, G) >= @_{(o -> o) -> o}(F, G)  because ~AP1 > @_{(o -> o) -> o}, [22] and [23], by (Copy) 
  22] ~AP1*(F, G) >= F  because [13], by (Select) 
  23] ~AP1*(F, G) >= G  because [14], by (Select) 

  24] ~AP1(F, G) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, G))  because [25], by (Star) 
  25] ~AP1*(F, G) >= #argfun-~AP1##(@_{(o -> o) -> o}(F, G))  because ~AP1 > #argfun-~AP1## and [26], by (Copy) 
  26] ~AP1*(F, G) >= @_{(o -> o) -> o}(F, G)  because ~AP1 > @_{(o -> o) -> o}, [27] and [29], by (Copy) 
  27] ~AP1*(F, G) >= F  because [28], by (Select) 
  28] F >= F  by (Meta) 
  29] ~AP1*(F, G) >= G  because [30], by (Select) 
  30] G >= G  by (Meta) 

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.
[Kop13:2]  C. Kop.  StarHorpo with an Eta-Rule.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.