We consider the system onearg.

  Alphabet:

    0 : [] --> nat 
    add : [nat] --> nat -> nat 
    eq : [nat] --> nat -> bool 
    err : [] --> nat 
    false : [] --> bool 
    id : [] --> nat -> nat 
    nul : [] --> nat -> bool 
    pred : [nat] --> nat 
    s : [nat] --> nat 
    true : [] --> bool 

  Rules:

    nul 0 => true 
    nul s(x) => false 
    nul err => false 
    pred(0) => err 
    pred(s(x)) => x 
    id x => x 
    eq(0) => nul 
    eq(s(x)) => /\y.eq(x) pred(y) 
    add(0) => id 
    add(s(x)) => /\y.add(x) s(y) 

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:

  nul(0) => true 
  nul(s(X)) => false 
  nul(err) => false 
  pred(0) => err 
  pred(s(X)) => X 
  id(X) => X 
  eq(0, X) => nul(X) 
  eq(s(X), Y) => (/\x.eq(X, pred(x))) Y 
  add(0, X) => id(X) 
  add(s(X), Y) => (/\x.add(X, s(x))) Y 

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

  Dependency Pairs P_0:

    0] eq#(0, X) =#> nul#(X)   
    1] eq#(s(X), Y) =#> eq#(X, pred(Y))   
    2] eq#(s(X), Y) =#> pred#(Y)   
    3] add#(0, X) =#> id#(X)   
    4] add#(s(X), Y) =#> add#(X, s(Y))   

  Rules R_0:

    nul(0) => true 
    nul(s(X)) => false 
    nul(err) => false 
    pred(0) => err 
    pred(s(X)) => X 
    id(X) => X 
    eq(0, X) => nul(X) 
    eq(s(X), Y) => (/\x.eq(X, pred(x))) Y 
    add(0, X) => id(X) 
    add(s(X), Y) => (/\x.add(X, s(x))) Y 

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

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

    * 0 :  
    * 1 : 0, 1, 2 
    * 2 :  
    * 3 :  
    * 4 : 3, 4 

This graph has the following strongly connected components:

  P_1:

    eq#(s(X), Y) =#> eq#(X, pred(Y))   

  P_2:

    add#(s(X), Y) =#> add#(X, s(Y))   

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) and (P_2, R_0, m, f).

Thus, the original system is terminating if each of (P_1, R_0, static, formative) and (P_2, R_0, static, formative) is finite.

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

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  (P_2, R_0) has no usable rules.

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  add#(s(X), Y) >? add#(X, s(Y)) 

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

The following interpretation satisfies the requirements:

  add# = \y0y1.3y0 
  s = \y0.3 + 3y0 

Using this interpretation, the requirements translate to:

  [[add#(s(_x0), _x1)]] = 9 + 9x0 > 3x0 = [[add#(_x0, s(_x1))]] 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_0) by ({}, R_0).  By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed.

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

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

We will use the reduction pair processor with usable rules [Kop12, Thm. 7.44].  The usable rules of (P_1, R_0) are:

  pred(0) => err 
  pred(s(X)) => X 

It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  eq#(s(X), Y) >? eq#(X, pred(Y)) 
  pred(0) >= err 
  pred(s(X)) >= X 

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

The following interpretation satisfies the requirements:

  0 = 3 
  eq# = \y0y1.y0 
  err = 0 
  pred = \y0.y0 
  s = \y0.3 + 3y0 

Using this interpretation, the requirements translate to:

  [[eq#(s(_x0), _x1)]] = 3 + 3x0 > x0 = [[eq#(_x0, pred(_x1))]] 
  [[pred(0)]] = 3 >= 0 = [[err]] 
  [[pred(s(_x0))]] = 3 + 3x0 >= x0 = [[_x0]] 

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 +++

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