We consider the system 02Ackermann.

  Alphabet:

    ack : [N * N] --> N 
    s : [N] --> N 
    z : [] --> N 

  Rules:

    ack(z, x) => s(x) 
    ack(s(x), z) => ack(x, s(z)) 
    ack(s(x), s(y)) => ack(x, ack(s(x), 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]).

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

  Dependency Pairs P_0:

    0] ack#(s(X), z) =#> ack#(X, s(z))   
    1] ack#(s(X), s(Y)) =#> ack#(X, ack(s(X), Y))   
    2] ack#(s(X), s(Y)) =#> ack#(s(X), Y)   

  Rules R_0:

    ack(z, X) => s(X) 
    ack(s(X), z) => ack(X, s(z)) 
    ack(s(X), s(Y)) => ack(X, ack(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 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:

  ack#(s(X), z) >? ack#(X, s(z)) 
  ack#(s(X), s(Y)) >? ack#(X, ack(s(X), Y)) 
  ack#(s(X), s(Y)) >? ack#(s(X), Y) 
  ack(z, X) >= s(X) 
  ack(s(X), z) >= ack(X, s(z)) 
  ack(s(X), s(Y)) >= ack(X, ack(s(X), Y)) 

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

We choose Lex = {ack, ack#} and Mul = {s, z}, and the following precedence: ack = ack# > s > z

With these choices, we have:

  1] ack#(s(X), z) > ack#(X, s(z))  because [2], by definition 
  2] ack#*(s(X), z) >= ack#(X, s(z))  because [3], [6] and [8], by (Stat) 
  3] s(X) > X  because [4], by definition 
  4] s*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] ack#*(s(X), z) >= X  because [7], by (Select) 
  7] s(X) >= X  because [4], by (Star) 
  8] ack#*(s(X), z) >= s(z)  because ack# > s and [9], by (Copy) 
  9] ack#*(s(X), z) >= z  because ack# > z, by (Copy) 

  10] ack#(s(X), s(Y)) >= ack#(X, ack(s(X), Y))  because [11], by (Star) 
  11] ack#*(s(X), s(Y)) >= ack#(X, ack(s(X), Y))  because [12], [15] and [17], by (Stat) 
  12] s(X) > X  because [13], by definition 
  13] s*(X) >= X  because [14], by (Select) 
  14] X >= X  by (Meta) 
  15] ack#*(s(X), s(Y)) >= X  because [16], by (Select) 
  16] s(X) >= X  because [13], by (Star) 
  17] ack#*(s(X), s(Y)) >= ack(s(X), Y)  because ack# = ack, [18], [20], [23] and [24], by (Stat) 
  18] s(X) >= s(X)  because s in Mul and [19], by (Fun) 
  19] X >= X  by (Meta) 
  20] s(Y) > Y  because [21], by definition 
  21] s*(Y) >= Y  because [22], by (Select) 
  22] Y >= Y  by (Meta) 
  23] ack#*(s(X), s(Y)) >= s(X)  because ack# > s and [15], by (Copy) 
  24] ack#*(s(X), s(Y)) >= Y  because [25], by (Select) 
  25] s(Y) >= Y  because [21], by (Star) 

  26] ack#(s(X), s(Y)) >= ack#(s(X), Y)  because [18] and [27], by (Fun) 
  27] s(Y) >= Y  because [21], by (Star) 

  28] ack(z, X) >= s(X)  because [29], by (Star) 
  29] ack*(z, X) >= s(X)  because ack > s and [30], by (Copy) 
  30] ack*(z, X) >= X  because [31], by (Select) 
  31] X >= X  by (Meta) 

  32] ack(s(X), z) >= ack(X, s(z))  because [33], by (Star) 
  33] ack*(s(X), z) >= ack(X, s(z))  because [3], [34] and [35], by (Stat) 
  34] ack*(s(X), z) >= X  because [7], by (Select) 
  35] ack*(s(X), z) >= s(z)  because ack > s and [36], by (Copy) 
  36] ack*(s(X), z) >= z  because ack > z, by (Copy) 

  37] ack(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [38], by (Star) 
  38] ack*(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [12], [39] and [40], by (Stat) 
  39] ack*(s(X), s(Y)) >= X  because [16], by (Select) 
  40] ack*(s(X), s(Y)) >= ack(s(X), Y)  because [18], [20], [41] and [42], by (Stat) 
  41] ack*(s(X), s(Y)) >= s(X)  because ack > s and [39], by (Copy) 
  42] ack*(s(X), s(Y)) >= Y  because [27], by (Select) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, static, formative) by (P_1, R_0, static, formative), where P_1 consists of:

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

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 [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  ack#(s(X), s(Y)) >? ack#(X, ack(s(X), Y)) 
  ack#(s(X), s(Y)) >? ack#(s(X), Y) 
  ack(z, X) >= s(X) 
  ack(s(X), z) >= ack(X, s(z)) 
  ack(s(X), s(Y)) >= ack(X, ack(s(X), Y)) 

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

We choose Lex = {ack, ack#} and Mul = {s, z}, and the following precedence: ack# > ack > s > z

With these choices, we have:

  1] ack#(s(X), s(Y)) >= ack#(X, ack(s(X), Y))  because [2], by (Star) 
  2] ack#*(s(X), s(Y)) >= ack#(X, ack(s(X), Y))  because [3], [6] and [8], by (Stat) 
  3] s(X) > X  because [4], by definition 
  4] s*(X) >= X  because [5], by (Select) 
  5] X >= X  by (Meta) 
  6] ack#*(s(X), s(Y)) >= X  because [7], by (Select) 
  7] s(X) >= X  because [4], by (Star) 
  8] ack#*(s(X), s(Y)) >= ack(s(X), Y)  because ack# > ack, [9] and [10], by (Copy) 
  9] ack#*(s(X), s(Y)) >= s(X)  because ack# > s and [6], by (Copy) 
  10] ack#*(s(X), s(Y)) >= Y  because [11], by (Select) 
  11] s(Y) >= Y  because [12], by (Star) 
  12] s*(Y) >= Y  because [13], by (Select) 
  13] Y >= Y  by (Meta) 

  14] ack#(s(X), s(Y)) > ack#(s(X), Y)  because [15], by definition 
  15] ack#*(s(X), s(Y)) >= ack#(s(X), Y)  because [16], [18], [9] and [10], by (Stat) 
  16] s(X) >= s(X)  because s in Mul and [17], by (Fun) 
  17] X >= X  by (Meta) 
  18] s(Y) > Y  because [19], by definition 
  19] s*(Y) >= Y  because [13], by (Select) 

  20] ack(z, X) >= s(X)  because [21], by (Star) 
  21] ack*(z, X) >= s(X)  because ack > s and [22], by (Copy) 
  22] ack*(z, X) >= X  because [23], by (Select) 
  23] X >= X  by (Meta) 

  24] ack(s(X), z) >= ack(X, s(z))  because [25], by (Star) 
  25] ack*(s(X), z) >= ack(X, s(z))  because [26], [29] and [31], by (Stat) 
  26] s(X) > X  because [27], by definition 
  27] s*(X) >= X  because [28], by (Select) 
  28] X >= X  by (Meta) 
  29] ack*(s(X), z) >= X  because [30], by (Select) 
  30] s(X) >= X  because [27], by (Star) 
  31] ack*(s(X), z) >= s(z)  because ack > s and [32], by (Copy) 
  32] ack*(s(X), z) >= z  because ack > z, by (Copy) 

  33] ack(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [34], by (Star) 
  34] ack*(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [3], [35] and [36], by (Stat) 
  35] ack*(s(X), s(Y)) >= X  because [7], by (Select) 
  36] ack*(s(X), s(Y)) >= ack(s(X), Y)  because [16], [18], [37] and [38], by (Stat) 
  37] ack*(s(X), s(Y)) >= s(X)  because [16], by (Select) 
  38] ack*(s(X), s(Y)) >= Y  because [11], by (Select) 

