We consider the system extrec. Alphabet: !plus : [nat * nat] --> nat !times : [nat * nat] --> nat 0 : [] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat Rules: !plus(x, 0) => x !plus(x, s(y)) => s(!plus(x, y)) rec(0, x, f) => x rec(s(x), y, f) => f x rec(x, y, f) !times(x, y) => rec(y, 0, /\z./\u.!plus(x, u)) 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] !plus#(X, s(Y)) =#> !plus#(X, Y) 1] rec#(s(X), Y, F) =#> rec#(X, Y, F) 2] !times#(X, Y) =#> rec#(Y, 0, /\x./\y.!plus(X, y)) 3] !times#(X, Y) =#> !plus#(X, Z) Rules R_0: !plus(X, 0) => X !plus(X, s(Y)) => s(!plus(X, Y)) rec(0, X, F) => X rec(s(X), Y, F) => F X rec(X, Y, F) !times(X, Y) => rec(Y, 0, /\x./\y.!plus(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: !plus#(X, s(Y)) >? !plus#(X, Y) rec#(s(X), Y, F) >? rec#(X, Y, F) !times#(X, Y) >? rec#(Y, 0, /\x./\y.!plus(X, y)) !times#(X, Y) >? !plus#(X, Z) !plus(X, 0) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(0, X, F) >= X rec(s(X), Y, F) >= F X rec(X, Y, F) !times(X, Y) >= rec(Y, 0, /\x./\y.!plus(X, y)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( !times(X, Y) ) = #argfun-!times#(rec(Y, 0, /\x./\y.!plus(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: [[!plus#(x_1, x_2)]] = !plus# [[!times#(x_1, x_2)]] = !times#(x_2) [[rec#(x_1, x_2, x_3)]] = rec#(x_1, x_2) We choose Lex = {} and Mul = {!plus, !plus#, !times, !times#, #argfun-!times#, 0, @_{o -> o -> o}, @_{o -> o}, rec, rec#, s}, and the following precedence: !times# > #argfun-!times# > 0 > !plus > !plus# > rec > s > @_{o -> o -> o} > !times > rec# > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: !plus# >= !plus# rec#(s(X), Y) >= rec#(X, Y) !times#(X) > rec#(X, 0) !times#(X) > !plus# !plus(X, 0) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(0, X, F) >= X rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) #argfun-!times#(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y)) With these choices, we have: 1] !plus# >= !plus# because !plus# in Mul, by (Fun) 2] rec#(s(X), Y) >= rec#(X, Y) because rec# in Mul, [3] and [6], by (Fun) 3] s(X) >= X because [4], by (Star) 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] Y >= Y by (Meta) 7] !times#(X) > rec#(X, 0) because [8], by definition 8] !times#*(X) >= rec#(X, 0) because !times# > rec#, [9] and [11], by (Copy) 9] !times#*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] !times#*(X) >= 0 because !times# > 0, by (Copy) 12] !times#(X) > !plus# because [13], by definition 13] !times#*(X) >= !plus# because !times# > !plus#, by (Copy) 14] !plus(X, 0) >= X because [15], by (Star) 15] !plus*(X, 0) >= X because [16], by (Select) 16] X >= X by (Meta) 17] !plus(X, s(Y)) >= s(!plus(X, Y)) because [18], by (Star) 18] !plus*(X, s(Y)) >= s(!plus(X, Y)) because !plus > s and [19], by (Copy) 19] !plus*(X, s(Y)) >= !plus(X, Y) because !plus in Mul, [20] and [21], by (Stat) 20] X >= X by (Meta) 21] s(Y) > Y because [22], by definition 22] s*(Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] rec(0, X, F) >= X because [25], by (Star) 25] rec*(0, X, F) >= X because [26], by (Select) 26] X >= X by (Meta) 27] rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because [28], by (Star) 28] rec*(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because rec > @_{o -> o}, [29] and [33], by (Copy) 29] rec*(s(X), Y, F) >= @_{o -> o -> o}(F, X) because rec > @_{o -> o -> o}, [30] and [32], by (Copy) 30] rec*(s(X), Y, F) >= F because [31], by (Select) 31] F >= F by (Meta) 32] rec*(s(X), Y, F) >= X because [3], by (Select) 33] rec*(s(X), Y, F) >= rec(X, Y, F) because rec in Mul, [34], [6] and [36], by (Stat) 34] s(X) > X because [35], by definition 35] s*(X) >= X because [5], by (Select) 36] F >= F by (Meta) 37] #argfun-!times#(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y)) because [38], by (Star) 38] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y))) >= rec(X, 0, /\x./\y.!plus(Y, y)) because #argfun-!times# > rec, [39], [42] and [43], by (Copy) 39] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y))) >= X because [40], by (Select) 40] rec(X, 0, /\x./\y.!plus(Y, y)) >= X because [41], by (Star) 41] rec*(X, 0, /\x./\y.!plus(Y, y)) >= X because [10], by (Select) 42] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y))) >= 0 because #argfun-!times# > 0, by (Copy) 43] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y))) >= /\x./\y.!plus(Y, y) because [44], by (F-Abs) 44] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y)), z) >= /\x.!plus(Y, x) because [45], by (F-Abs) 45] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y)), z, u) >= !plus(Y, u) because #argfun-!times# > !plus, [46] and [55], by (Copy) 46] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y)), z, u) >= Y because [47], by (Select) 47] rec(X, 0, /\x./\y.!plus(Y, y)) >= Y because [48], by (Star) 48] rec*(X, 0, /\x./\y.!plus(Y, y)) >= Y because [49], by (Select) 49] !plus(Y, rec*(X, 0, /\x./\y.!plus(Y, y))) >= Y because [50], by (Star) 50] !plus*(Y, rec*(X, 0, /\x./\y.!plus(Y, y))) >= Y because [51], by (Select) 51] rec*(X, 0, /\x./\y.!plus(Y, y)) >= Y because [52], by (Select) 52] !plus(Y, rec*(X, 0, /\x./\y.!plus(Y, y))) >= Y because [53], by (Star) 53] !plus*(Y, rec*(X, 0, /\x./\y.!plus(Y, y))) >= Y because [54], by (Select) 54] Y >= Y by (Meta) 55] #argfun-!times#*(rec(X, 0, /\x./\y.!plus(Y, y)), z, u) >= u because [56], by (Select) 56] u >= u by (Var) 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#(X, s(Y)) =#> !plus#(X, Y) rec#(s(X), Y, F) =#> rec#(X, Y, F) 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#(X, s(Y)) >? !plus#(X, Y) rec#(s(X), Y, F) >? rec#(X, Y, F) !plus(X, 0) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(0, X, F) >= X rec(s(X), Y, F) >= F X rec(X, Y, F) !times(X, Y) >= rec(Y, 0, /\x./\y.!plus(X, y)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( !times(X, Y) ) = #argfun-!times#(rec(Y, 0, /\x./\y.!plus(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: [[!plus#(x_1, x_2)]] = x_2 [[0]] = _|_ [[rec#(x_1, x_2, x_3)]] = rec#(x_3, x_1, x_2) We choose Lex = {rec#} and Mul = {!plus, !times, #argfun-!times#, @_{o -> o -> o}, @_{o -> o}, rec, s}, and the following precedence: !times > #argfun-!times# > !plus > rec > @_{o -> o -> o} > @_{o -> o} > rec# > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: s(X) > X rec#(s(X), Y, F) >= rec#(X, Y, F) !plus(X, _|_) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(_|_, X, F) >= X rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) With these choices, we have: 1] s(X) > X because [2], by definition 2] s*(X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] rec#(s(X), Y, F) >= rec#(X, Y, F) because [5], [8] and [9], by (Fun) 5] s(X) >= X because [6], by (Star) 6] s*(X) >= X because [7], by (Select) 7] X >= X by (Meta) 8] Y >= Y by (Meta) 9] F >= F by (Meta) 10] !plus(X, _|_) >= X because [11], by (Star) 11] !plus*(X, _|_) >= X because [12], by (Select) 12] X >= X by (Meta) 13] !plus(X, s(Y)) >= s(!plus(X, Y)) because [14], by (Star) 14] !plus*(X, s(Y)) >= s(!plus(X, Y)) because !plus > s and [15], by (Copy) 15] !plus*(X, s(Y)) >= !plus(X, Y) because !plus in Mul, [16] and [17], by (Stat) 16] X >= X by (Meta) 17] s(Y) > Y because [2], by definition 18] rec(_|_, X, F) >= X because [19], by (Star) 19] rec*(_|_, X, F) >= X because [20], by (Select) 20] X >= X by (Meta) 21] rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because [22], by (Star) 22] rec*(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because rec > @_{o -> o}, [23] and [26], by (Copy) 23] rec*(s(X), Y, F) >= @_{o -> o -> o}(F, X) because rec > @_{o -> o -> o}, [24] and [25], by (Copy) 24] rec*(s(X), Y, F) >= F because [9], by (Select) 25] rec*(s(X), Y, F) >= X because [5], by (Select) 26] rec*(s(X), Y, F) >= rec(X, Y, F) because rec in Mul, [27], [8] and [9], by (Stat) 27] s(X) > X because [28], by definition 28] s*(X) >= X because [7], by (Select) 29] #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) because [30], by (Star) 30] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) because #argfun-!times# > rec, [31], [35] and [36], by (Copy) 31] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= X because [32], by (Select) 32] rec(X, _|_, /\x./\y.!plus(Y, y)) >= X because [33], by (Star) 33] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= X because [34], by (Select) 34] X >= X by (Meta) 35] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= _|_ by (Bot) 36] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= /\x./\y.!plus(Y, y) because [37], by (F-Abs) 37] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z) >= /\x.!plus(Y, x) because [38], by (F-Abs) 38] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= !plus(Y, u) because #argfun-!times# > !plus, [39] and [45], by (Copy) 39] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= Y because [40], by (Select) 40] rec(X, _|_, /\x./\y.!plus(Y, y)) >= Y because [41], by (Star) 41] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= Y because [42], by (Select) 42] !plus(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y because [43], by (Star) 43] !plus*(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y because [44], by (Select) 44] Y >= Y by (Meta) 45] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= u because [46], by (Select) 46] u >= u by (Var) 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: rec#(s(X), Y, F) =#> rec#(X, Y, F) 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: rec#(s(X), Y, F) >? rec#(X, Y, F) !plus(X, 0) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(0, X, F) >= X rec(s(X), Y, F) >= F X rec(X, Y, F) !times(X, Y) >= rec(Y, 0, /\x./\y.!plus(X, y)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( !times(X, Y) ) = #argfun-!times#(rec(Y, 0, /\x./\y.!plus(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: [[0]] = _|_ [[rec#(x_1, x_2, x_3)]] = rec#(x_1, x_3, x_2) We choose Lex = {rec#} and Mul = {!plus, !times, #argfun-!times#, @_{o -> o -> o}, @_{o -> o}, rec, s}, and the following precedence: !times > #argfun-!times# > !plus > rec > @_{o -> o -> o} > @_{o -> o} > rec# > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: rec#(s(X), Y, F) > rec#(X, Y, F) !plus(X, _|_) >= X !plus(X, s(Y)) >= s(!plus(X, Y)) rec(_|_, X, F) >= X rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) With these choices, we have: 1] rec#(s(X), Y, F) > rec#(X, Y, F) because [2], by definition 2] rec#*(s(X), Y, F) >= rec#(X, Y, F) because [3], [6], [8] and [10], by (Stat) 3] s(X) > X because [4], by definition 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] rec#*(s(X), Y, F) >= X because [7], by (Select) 7] s(X) >= X because [4], by (Star) 8] rec#*(s(X), Y, F) >= Y because [9], by (Select) 9] Y >= Y by (Meta) 10] rec#*(s(X), Y, F) >= F because [11], by (Select) 11] F >= F by (Meta) 12] !plus(X, _|_) >= X because [13], by (Star) 13] !plus*(X, _|_) >= X because [14], by (Select) 14] X >= X by (Meta) 15] !plus(X, s(Y)) >= s(!plus(X, Y)) because [16], by (Star) 16] !plus*(X, s(Y)) >= s(!plus(X, Y)) because !plus > s and [17], by (Copy) 17] !plus*(X, s(Y)) >= !plus(X, Y) because !plus in Mul, [18] and [19], by (Stat) 18] X >= X by (Meta) 19] s(Y) > Y because [20], by definition 20] s*(Y) >= Y because [21], by (Select) 21] Y >= Y by (Meta) 22] rec(_|_, X, F) >= X because [23], by (Star) 23] rec*(_|_, X, F) >= X because [24], by (Select) 24] X >= X by (Meta) 25] rec(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because [26], by (Star) 26] rec*(s(X), Y, F) >= @_{o -> o}(@_{o -> o -> o}(F, X), rec(X, Y, F)) because rec > @_{o -> o}, [27] and [30], by (Copy) 27] rec*(s(X), Y, F) >= @_{o -> o -> o}(F, X) because rec > @_{o -> o -> o}, [28] and [29], by (Copy) 28] rec*(s(X), Y, F) >= F because [11], by (Select) 29] rec*(s(X), Y, F) >= X because [7], by (Select) 30] rec*(s(X), Y, F) >= rec(X, Y, F) because rec in Mul, [3], [31] and [32], by (Stat) 31] Y >= Y by (Meta) 32] F >= F by (Meta) 33] #argfun-!times#(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) because [34], by (Star) 34] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= rec(X, _|_, /\x./\y.!plus(Y, y)) because #argfun-!times# > rec, [35], [39] and [40], by (Copy) 35] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= X because [36], by (Select) 36] rec(X, _|_, /\x./\y.!plus(Y, y)) >= X because [37], by (Star) 37] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= X because [38], by (Select) 38] X >= X by (Meta) 39] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= _|_ by (Bot) 40] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y))) >= /\x./\y.!plus(Y, y) because [41], by (F-Abs) 41] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z) >= /\x.!plus(Y, x) because [42], by (F-Abs) 42] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= !plus(Y, u) because #argfun-!times# > !plus, [43] and [49], by (Copy) 43] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= Y because [44], by (Select) 44] rec(X, _|_, /\x./\y.!plus(Y, y)) >= Y because [45], by (Star) 45] rec*(X, _|_, /\x./\y.!plus(Y, y)) >= Y because [46], by (Select) 46] !plus(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y because [47], by (Star) 47] !plus*(Y, rec*(X, _|_, /\x./\y.!plus(Y, y))) >= Y because [48], by (Select) 48] Y >= Y by (Meta) 49] #argfun-!times#*(rec(X, _|_, /\x./\y.!plus(Y, y)), z, u) >= u because [50], by (Select) 50] u >= u by (Var) 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.