We consider the system plode.

  Alphabet:

    cons : [nat * list] --> list 
    explode : [list * nat -> nat * nat] --> nat 
    implode : [list * nat -> nat * nat] --> nat 
    nil : [] --> list 
    op : [nat -> nat * nat -> nat] --> nat -> nat 

  Rules:

    op(f, g) x => f (g x) 
    implode(nil, f, x) => x 
    implode(cons(x, y), f, z) => implode(y, f, f z) 
    explode(nil, f, x) => x 
    explode(cons(x, y), f, z) => explode(y, op(f, f), f z) 

This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0).

We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]).

In order to do so, we start by eta-expanding the system, which gives:

  op(F, G, X) => F (G X) 
  implode(nil, F, X) => X 
  implode(cons(X, Y), F, Z) => implode(Y, F, F Z) 
  explode(nil, F, X) => X 
  explode(cons(X, Y), F, Z) => explode(Y, /\x.op(F, F, x), F Z) 

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

  Dependency Pairs P_0:

    0] implode#(cons(X, Y), F, Z) =#> implode#(Y, F, F Z)   
    1] explode#(cons(X, Y), F, Z) =#> explode#(Y, /\x.op(F, F, x), F Z)   
    2] explode#(cons(X, Y), F, Z) =#> op#(F, F, U)   

  Rules R_0:

    op(F, G, X) => F (G X) 
    implode(nil, F, X) => X 
    implode(cons(X, Y), F, Z) => implode(Y, F, F Z) 
    explode(nil, F, X) => X 
    explode(cons(X, Y), F, Z) => explode(Y, /\x.op(F, F, x), F Z) 

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

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

This combination (P_0, R_0) has no formative rules!  We will name the empty set of rules:R_1.

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

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

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

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:

  implode#(cons(X, Y), F, Z) >? implode#(Y, F, F Z) 
  explode#(cons(X, Y), F, Z) >? explode#(Y, /\x.op(F, F, x), F Z) 
  explode#(cons(X, Y), F, Z) >? op#(F, F, U) 

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

The following interpretation satisfies the requirements:

  cons = \y0y1.3 + 2y1 
  explode# = \y0G1y2.3 + y0 
  implode# = \y0G1y2.y0 
  op = \G0G1y2.0 
  op# = \G0G1y2.0 

Using this interpretation, the requirements translate to:

  [[implode#(cons(_x0, _x1), _F2, _x3)]] = 3 + 2x1 > x1 = [[implode#(_x1, _F2, _F2 _x3)]] 
  [[explode#(cons(_x0, _x1), _F2, _x3)]] = 6 + 2x1 > 3 + x1 = [[explode#(_x1, /\x.op(_F2, _F2, x), _F2 _x3)]] 
  [[explode#(cons(_x0, _x1), _F2, _x3)]] = 6 + 2x1 > 0 = [[op#(_F2, _F2, _x4)]] 

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.
[Kop13]  C. Kop.  Static Dependency Pairs with Accessibility.  Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013.
[KusIsoSakBla09]  K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui.  Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems.  In volume 92(10) of IEICE Transactions on Information and Systems.  2007--2015, 2009.