We consider the system h15. Alphabet: 0 : [] --> nat cons : [nat * natlist] --> natlist foldl : [nat -> nat -> nat * nat * natlist] --> nat nil : [] --> natlist plus : [] --> nat -> nat -> nat sum : [natlist] --> nat xap : [nat -> nat -> nat * nat] --> nat -> nat yap : [nat -> nat * nat] --> nat Rules: foldl(/\x./\y.yap(xap(f, x), y), z, nil) => z foldl(/\x./\y.yap(xap(f, x), y), z, cons(u, v)) => foldl(/\w./\x'.yap(xap(f, w), x'), yap(xap(f, z), u), v) sum(x) => foldl(/\y./\z.yap(xap(plus, y), z), 0, x) xap(f, x) => f x yap(f, x) => f x This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). Symbol xap is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. This gives: Alphabet: 0 : [] --> nat cons : [nat * natlist] --> natlist foldl : [nat -> nat -> nat * nat * natlist] --> nat nil : [] --> natlist plus : [nat] --> nat -> nat sum : [natlist] --> nat yap : [nat -> nat * nat] --> nat Rules: foldl(/\x./\y.yap(F(x), y), X, nil) => X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) => foldl(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) sum(X) => foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) => F X We use the dependency pair framework as described in [Kop12, Ch. 6/7], with dynamic dependency pairs. After applying [Kop12, Thm. 7.22] to denote collapsing dependency pairs in an extended form, we thus obtain the following dependency pair problem (P_0, R_0, minimal, all): Dependency Pairs P_0: 0] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldl#(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) 1] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(z), u) 2] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(z) 3] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(X), Y) 4] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(X) 5] sum#(X) =#> foldl#(/\x./\y.yap(plus(x), y), 0, X) 6] sum#(X) =#> yap#(plus(x), y) 7] yap#(F, X) =#> F(X) Rules R_0: foldl(/\x./\y.yap(F(x), y), X, nil) => X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) => foldl(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) sum(X) => foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) => F X Thus, the original system is terminating if (P_0, R_0, minimal, all) is finite. We consider the dependency pair problem (P_0, R_0, minimal, all). 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, 2, 3, 4 * 1 : * 2 : 0, 1, 2, 3, 4, 5, 6, 7 * 3 : 7 * 4 : 0, 1, 2, 3, 4, 5, 6, 7 * 5 : 0, 1, 2, 3, 4 * 6 : * 7 : 0, 1, 2, 3, 4, 5, 6, 7 This graph has the following strongly connected components: P_1: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> foldl#(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(z) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(X), Y) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(X) sum#(X) =#> foldl#(/\x./\y.yap(plus(x), y), 0, X) yap#(F, X) =#> F(X) 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). Thus, the original system is terminating if (P_1, R_0, minimal, all) is finite. We consider the dependency pair problem (P_1, R_0, minimal, all). 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: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? foldl#(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? F(~c1) ~c0 foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? yap#(F(X), Y) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? F(X) ~c2 sum#(X) >? foldl#(/\x./\y.yap(plus(x), y), 0, X) yap#(F, X) >? F(X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) >= F X foldl(F, X, Y) >= foldl#(F, X, Y) sum(X) >= sum#(X) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( sum#(X) ) = #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) pi( yap#(F, X) ) = #argfun-yap##(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: [[foldl(x_1, x_2, x_3)]] = foldl(x_3, x_2, x_1) [[foldl#(x_1, x_2, x_3)]] = foldl#(x_1, x_3, x_2) [[sum#(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ [[~c2]] = _|_ We choose Lex = {foldl, foldl#} and Mul = {#argfun-sum##, #argfun-yap##, 0, @_{o -> o}, cons, nil, plus, sum, yap, yap#}, and the following precedence: nil > sum > #argfun-sum## > foldl > foldl# > plus > yap > yap# > @_{o -> o} > cons > #argfun-yap## > 0 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > foldl#(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(_|_), _|_) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= #argfun-yap##(@_{o -> o}(F(X), Y)) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(X), _|_) #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) > foldl#(/\x./\y.yap(plus(x), y), 0, X) #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) >= @_{o -> o}(F, X) foldl(F, X, Y) >= foldl#(F, X, Y) sum(X) >= #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > foldl#(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [2], by definition 2] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl#(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [3], [9], [12], [13] and [23], by (Stat) 3] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [4], by (Abs) 4] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [5], by (Abs) 5] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [6] and [8], by (Fun) 6] F(y) >= F(y) because [7], by (Meta) 7] y >= y by (Var) 8] x >= x by (Var) 9] cons(Y, Z) > Z because [10], by definition 10] cons*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= /\z./\u.yap(F(z), u) because [3], by (Select) 13] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= yap(F(X), Y) because foldl# > yap, [14] and [19], by (Copy) 14] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= F(X) because [15], by (Select) 15] /\z.yap(F(foldl#*(/\u./\v.yap(F(u), v), X, cons(Y, Z))), z) >= F(X) because [16], by (Eta)[Kop13:2] 16] F(foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(X) because [17], by (Meta) 17] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= X because [18], by (Select) 18] X >= X by (Meta) 19] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Y because [20], by (Select) 20] cons(Y, Z) >= Y because [21], by (Star) 21] cons*(Y, Z) >= Y because [22], by (Select) 22] Y >= Y by (Meta) 23] foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Z because [24], by (Select) 24] cons(Y, Z) >= Z because [10], by (Star) 25] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(_|_), _|_) because [26], by definition 26] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(_|_), _|_) because [27], by (Select) 27] yap(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(_|_), _|_) because [28], by (Star) 28] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(_|_), _|_) because yap > @_{o -> o}, [29] and [32], by (Copy) 29] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(_|_) because [30], by (Select) 30] F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(_|_) because [31], by (Meta) 31] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= _|_ by (Bot) 32] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= _|_ by (Bot) 33] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because [34], by (Star) 34] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because [35], by (Select) 35] yap(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because [36], by (Star) 36] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because yap > #argfun-yap## and [37], by (Copy) 37] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(X), Y) because yap > @_{o -> o}, [38] and [39], by (Copy) 38] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(X) because [16], by (Select) 39] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= Y because [19], by (Select) 40] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(X), _|_) because [41], by (Star) 41] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(X), _|_) because foldl# > @_{o -> o}, [14] and [42], by (Copy) 42] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= _|_ by (Bot) 43] #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) > foldl#(/\x./\y.yap(plus(x), y), 0, X) because [44], by definition 44] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X)) >= foldl#(/\x./\y.yap(plus(x), y), 0, X) because #argfun-sum## > foldl#, [45], [53] and [54], by (Copy) 45] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X)) >= /\x./\y.yap(plus(x), y) because [46], by (F-Abs) 46] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X), z) >= /\x.yap(plus(z), x) because [47], by (F-Abs) 47] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X), z, u) >= yap(plus(z), u) because #argfun-sum## > yap, [48] and [51], by (Copy) 48] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X), z, u) >= plus(z) because #argfun-sum## > plus and [49], by (Copy) 49] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X), z, u) >= z because [50], by (Select) 50] z >= z by (Var) 51] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X), z, u) >= u because [52], by (Select) 52] u >= u by (Var) 53] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X)) >= 0 because #argfun-sum## > 0, by (Copy) 54] #argfun-sum##*(foldl#(/\x./\y.yap(plus(x), y), 0, X)) >= X because [55], by (Select) 55] foldl#(/\x./\y.yap(plus(x), y), 0, X) >= X because [56], by (Star) 56] foldl#*(/\x./\y.yap(plus(x), y), 0, X) >= X because [57], by (Select) 57] X >= X by (Meta) 58] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [59], by (Star) 59] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [60], by (Select) 60] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [61] and [62], by (Fun) 61] F >= F by (Meta) 62] X >= X by (Meta) 63] foldl(/\x./\y.yap(F(x), y), X, nil) >= X because [64], by (Star) 64] foldl*(/\x./\y.yap(F(x), y), X, nil) >= X because [65], by (Select) 65] X >= X by (Meta) 66] foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [67], by (Star) 67] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [9], [68], [69] and [75], by (Stat) 68] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= /\x./\y.yap(F(x), y) because [3], by (Select) 69] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= yap(F(X), Y) because foldl > yap, [70] and [74], by (Copy) 70] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= F(X) because [71], by (Select) 71] /\x.yap(F(foldl*(/\y./\z.yap(F(y), z), X, cons(Y, Z))), x) >= F(X) because [72], by (Eta)[Kop13:2] 72] F(foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(X) because [73], by (Meta) 73] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= X because [18], by (Select) 74] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Y because [20], by (Select) 75] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Z because [24], by (Select) 76] sum(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) because [77], by (Star) 77] sum*(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) because sum > foldl, [78], [86] and [87], by (Copy) 78] sum*(X) >= /\y./\z.yap(plus(y), z) because [79], by (F-Abs) 79] sum*(X, x) >= /\z.yap(plus(x), z) because [80], by (F-Abs) 80] sum*(X, x, y) >= yap(plus(x), y) because sum > yap, [81] and [84], by (Copy) 81] sum*(X, x, y) >= plus(x) because sum > plus and [82], by (Copy) 82] sum*(X, x, y) >= x because [83], by (Select) 83] x >= x by (Var) 84] sum*(X, x, y) >= y because [85], by (Select) 85] y >= y by (Var) 86] sum*(X) >= 0 because sum > 0, by (Copy) 87] sum*(X) >= X because [57], by (Select) 88] yap(F, X) >= @_{o -> o}(F, X) because [89], by (Star) 89] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [90] and [91], by (Copy) 90] yap*(F, X) >= F because [61], by (Select) 91] yap*(F, X) >= X because [62], by (Select) 92] foldl(F, X, Y) >= foldl#(F, X, Y) because [93], by (Star) 93] foldl*(F, X, Y) >= foldl#(F, X, Y) because foldl > foldl#, [94], [96] and [98], by (Copy) 94] foldl*(F, X, Y) >= F because [95], by (Select) 95] F >= F by (Meta) 96] foldl*(F, X, Y) >= X because [97], by (Select) 97] X >= X by (Meta) 98] foldl*(F, X, Y) >= Y because [99], by (Select) 99] Y >= Y by (Meta) 100] sum(X) >= #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) because [101], by (Star) 101] sum*(X) >= #argfun-sum##(foldl#(/\x./\y.yap(plus(x), y), 0, X)) because sum > #argfun-sum## and [102], by (Copy) 102] sum*(X) >= foldl#(/\x./\y.yap(plus(x), y), 0, X) because sum > foldl#, [103], [111] and [112], by (Copy) 103] sum*(X) >= /\y./\z.yap(plus(y), z) because [104], by (F-Abs) 104] sum*(X, x) >= /\z.yap(plus(x), z) because [105], by (F-Abs) 105] sum*(X, x, y) >= yap(plus(x), y) because sum > yap, [106] and [109], by (Copy) 106] sum*(X, x, y) >= plus(x) because sum > plus and [107], by (Copy) 107] sum*(X, x, y) >= x because [108], by (Select) 108] x >= x by (Var) 109] sum*(X, x, y) >= y because [110], by (Select) 110] y >= y by (Var) 111] sum*(X) >= 0 because sum > 0, by (Copy) 112] sum*(X) >= X because [113], by (Select) 113] X >= X by (Meta) 114] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [115], by (Star) 115] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [116], by (Copy) 116] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [117] and [119], by (Copy) 117] yap*(F, X) >= F because [118], by (Select) 118] F >= F by (Meta) 119] yap*(F, X) >= X because [120], by (Select) 120] 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, minimal, all) by (P_2, R_0, minimal, all), where P_2 consists of: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> yap#(F(X), Y) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) =#> F(X) yap#(F, X) =#> F(X) Thus, the original system is terminating if (P_2, R_0, minimal, all) is finite. We consider the dependency pair problem (P_2, R_0, minimal, all). 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: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? yap#(F(X), Y) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >? F(X) ~c0 yap#(F, X) >? F(X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) >= F X foldl(F, X, Y) >= foldl#(F, X, Y) yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( yap#(F, X) ) = #argfun-yap##(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]] = _|_ [[foldl(x_1, x_2, x_3)]] = foldl(x_3, x_2, x_1) [[~c0]] = _|_ We choose Lex = {foldl} and Mul = {#argfun-yap##, @_{o -> o}, cons, foldl#, nil, plus, sum, yap, yap#}, and the following precedence: nil > sum > plus > foldl > foldl# > yap > cons > #argfun-yap## > @_{o -> o} > yap# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > #argfun-yap##(@_{o -> o}(F(X), Y)) foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(X), _|_) #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) yap(F, X) >= @_{o -> o}(F, X) foldl(F, X, Y) >= foldl#(F, X, Y) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > #argfun-yap##(@_{o -> o}(F(X), Y)) because [2], by definition 2] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because [3], by (Select) 3] yap(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because [4], by (Star) 4] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= #argfun-yap##(@_{o -> o}(F(X), Y)) because yap > #argfun-yap## and [5], by (Copy) 5] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(X), Y) because yap > @_{o -> o}, [6] and [10], by (Copy) 6] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(X) because [7], by (Select) 7] F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))) >= F(X) because [8], by (Meta) 8] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= X because [9], by (Select) 9] X >= X by (Meta) 10] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= Y because [11], by (Select) 11] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= Y because [12], by (Select) 12] cons(Y, Z) >= Y because [13], by (Star) 13] cons*(Y, Z) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] foldl#(/\x./\y.yap(F(x), y), X, cons(Y, Z)) > @_{o -> o}(F(X), _|_) because [16], by definition 16] foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= @_{o -> o}(F(X), _|_) because [17], by (Select) 17] yap(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(X), _|_) because [18], by (Star) 18] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= @_{o -> o}(F(X), _|_) because yap > @_{o -> o}, [6] and [19], by (Copy) 19] yap*(F(foldl#*(/\x./\y.yap(F(x), y), X, cons(Y, Z))), foldl#*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= _|_ by (Bot) 20] #argfun-yap##(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [21], by (Star) 21] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [22], by (Select) 22] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [23] and [24], by (Fun) 23] F >= F by (Meta) 24] X >= X by (Meta) 25] foldl(/\x./\y.yap(F(x), y), X, nil) >= X because [26], by (Star) 26] foldl*(/\x./\y.yap(F(x), y), X, nil) >= X because [27], by (Select) 27] X >= X by (Meta) 28] foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [29], by (Star) 29] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [30], [33], [40] and [46], by (Stat) 30] cons(Y, Z) > Z because [31], by definition 31] cons*(Y, Z) >= Z because [32], by (Select) 32] Z >= Z by (Meta) 33] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= /\x./\y.yap(F(x), y) because [34], by (Select) 34] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [35], by (Abs) 35] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [36], by (Abs) 36] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [37] and [39], by (Fun) 37] F(y) >= F(y) because [38], by (Meta) 38] y >= y by (Var) 39] x >= x by (Var) 40] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= yap(F(X), Y) because foldl > yap, [41] and [45], by (Copy) 41] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= F(X) because [42], by (Select) 42] /\z.yap(F(foldl*(/\u./\v.yap(F(u), v), X, cons(Y, Z))), z) >= F(X) because [43], by (Eta)[Kop13:2] 43] F(foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(X) because [44], by (Meta) 44] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= X because [9], by (Select) 45] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Y because [12], by (Select) 46] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Z because [47], by (Select) 47] cons(Y, Z) >= Z because [31], by (Star) 48] sum(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) because [49], by (Star) 49] sum*(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) because sum > foldl, [50], [58] and [59], by (Copy) 50] sum*(X) >= /\y./\z.yap(plus(y), z) because [51], by (F-Abs) 51] sum*(X, x) >= /\z.yap(plus(x), z) because [52], by (F-Abs) 52] sum*(X, x, y) >= yap(plus(x), y) because sum > yap, [53] and [56], by (Copy) 53] sum*(X, x, y) >= plus(x) because sum > plus and [54], by (Copy) 54] sum*(X, x, y) >= x because [55], by (Select) 55] x >= x by (Var) 56] sum*(X, x, y) >= y because [57], by (Select) 57] y >= y by (Var) 58] sum*(X) >= _|_ by (Bot) 59] sum*(X) >= X because [60], by (Select) 60] X >= X by (Meta) 61] yap(F, X) >= @_{o -> o}(F, X) because [62], by (Star) 62] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [63] and [64], by (Copy) 63] yap*(F, X) >= F because [23], by (Select) 64] yap*(F, X) >= X because [24], by (Select) 65] foldl(F, X, Y) >= foldl#(F, X, Y) because [66], by (Star) 66] foldl*(F, X, Y) >= foldl#(F, X, Y) because foldl > foldl#, [67], [69] and [71], by (Copy) 67] foldl*(F, X, Y) >= F because [68], by (Select) 68] F >= F by (Meta) 69] foldl*(F, X, Y) >= X because [70], by (Select) 70] X >= X by (Meta) 71] foldl*(F, X, Y) >= Y because [72], by (Select) 72] Y >= Y by (Meta) 73] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [74], by (Star) 74] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [75], by (Copy) 75] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [76] and [78], by (Copy) 76] yap*(F, X) >= F because [77], by (Select) 77] F >= F by (Meta) 78] yap*(F, X) >= X because [79], by (Select) 79] 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_2, R_0, minimal, all) by (P_3, R_0, minimal, all), where P_3 consists of: yap#(F, X) =#> F(X) Thus, the original system is terminating if (P_3, R_0, minimal, all) is finite. We consider the dependency pair problem (P_3, R_0, minimal, all). 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: yap#(F, X) >? F(X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\z./\u.yap(F(z), u), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), 0, X) yap(F, X) >= F X yap(F, X) >= yap#(F, X) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( yap#(F, X) ) = #argfun-yap##(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]] = _|_ [[foldl(x_1, x_2, x_3)]] = foldl(x_3, x_2, x_1) We choose Lex = {foldl} and Mul = {#argfun-yap##, @_{o -> o}, cons, nil, plus, sum, yap, yap#}, and the following precedence: nil > sum > plus > foldl > yap > #argfun-yap## > @_{o -> o} > cons > yap# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) foldl(/\x./\y.yap(F(x), y), X, nil) >= X foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) sum(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) yap(F, X) >= @_{o -> o}(F, X) yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) With these choices, we have: 1] #argfun-yap##(@_{o -> o}(F, X)) > @_{o -> o}(F, X) because [2], by definition 2] #argfun-yap##*(@_{o -> o}(F, X)) >= @_{o -> o}(F, X) because [3], by (Select) 3] @_{o -> o}(F, X) >= @_{o -> o}(F, X) because @_{o -> o} in Mul, [4] and [5], by (Fun) 4] F >= F by (Meta) 5] X >= X by (Meta) 6] foldl(/\x./\y.yap(F(x), y), X, nil) >= X because [7], by (Star) 7] foldl*(/\x./\y.yap(F(x), y), X, nil) >= X because [8], by (Select) 8] X >= X by (Meta) 9] foldl(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [10], by (Star) 10] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= foldl(/\x./\y.yap(F(x), y), yap(F(X), Y), Z) because [11], [14], [21] and [31], by (Stat) 11] cons(Y, Z) > Z because [12], by definition 12] cons*(Y, Z) >= Z because [13], by (Select) 13] Z >= Z by (Meta) 14] foldl*(/\x./\y.yap(F(x), y), X, cons(Y, Z)) >= /\x./\y.yap(F(x), y) because [15], by (Select) 15] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [16], by (Abs) 16] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [17], by (Abs) 17] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [18] and [20], by (Fun) 18] F(y) >= F(y) because [19], by (Meta) 19] y >= y by (Var) 20] x >= x by (Var) 21] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= yap(F(X), Y) because foldl > yap, [22] and [27], by (Copy) 22] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= F(X) because [23], by (Select) 23] /\z.yap(F(foldl*(/\u./\v.yap(F(u), v), X, cons(Y, Z))), z) >= F(X) because [24], by (Eta)[Kop13:2] 24] F(foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z))) >= F(X) because [25], by (Meta) 25] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= X because [26], by (Select) 26] X >= X by (Meta) 27] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Y because [28], by (Select) 28] cons(Y, Z) >= Y because [29], by (Star) 29] cons*(Y, Z) >= Y because [30], by (Select) 30] Y >= Y by (Meta) 31] foldl*(/\z./\u.yap(F(z), u), X, cons(Y, Z)) >= Z because [32], by (Select) 32] cons(Y, Z) >= Z because [12], by (Star) 33] sum(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) because [34], by (Star) 34] sum*(X) >= foldl(/\x./\y.yap(plus(x), y), _|_, X) because sum > foldl, [35], [43] and [44], by (Copy) 35] sum*(X) >= /\y./\z.yap(plus(y), z) because [36], by (F-Abs) 36] sum*(X, x) >= /\z.yap(plus(x), z) because [37], by (F-Abs) 37] sum*(X, x, y) >= yap(plus(x), y) because sum > yap, [38] and [41], by (Copy) 38] sum*(X, x, y) >= plus(x) because sum > plus and [39], by (Copy) 39] sum*(X, x, y) >= x because [40], by (Select) 40] x >= x by (Var) 41] sum*(X, x, y) >= y because [42], by (Select) 42] y >= y by (Var) 43] sum*(X) >= _|_ by (Bot) 44] sum*(X) >= X because [45], by (Select) 45] X >= X by (Meta) 46] yap(F, X) >= @_{o -> o}(F, X) because [47], by (Star) 47] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [48] and [49], by (Copy) 48] yap*(F, X) >= F because [4], by (Select) 49] yap*(F, X) >= X because [5], by (Select) 50] yap(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because [51], by (Star) 51] yap*(F, X) >= #argfun-yap##(@_{o -> o}(F, X)) because yap > #argfun-yap## and [52], by (Copy) 52] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [53] and [55], by (Copy) 53] yap*(F, X) >= F because [54], by (Select) 54] F >= F by (Meta) 55] yap*(F, X) >= X because [56], by (Select) 56] 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_3, 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:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.