By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, static, formative) by (P_2, R_0, static, formative), where P_2 consists of:

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

Thus, the original system is terminating if (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 [Kop12, Thm. 7.16].  It suffices to find a standard reduction pair [Kop12, Def. 6.69].  Thus, we must orient:

  ack#(s(X), s(Y)) >? ack#(X, ack(s(X), Y)) 
  ack(z, X) >= s(X) 
  ack(s(X), z) >= ack(X, s(z)) 
  ack(s(X), s(Y)) >= ack(X, ack(s(X), Y)) 

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:

  [[ack#(x_1, x_2)]] = ack#(x_1) 

We choose Lex = {ack} and Mul = {ack#, s, z}, and the following precedence: ack > s > ack# > z

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

  ack#(s(X)) > ack#(X) 
  ack(z, X) >= s(X) 
  ack(s(X), z) >= ack(X, s(z)) 
  ack(s(X), s(Y)) >= ack(X, ack(s(X), Y)) 

With these choices, we have:

  1] ack#(s(X)) > ack#(X)  because [2], by definition 
  2] ack#*(s(X)) >= ack#(X)  because [3], by (Select) 
  3] s(X) >= ack#(X)  because [4], by (Star) 
  4] s*(X) >= ack#(X)  because s > ack# and [5], by (Copy) 
  5] s*(X) >= X  because [6], by (Select) 
  6] X >= X  by (Meta) 

  7] ack(z, X) >= s(X)  because [8], by (Star) 
  8] ack*(z, X) >= s(X)  because ack > s and [9], by (Copy) 
  9] ack*(z, X) >= X  because [10], by (Select) 
  10] X >= X  by (Meta) 

  11] ack(s(X), z) >= ack(X, s(z))  because [12], by (Star) 
  12] ack*(s(X), z) >= ack(X, s(z))  because [13], [16] and [18], by (Stat) 
  13] s(X) > X  because [14], by definition 
  14] s*(X) >= X  because [15], by (Select) 
  15] X >= X  by (Meta) 
  16] ack*(s(X), z) >= X  because [17], by (Select) 
  17] s(X) >= X  because [14], by (Star) 
  18] ack*(s(X), z) >= s(z)  because ack > s and [19], by (Copy) 
  19] ack*(s(X), z) >= z  because ack > z, by (Copy) 

  20] ack(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [21], by (Star) 
  21] ack*(s(X), s(Y)) >= ack(X, ack(s(X), Y))  because [22], [23] and [25], by (Stat) 
  22] s(X) > X  because [5], by definition 
  23] ack*(s(X), s(Y)) >= X  because [24], by (Select) 
  24] s(X) >= X  because [5], by (Star) 
  25] ack*(s(X), s(Y)) >= ack(s(X), Y)  because [26], [28], [31] and [32], by (Stat) 
  26] s(X) >= s(X)  because s in Mul and [27], by (Fun) 
  27] X >= X  by (Meta) 
  28] s(Y) > Y  because [29], by definition 
  29] s*(Y) >= Y  because [30], by (Select) 
  30] Y >= Y  by (Meta) 
  31] ack*(s(X), s(Y)) >= s(X)  because [26], by (Select) 
  32] ack*(s(X), s(Y)) >= Y  because [33], by (Select) 
  33] s(Y) >= Y  because [29], by (Star) 

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.

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.