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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 0 * 1 : 0 * 2 : 1, 2 * 3 : This graph has the following strongly connected components: P_1: plus#(s(X), Y) =#> plus#(X, Y) P_2: times#(s(X), Y) =#> times#(X, 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 [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]] = _|_ [[times#(x_1, x_2)]] = times#(x_1) We choose Lex = {} and Mul = {#argfun-comp#, #argfun-twice#, @_{o -> o}, comp, plus, s, times, times#, twice}, and the following precedence: times > twice > @_{o -> o} > #argfun-twice# > plus > s > times# > #argfun-comp# > comp Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times#(s(X)) > times#(X) 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)) > times#(X) because [2], by definition 2] times#*(s(X)) >= times#(X) because [3], by (Select) 3] s(X) >= times#(X) because [4], by (Star) 4] s*(X) >= times#(X) because s > times# and [5], by (Copy) 5] s*(X) >= X because [6], by (Select) 6] X >= X 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 [23], by (Copy) 20] times*(s(X), Y) >= times(X, Y) because times in Mul, [21] and [22], by (Stat) 21] s(X) > X because [5], by definition 22] Y >= Y by (Meta) 23] times*(s(X), Y) >= Y because [22], 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-twice#(#argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X)))) >= #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) because [32], by (Star) 32] #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# and [33], by (Copy) 33] #argfun-twice#*(#argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X)))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [34], by (Select) 34] #argfun-comp#(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [35], by (Star) 35] #argfun-comp#*(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [36], by (Select) 36] @_{o -> o}(F, @_{o -> o}(F, X)) >= @_{o -> o}(F, @_{o -> o}(F, X)) because @_{o -> o} in Mul, [37] and [38], by (Fun) 37] F >= F by (Meta) 38] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [37] and [39], by (Fun) 39] 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. 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) 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-comp#(x_1)]] = x_1 [[0]] = _|_ [[plus#(x_1, x_2)]] = plus#(x_2, x_1) We choose Lex = {plus#} and Mul = {#argfun-twice#, @_{o -> o}, comp, plus, s, times, twice}, and the following precedence: #argfun-twice# > @_{o -> o} > comp > plus# > times > plus > s > 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) plus(_|_, X) >= X plus(s(X), Y) >= s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) >= plus(times(X, Y), Y) @_{o -> o}(F, @_{o -> o}(G, X)) >= @_{o -> o}(F, @_{o -> o}(G, X)) #argfun-twice#(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{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 [3], [6], [7] and [9], 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#*(s(X), Y) >= X because [8], by (Select) 8] s(X) >= X because [4], by (Star) 9] plus#*(s(X), Y) >= Y because [6], by (Select) 10] plus(_|_, X) >= X because [11], by (Star) 11] plus*(_|_, X) >= X because [12], by (Select) 12] X >= X by (Meta) 13] plus(s(X), Y) >= s(plus(X, Y)) because [14], by (Star) 14] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [15], by (Copy) 15] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [3] and [6], by (Stat) 16] times(_|_, X) >= _|_ by (Bot) 17] times(s(X), Y) >= plus(times(X, Y), Y) because [18], by (Star) 18] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [19] and [24], by (Copy) 19] times*(s(X), Y) >= times(X, Y) because times in Mul, [20] and [23], by (Stat) 20] s(X) > X because [21], by definition 21] s*(X) >= X because [22], by (Select) 22] X >= X by (Meta) 23] Y >= Y by (Meta) 24] times*(s(X), Y) >= Y because [23], by (Select) 25] @_{o -> o}(F, @_{o -> o}(G, X)) >= @_{o -> o}(F, @_{o -> o}(G, X)) because @_{o -> o} in Mul, [26] and [27], by (Fun) 26] F >= F by (Meta) 27] @_{o -> o}(G, X) >= @_{o -> o}(G, X) because @_{o -> o} in Mul, [28] and [29], by (Fun) 28] G >= G by (Meta) 29] X >= X by (Meta) 30] #argfun-twice#(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [31], by (Star) 31] #argfun-twice#*(@_{o -> o}(F, @_{o -> o}(F, X))) >= @_{o -> o}(F, @_{o -> o}(F, X)) because [32], by (Select) 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 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.