We consider the system AotoYamada_05__020. Alphabet: 0 : [] --> a comp : [b -> b * b -> b] --> b -> b plus : [a * a] --> a s : [a] --> a times : [a * a] --> a twice : [b -> b] --> b -> b Rules: plus(0, x) => x plus(s(x), y) => s(plus(x, y)) times(0, x) => 0 times(s(x), y) => plus(times(x, y), y) comp(f, g) x => f (g x) twice(f) => comp(f, f) 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: plus(0, X) => X plus(s(X), Y) => s(plus(X, Y)) times(0, X) => 0 times(s(X), Y) => plus(times(X, Y), Y) comp(F, G, X) => F (G X) twice(F, X) => comp(F, F, X) We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] plus#(s(X), Y) =#> plus#(X, Y) 1] times#(s(X), Y) =#> plus#(times(X, Y), Y) 2] times#(s(X), Y) =#> times#(X, Y) 3] twice#(F, X) =#> comp#(F, F, X) Rules R_0: plus(0, X) => X plus(s(X), Y) => s(plus(X, Y)) times(0, X) => 0 times(s(X), Y) => plus(times(X, Y), Y) comp(F, G, X) => F (G X) twice(F, X) => comp(F, F, X) 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: plus#(s(X), Y) >? plus#(X, Y) times#(s(X), Y) >? plus#(times(X, Y), Y) times#(s(X), Y) >? times#(X, Y) twice#(F, X) >? comp#(F, F, X) plus(0, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(0, X) >= 0 times(s(X), Y) >= plus(times(X, Y), Y) comp(F, G, X) >= F (G X) twice(F, X) >= comp(F, F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( comp(F, G, X) ) = #argfun-comp#(F (G X)) pi( twice(F, X) ) = #argfun-twice#(#argfun-comp#(F (F X))) pi( twice#(F, X) ) = #argfun-twice##(comp#(F, F, X)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-comp# = \y0.3 + y0 #argfun-twice# = \y0.3 + y0 #argfun-twice## = \y0.3 + y0 0 = 0 comp = \G0G1y2.0 comp# = \G0G1y2.0 plus = \y0y1.2y1 plus# = \y0y1.0 s = \y0.0 times = \y0y1.2y1 times# = \y0y1.3 + 2y1 twice = \G0y1.0 twice# = \G0y1.0 Using this interpretation, the requirements translate to: [[plus#(s(_x0), _x1)]] = 0 >= 0 = [[plus#(_x0, _x1)]] [[times#(s(_x0), _x1)]] = 3 + 2x1 > 0 = [[plus#(times(_x0, _x1), _x1)]] [[times#(s(_x0), _x1)]] = 3 + 2x1 >= 3 + 2x1 = [[times#(_x0, _x1)]] [[#argfun-twice##(comp#(_F0, _F0, _x1))]] = 3 > 0 = [[comp#(_F0, _F0, _x1)]] [[plus(0, _x0)]] = 2x0 >= x0 = [[_x0]] [[plus(s(_x0), _x1)]] = 2x1 >= 0 = [[s(plus(_x0, _x1))]] [[times(0, _x0)]] = 2x0 >= 0 = [[0]] [[times(s(_x0), _x1)]] = 2x1 >= 2x1 = [[plus(times(_x0, _x1), _x1)]] [[#argfun-comp#(_F0 (_F1 _x2))]] = 3 + F0(F1(x2)) >= F0(F1(x2)) = [[_F0 (_F1 _x2)]] [[#argfun-twice#(#argfun-comp#(_F0 (_F0 _x1)))]] = 6 + F0(F0(x1)) >= 3 + F0(F0(x1)) = [[#argfun-comp#(_F0 (_F0 _x1))]] 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: plus#(s(X), Y) =#> plus#(X, Y) times#(s(X), Y) =#> times#(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: plus#(s(X), Y) >? plus#(X, Y) times#(s(X), Y) >? times#(X, Y) plus(0, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(0, X) >= 0 times(s(X), Y) >= plus(times(X, Y), Y) comp(F, G, X) >= F (G X) twice(F, X) >= comp(F, F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( comp(F, G, X) ) = #argfun-comp#(F (G X)) pi( twice(F, X) ) = #argfun-twice#(#argfun-comp#(F (F X))) 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: [[#argfun-twice#(x_1)]] = x_1 [[0]] = _|_ We choose Lex = {} and Mul = {#argfun-comp#, @_{o -> o}, comp, plus, plus#, s, times, times#, twice}, and the following precedence: comp > @_{o -> o} > plus# > times > #argfun-comp# > plus > s > times# > twice Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: plus#(s(X), Y) > plus#(X, Y) times#(s(X), Y) >= times#(X, Y) plus(_|_, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) >= plus(times(X, Y), Y) #argfun-comp#(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) With these choices, we have: 1] plus#(s(X), Y) > plus#(X, Y) because [2], by definition 2] plus#*(s(X), Y) >= plus#(X, Y) because plus# in Mul, [3] and [6], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] Y >= Y by (Meta) 7] times#(s(X), Y) >= times#(X, Y) because [8], by (Star) 8] times#*(s(X), Y) >= times#(X, Y) because times# in Mul, [9] and [12], by (Stat) 9] s(X) > X because [10], by definition 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] Y >= Y by (Meta) 13] plus(_|_, X) >= X because [14], by (Star) 14] plus*(_|_, X) >= X because [15], by (Select) 15] X >= X by (Meta) 16] plus(s(X), Y) >= s(plus(X, Y)) because [17], by (Star) 17] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [18], by (Copy) 18] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [3] and [6], by (Stat) 19] times(_|_, X) >= _|_ by (Bot) 20] times(s(X), Y) >= plus(times(X, Y), Y) because [21], by (Star) 21] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [22] and [23], by (Copy) 22] times*(s(X), Y) >= times(X, Y) because times in Mul, [9] and [12], by (Stat) 23] times*(s(X), Y) >= Y because [12], by (Select) 24] #argfun-comp#(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) because [25], by (Star) 25] #argfun-comp#*(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) because [26], by (Select) 26] @_{o -> o}(F, @_{o -> o}(G, X)) >= @_{o -> o}(F, @_{o -> o}(G, X)) because @_{o -> o} in Mul, [27] and [28], by (Fun) 27] F >= F by (Meta) 28] @_{o -> o}(G, X) >= @_{o -> o}(G, X) because @_{o -> o} in Mul, [29] and [30], by (Fun) 29] G >= G by (Meta) 30] X >= X by (Meta) 31] #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) because #argfun-comp# in Mul and [32], by (Fun) 32] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X)) because @_{o -> o} in Mul, [33] and [34], by (Fun) 33] F >= F by (Meta) 34] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [33] and [35], by (Fun) 35] X >= X by (Meta) 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: times#(s(X), Y) =#> times#(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: times#(s(X), Y) >? times#(X, Y) plus(0, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(0, X) >= 0 times(s(X), Y) >= plus(times(X, Y), Y) comp(F, G, X) >= F (G X) twice(F, X) >= comp(F, F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( comp(F, G, X) ) = #argfun-comp#(F (G X)) pi( twice(F, X) ) = #argfun-twice#(#argfun-comp#(F (F X))) 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: [[0]] = _|_ We choose Lex = {} and Mul = {#argfun-comp#, #argfun-twice#, @_{o -> o}, comp, plus, s, times, times#, twice}, and the following precedence: #argfun-comp# = #argfun-twice# > @_{o -> o} > comp > times > plus > s > times# > twice Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times#(s(X), Y) > times#(X, Y) plus(_|_, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) >= plus(times(X, Y), Y) #argfun-comp#(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) #argfun-twice#(#argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X)))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) With these choices, we have: 1] times#(s(X), Y) > times#(X, Y) because [2], by definition 2] times#*(s(X), Y) >= times#(X, Y) because times# in Mul, [3] and [6], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] Y >= Y by (Meta) 7] plus(_|_, X) >= X because [8], by (Star) 8] plus*(_|_, X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] plus(s(X), Y) >= s(plus(X, Y)) because [11], by (Star) 11] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [12], by (Copy) 12] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [13] and [16], by (Stat) 13] s(X) > X because [14], by definition 14] s*(X) >= X because [15], by (Select) 15] X >= X by (Meta) 16] Y >= Y by (Meta) 17] times(_|_, X) >= _|_ by (Bot) 18] times(s(X), Y) >= plus(times(X, Y), Y) because [19], by (Star) 19] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [20] and [21], by (Copy) 20] times*(s(X), Y) >= times(X, Y) because times in Mul, [3] and [6], by (Stat) 21] times*(s(X), Y) >= Y because [6], by (Select) 22] #argfun-comp#(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) because [23], by (Star) 23] #argfun-comp#*(@_{o -> o}(F, @_{o -> o}(G, X))) >= @_{o -> o}(F, @_{o -> o}(G, X)) because [24], by (Select) 24] @_{o -> o}(F, @_{o -> o}(G, X)) >= @_{o -> o}(F, @_{o -> o}(G, X)) because @_{o -> o} in Mul, [25] and [26], by (Fun) 25] F >= F by (Meta) 26] @_{o -> o}(G, X) >= @_{o -> o}(G, X) because @_{o -> o} in Mul, [27] and [28], by (Fun) 27] G >= G by (Meta) 28] X >= X by (Meta) 29] #argfun-twice#(#argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X)))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) because [30], by (Star) 30] #argfun-twice#*(#argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X)))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) because #argfun-twice# = #argfun-comp#, #argfun-twice# in Mul and [31], by (Stat) 31] #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) > @_{o -> o}(F, @_{o -> o}(F, X)) because [32], by definition 32] #argfun-comp#*(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [33], by (Select) 33] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X)) because @_{o -> o} in Mul, [34] and [35], by (Fun) 34] F >= F by (Meta) 35] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [34] and [36], by (Fun) 36] X >= X by (Meta) 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.