We consider the system Applicative_05__Ex6Folding. Alphabet: 0 : [] --> c 1 : [] --> c add : [] --> c -> a -> c cons : [a * b] --> b fold : [c -> a -> c * b * c] --> c mul : [] --> c -> a -> c nil : [] --> b prod : [b] --> c sum : [b] --> c Rules: fold(f, nil, x) => x fold(f, cons(x, y), z) => fold(f, y, f z x) sum(x) => fold(add, x, 0) fold(mul, x, 1) => prod(x) 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: fold(F, nil, X) => X fold(F, cons(X, Y), Z) => fold(F, Y, F Z X) sum(X) => fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) => prod(X) We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] fold#(F, cons(X, Y), Z) =#> fold#(F, Y, F Z X) 1] sum#(X) =#> fold#(/\x./\y.add(x, y), X, 0) Rules R_0: fold(F, nil, X) => X fold(F, cons(X, Y), Z) => fold(F, Y, F Z X) sum(X) => fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) => prod(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: fold#(F, cons(X, Y), Z) >? fold#(F, Y, F Z X) sum#(X) >? fold#(/\x./\y.add(x, y), X, 0) fold(F, nil, X) >= X fold(F, cons(X, Y), Z) >= fold(F, Y, F Z X) sum(X) >= fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) >= prod(X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( sum(X) ) = #argfun-sum#(fold(/\x./\y.add(x, y), X, 0)) pi( sum#(X) ) = #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) 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-sum#(x_1)]] = x_1 [[fold#(x_1, x_2, x_3)]] = fold#(x_2) We choose Lex = {#argfun-sum##, fold, fold#} and Mul = {0, 1, @_{o -> o -> o}, @_{o -> o}, add, cons, mul, nil, prod, sum, sum#}, and the following precedence: 1 > nil > sum# > #argfun-sum## = fold# > mul = prod > add > fold > @_{o -> o -> o} > 0 > sum > cons > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold#(F, cons(X, Y), Z) > fold#(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) >= fold#(/\x./\y.add(x, y), X, 0) fold(F, nil, X) >= X fold(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) fold(/\x./\y.add(x, y), X, 0) >= fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) >= prod(X) With these choices, we have: 1] fold#(F, cons(X, Y), Z) > fold#(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [2], by definition 2] fold#*(F, cons(X, Y), Z) >= fold#(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [3] and [6], by (Stat) 3] cons(X, Y) > Y because [4], by definition 4] cons*(X, Y) >= Y because [5], by (Select) 5] Y >= Y by (Meta) 6] fold#*(F, cons(X, Y), Z) >= Y because [7], by (Select) 7] cons(X, Y) >= Y because [4], by (Star) 8] #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) >= fold#(/\x./\y.add(x, y), X, 0) because #argfun-sum## = fold# and [9], by (Fun) 9] fold#(/\x./\y.add(x, y), X, 0) >= X because [10], by (Star) 10] fold#*(/\x./\y.add(x, y), X, 0) >= X because [11], by (Select) 11] X >= X by (Meta) 12] fold(F, nil, X) >= X because [13], by (Star) 13] fold*(F, nil, X) >= X because [14], by (Select) 14] X >= X by (Meta) 15] fold(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [16], by (Star) 16] fold*(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [17], [3], [18], [19] and [20], by (Stat) 17] F >= F by (Meta) 18] fold*(F, cons(X, Y), Z) >= F because [17], by (Select) 19] fold*(F, cons(X, Y), Z) >= Y because [7], by (Select) 20] fold*(F, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(F, Z), X) because fold > @_{o -> o}, [21] and [24], by (Copy) 21] fold*(F, cons(X, Y), Z) >= @_{o -> o -> o}(F, Z) because fold > @_{o -> o -> o}, [18] and [22], by (Copy) 22] fold*(F, cons(X, Y), Z) >= Z because [23], by (Select) 23] Z >= Z by (Meta) 24] fold*(F, cons(X, Y), Z) >= X because [25], by (Select) 25] cons(X, Y) >= X because [26], by (Star) 26] cons*(X, Y) >= X because [27], by (Select) 27] X >= X by (Meta) 28] fold(/\x./\y.add(x, y), X, 0) >= fold(/\x./\y.add(x, y), X, 0) because [29], [34] and [35], by (Fun) 29] /\x./\z.add(x, z) >= /\x./\z.add(x, z) because [30], by (Abs) 30] /\z.add(y, z) >= /\z.add(y, z) because [31], by (Abs) 31] add(y, x) >= add(y, x) because add in Mul, [32] and [33], by (Fun) 32] y >= y by (Var) 33] x >= x by (Var) 34] X >= X by (Meta) 35] 0 >= 0 by (Fun) 36] fold(/\x./\y.mul(x, y), X, 1) >= prod(X) because [37], by (Star) 37] fold*(/\x./\y.mul(x, y), X, 1) >= prod(X) because [38], by (Select) 38] mul(fold*(/\x./\y.mul(x, y), X, 1), fold*(/\z./\u.mul(z, u), X, 1)) >= prod(X) because [39], by (Star) 39] mul*(fold*(/\x./\y.mul(x, y), X, 1), fold*(/\z./\u.mul(z, u), X, 1)) >= prod(X) because mul = prod, mul in Mul and [40], by (Stat) 40] fold*(/\x./\y.mul(x, y), X, 1) >= X because [41], by (Select) 41] 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_0, R_0, static, formative) by (P_1, R_0, static, formative), where P_1 consists of: sum#(X) =#> fold#(/\x./\y.add(x, y), X, 0) 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: sum#(X) >? fold#(/\x./\y.add(x, y), X, 0) fold(F, nil, X) >= X fold(F, cons(X, Y), Z) >= fold(F, Y, F Z X) sum(X) >= fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) >= prod(X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( sum(X) ) = #argfun-sum#(fold(/\x./\y.add(x, y), X, 0)) pi( sum#(X) ) = #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) 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-sum#(x_1)]] = x_1 [[fold(x_1, x_2, x_3)]] = fold(x_2, x_3, x_1) [[prod(x_1)]] = _|_ [[sum(x_1)]] = x_1 [[sum#(x_1)]] = x_1 We choose Lex = {fold} and Mul = {#argfun-sum##, 0, 1, @_{o -> o -> o}, @_{o -> o}, add, cons, fold#, mul, nil}, and the following precedence: #argfun-sum## > 0 > fold > @_{o -> o -> o} > fold# > nil > mul > cons > add > @_{o -> o} > 1 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) > fold#(/\x./\y.add(x, y), X, 0) fold(F, nil, X) >= X fold(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) fold(/\x./\y.add(x, y), X, 0) >= fold(/\x./\y.add(x, y), X, 0) fold(/\x./\y.mul(x, y), X, 1) >= _|_ With these choices, we have: 1] #argfun-sum##(fold#(/\x./\y.add(x, y), X, 0)) > fold#(/\x./\y.add(x, y), X, 0) because [2], by definition 2] #argfun-sum##*(fold#(/\x./\y.add(x, y), X, 0)) >= fold#(/\x./\y.add(x, y), X, 0) because [3], by (Select) 3] fold#(/\x./\y.add(x, y), X, 0) >= fold#(/\x./\y.add(x, y), X, 0) because fold# in Mul, [4], [9] and [10], by (Fun) 4] /\x./\z.add(x, z) >= /\x./\z.add(x, z) because [5], by (Abs) 5] /\z.add(y, z) >= /\z.add(y, z) because [6], by (Abs) 6] add(y, x) >= add(y, x) because add in Mul, [7] and [8], by (Fun) 7] y >= y by (Var) 8] x >= x by (Var) 9] X >= X by (Meta) 10] 0 >= 0 by (Fun) 11] fold(F, nil, X) >= X because [12], by (Star) 12] fold*(F, nil, X) >= X because [13], by (Select) 13] X >= X by (Meta) 14] fold(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [15], by (Star) 15] fold*(F, cons(X, Y), Z) >= fold(F, Y, @_{o -> o}(@_{o -> o -> o}(F, Z), X)) because [16], [19], [21] and [23], by (Stat) 16] cons(X, Y) > Y because [17], by definition 17] cons*(X, Y) >= Y because [18], by (Select) 18] Y >= Y by (Meta) 19] fold*(F, cons(X, Y), Z) >= F because [20], by (Select) 20] F >= F by (Meta) 21] fold*(F, cons(X, Y), Z) >= Y because [22], by (Select) 22] cons(X, Y) >= Y because [17], by (Star) 23] fold*(F, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(F, Z), X) because fold > @_{o -> o}, [24] and [27], by (Copy) 24] fold*(F, cons(X, Y), Z) >= @_{o -> o -> o}(F, Z) because fold > @_{o -> o -> o}, [19] and [25], by (Copy) 25] fold*(F, cons(X, Y), Z) >= Z because [26], by (Select) 26] Z >= Z by (Meta) 27] fold*(F, cons(X, Y), Z) >= X because [28], by (Select) 28] cons(X, Y) >= X because [29], by (Star) 29] cons*(X, Y) >= X because [30], by (Select) 30] X >= X by (Meta) 31] fold(/\x./\y.add(x, y), X, 0) >= fold(/\x./\y.add(x, y), X, 0) because [4], [9] and [10], by (Fun) 32] fold(/\x./\y.mul(x, y), X, 1) >= _|_ by (Bot) 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.