We consider the system Applicative_05__Ex7Sorting. Alphabet: 0 : [] --> a asort : [b] --> b cons : [a * b] --> b dsort : [b] --> b insert : [a -> a -> a * a -> a -> a * b * a] --> b max : [] --> a -> a -> a min : [] --> a -> a -> a nil : [] --> b s : [a] --> a sort : [a -> a -> a * a -> a -> a * b] --> b Rules: sort(f, g, nil) => nil sort(f, g, cons(x, y)) => insert(f, g, sort(f, g, y), x) insert(f, g, nil, x) => cons(x, nil) insert(f, g, cons(x, y), z) => cons(f x z, insert(f, g, y, g x z)) max 0 x => x max x 0 => x max s(x) s(y) => max x y min 0 x => 0 min x 0 => 0 min s(x) s(y) => min x y asort(x) => sort(min, max, x) dsort(x) => sort(max, min, x) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): sort(F, G, nil) >? nil sort(F, G, cons(X, Y)) >? insert(F, G, sort(F, G, Y), X) insert(F, G, nil, X) >? cons(X, nil) insert(F, G, cons(X, Y), Z) >? cons(F X Z, insert(F, G, Y, G X Z)) max 0 X >? X max X 0 >? X max s(X) s(Y) >? max X Y min 0 X >? 0 min X 0 >? 0 min s(X) s(Y) >? min X Y asort(X) >? sort(min, max, X) dsort(X) >? sort(max, min, X) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[max]] = _|_ [[nil]] = _|_ We choose Lex = {insert} and Mul = {0, @_{o -> o -> o}, @_{o -> o}, asort, cons, dsort, min, s, sort}, and the following precedence: asort > dsort > min > s > sort > 0 > insert > @_{o -> o} > cons > @_{o -> o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: sort(F, G, _|_) > _|_ sort(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) insert(F, G, _|_, X) > cons(X, _|_) insert(F, G, cons(X, Y), Z) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) @_{o -> o}(@_{o -> o -> o}(_|_, 0), X) > X @_{o -> o}(@_{o -> o -> o}(_|_, X), 0) > X @_{o -> o}(@_{o -> o -> o}(_|_, s(X)), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) @_{o -> o}(@_{o -> o -> o}(min, 0), X) > 0 @_{o -> o}(@_{o -> o -> o}(min, X), 0) >= 0 @_{o -> o}(@_{o -> o -> o}(min, s(X)), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(min, X), Y) asort(X) > sort(min, _|_, X) dsort(X) > sort(_|_, min, X) With these choices, we have: 1] sort(F, G, _|_) > _|_ because [2], by definition 2] sort*(F, G, _|_) >= _|_ by (Bot) 3] sort(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) because [4], by (Star) 4] sort*(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) because sort > insert, [5], [7], [9] and [15], by (Copy) 5] sort*(F, G, cons(X, Y)) >= F because [6], by (Select) 6] F >= F by (Meta) 7] sort*(F, G, cons(X, Y)) >= G because [8], by (Select) 8] G >= G by (Meta) 9] sort*(F, G, cons(X, Y)) >= sort(F, G, Y) because sort in Mul, [10], [11] and [12], by (Stat) 10] F >= F by (Meta) 11] G >= G by (Meta) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] sort*(F, G, cons(X, Y)) >= X because [16], by (Select) 16] cons(X, Y) >= X because [17], by (Star) 17] cons*(X, Y) >= X because [18], by (Select) 18] X >= X by (Meta) 19] insert(F, G, _|_, X) > cons(X, _|_) because [20], by definition 20] insert*(F, G, _|_, X) >= cons(X, _|_) because insert > cons, [21] and [23], by (Copy) 21] insert*(F, G, _|_, X) >= X because [22], by (Select) 22] X >= X by (Meta) 23] insert*(F, G, _|_, X) >= _|_ by (Bot) 24] insert(F, G, cons(X, Y), Z) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) because [25], by (Star) 25] insert*(F, G, cons(X, Y), Z) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) because insert > cons, [26] and [36], by (Copy) 26] insert*(F, G, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(F, X), Z) because insert > @_{o -> o}, [27] and [34], by (Copy) 27] insert*(F, G, cons(X, Y), Z) >= @_{o -> o -> o}(F, X) because insert > @_{o -> o -> o}, [28] and [30], by (Copy) 28] insert*(F, G, cons(X, Y), Z) >= F because [29], by (Select) 29] F >= F by (Meta) 30] insert*(F, G, cons(X, Y), Z) >= X because [31], by (Select) 31] cons(X, Y) >= X because [32], by (Star) 32] cons*(X, Y) >= X because [33], by (Select) 33] X >= X by (Meta) 34] insert*(F, G, cons(X, Y), Z) >= Z because [35], by (Select) 35] Z >= Z by (Meta) 36] insert*(F, G, cons(X, Y), Z) >= insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z)) because [37], [38], [39], [28], [42], [43] and [45], by (Stat) 37] F >= F by (Meta) 38] G >= G by (Meta) 39] cons(X, Y) > Y because [40], by definition 40] cons*(X, Y) >= Y because [41], by (Select) 41] Y >= Y by (Meta) 42] insert*(F, G, cons(X, Y), Z) >= G because [38], by (Select) 43] insert*(F, G, cons(X, Y), Z) >= Y because [44], by (Select) 44] cons(X, Y) >= Y because [40], by (Star) 45] insert*(F, G, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(G, X), Z) because insert > @_{o -> o}, [46] and [34], by (Copy) 46] insert*(F, G, cons(X, Y), Z) >= @_{o -> o -> o}(G, X) because insert > @_{o -> o -> o}, [42] and [30], by (Copy) 47] @_{o -> o}(@_{o -> o -> o}(_|_, 0), X) > X because [48], by definition 48] @_{o -> o}*(@_{o -> o -> o}(_|_, 0), X) >= X because [49], by (Select) 49] X >= X by (Meta) 50] @_{o -> o}(@_{o -> o -> o}(_|_, X), 0) > X because [51], by definition 51] @_{o -> o}*(@_{o -> o -> o}(_|_, X), 0) >= X because [52], by (Select) 52] @_{o -> o -> o}(_|_, X) @_{o -> o}*(@_{o -> o -> o}(_|_, X), 0) >= X because [53] 53] @_{o -> o -> o}*(_|_, X, @_{o -> o}*(@_{o -> o -> o}(_|_, X), 0)) >= X because [54], by (Select) 54] X >= X by (Meta) 55] @_{o -> o}(@_{o -> o -> o}(_|_, s(X)), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) because [56], by (Star) 56] @_{o -> o}*(@_{o -> o -> o}(_|_, s(X)), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(_|_, X), Y) because @_{o -> o} in Mul, [57] and [63], by (Stat) 57] @_{o -> o -> o}(_|_, s(X)) > @_{o -> o -> o}(_|_, X) because [58], by definition 58] @_{o -> o -> o}*(_|_, s(X)) >= @_{o -> o -> o}(_|_, X) because @_{o -> o -> o} in Mul, [59] and [60], by (Stat) 59] _|_ >= _|_ by (Bot) 60] s(X) > X because [61], by definition 61] s*(X) >= X because [62], by (Select) 62] X >= X by (Meta) 63] s(Y) >= Y because [64], by (Star) 64] s*(Y) >= Y because [65], by (Select) 65] Y >= Y by (Meta) 66] @_{o -> o}(@_{o -> o -> o}(min, 0), X) > 0 because [67], by definition 67] @_{o -> o}*(@_{o -> o -> o}(min, 0), X) >= 0 because [68], by (Select) 68] @_{o -> o -> o}(min, 0) @_{o -> o}*(@_{o -> o -> o}(min, 0), X) >= 0 because [69] 69] @_{o -> o -> o}*(min, 0, @_{o -> o}*(@_{o -> o -> o}(min, 0), X)) >= 0 because [70], by (Select) 70] min @_{o -> o -> o}*(min, 0, @_{o -> o}*(@_{o -> o -> o}(min, 0), X)) @_{o -> o -> o}*(min, 0, @_{o -> o}*(@_{o -> o -> o}(min, 0), X)) >= 0 because [71] 71] min*(@_{o -> o -> o}*(min, 0, @_{o -> o}*(@_{o -> o -> o}(min, 0), X)), @_{o -> o -> o}*(min, 0, @_{o -> o}*(@_{o -> o -> o}(min, 0), X))) >= 0 because min > 0, by (Copy) 72] @_{o -> o}(@_{o -> o -> o}(min, X), 0) >= 0 because [73], by (Star) 73] @_{o -> o}*(@_{o -> o -> o}(min, X), 0) >= 0 because [74], by (Select) 74] 0 >= 0 by (Fun) 75] @_{o -> o}(@_{o -> o -> o}(min, s(X)), s(Y)) >= @_{o -> o}(@_{o -> o -> o}(min, X), Y) because @_{o -> o} in Mul, [76] and [81], by (Fun) 76] @_{o -> o -> o}(min, s(X)) >= @_{o -> o -> o}(min, X) because @_{o -> o -> o} in Mul, [77] and [78], by (Fun) 77] min >= min by (Fun) 78] s(X) >= X because [79], by (Star) 79] s*(X) >= X because [80], by (Select) 80] X >= X by (Meta) 81] s(Y) >= Y because [82], by (Star) 82] s*(Y) >= Y because [83], by (Select) 83] Y >= Y by (Meta) 84] asort(X) > sort(min, _|_, X) because [85], by definition 85] asort*(X) >= sort(min, _|_, X) because asort > sort, [86], [87] and [88], by (Copy) 86] asort*(X) >= min because asort > min, by (Copy) 87] asort*(X) >= _|_ by (Bot) 88] asort*(X) >= X because [89], by (Select) 89] X >= X by (Meta) 90] dsort(X) > sort(_|_, min, X) because [91], by definition 91] dsort*(X) >= sort(_|_, min, X) because dsort > sort, [92], [93] and [94], by (Copy) 92] dsort*(X) >= _|_ by (Bot) 93] dsort*(X) >= min because dsort > min, by (Copy) 94] dsort*(X) >= X because [95], by (Select) 95] X >= X by (Meta) We can thus remove the following rules: sort(F, G, nil) => nil insert(F, G, nil, X) => cons(X, nil) max 0 X => X max X 0 => X min 0 X => 0 asort(X) => sort(min, max, X) dsort(X) => sort(max, min, X) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): sort(F, G, cons(X, Y)) >? insert(F, G, sort(F, G, Y), X) insert(F, G, cons(X, Y), Z) >? cons(F X Z, insert(F, G, Y, G X Z)) max(s(X), s(Y)) >? max(X, Y) min(X, 0) >? 0 min(s(X), s(Y)) >? min(X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[insert(x_1, x_2, x_3, x_4)]] = insert(x_2, x_3, x_4, x_1) We choose Lex = {insert} and Mul = {0, @_{o -> o -> o}, @_{o -> o}, cons, max, min, s, sort}, and the following precedence: max = min > sort > insert > @_{o -> o -> o} > @_{o -> o} > s > cons > 0 Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: sort(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) insert(F, G, cons(X, Y), Z) > cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) max(s(X), s(Y)) >= max(X, Y) min(X, 0) >= 0 min(s(X), s(Y)) >= min(X, Y) With these choices, we have: 1] sort(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) because [2], by (Star) 2] sort*(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) because sort > insert, [3], [5], [7] and [13], by (Copy) 3] sort*(F, G, cons(X, Y)) >= F because [4], by (Select) 4] F >= F by (Meta) 5] sort*(F, G, cons(X, Y)) >= G because [6], by (Select) 6] G >= G by (Meta) 7] sort*(F, G, cons(X, Y)) >= sort(F, G, Y) because sort in Mul, [8], [9] and [10], by (Stat) 8] F >= F by (Meta) 9] G >= G by (Meta) 10] cons(X, Y) > Y because [11], by definition 11] cons*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] sort*(F, G, cons(X, Y)) >= X because [14], by (Select) 14] cons(X, Y) >= X because [15], by (Star) 15] cons*(X, Y) >= X because [16], by (Select) 16] X >= X by (Meta) 17] insert(F, G, cons(X, Y), Z) > cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) because [18], by definition 18] insert*(F, G, cons(X, Y), Z) >= cons(@_{o -> o}(@_{o -> o -> o}(F, X), Z), insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z))) because insert > cons, [19] and [29], by (Copy) 19] insert*(F, G, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(F, X), Z) because insert > @_{o -> o}, [20] and [27], by (Copy) 20] insert*(F, G, cons(X, Y), Z) >= @_{o -> o -> o}(F, X) because insert > @_{o -> o -> o}, [21] and [23], by (Copy) 21] insert*(F, G, cons(X, Y), Z) >= F because [22], by (Select) 22] F >= F by (Meta) 23] insert*(F, G, cons(X, Y), Z) >= X because [24], by (Select) 24] cons(X, Y) >= X because [25], by (Star) 25] cons*(X, Y) >= X because [26], by (Select) 26] X >= X by (Meta) 27] insert*(F, G, cons(X, Y), Z) >= Z because [28], by (Select) 28] Z >= Z by (Meta) 29] insert*(F, G, cons(X, Y), Z) >= insert(F, G, Y, @_{o -> o}(@_{o -> o -> o}(G, X), Z)) because [30], [31], [21], [34], [35] and [37], by (Stat) 30] G >= G by (Meta) 31] cons(X, Y) > Y because [32], by definition 32] cons*(X, Y) >= Y because [33], by (Select) 33] Y >= Y by (Meta) 34] insert*(F, G, cons(X, Y), Z) >= G because [30], by (Select) 35] insert*(F, G, cons(X, Y), Z) >= Y because [36], by (Select) 36] cons(X, Y) >= Y because [32], by (Star) 37] insert*(F, G, cons(X, Y), Z) >= @_{o -> o}(@_{o -> o -> o}(G, X), Z) because insert > @_{o -> o}, [38] and [27], by (Copy) 38] insert*(F, G, cons(X, Y), Z) >= @_{o -> o -> o}(G, X) because insert > @_{o -> o -> o}, [34] and [23], by (Copy) 39] max(s(X), s(Y)) >= max(X, Y) because [40], by (Star) 40] max*(s(X), s(Y)) >= max(X, Y) because max in Mul, [41] and [44], by (Stat) 41] s(X) > X because [42], by definition 42] s*(X) >= X because [43], by (Select) 43] X >= X by (Meta) 44] s(Y) >= Y because [45], by (Star) 45] s*(Y) >= Y because [46], by (Select) 46] Y >= Y by (Meta) 47] min(X, 0) >= 0 because [48], by (Star) 48] min*(X, 0) >= 0 because min > 0, by (Copy) 49] min(s(X), s(Y)) >= min(X, Y) because min in Mul, [50] and [53], by (Fun) 50] s(X) >= X because [51], by (Star) 51] s*(X) >= X because [52], by (Select) 52] X >= X by (Meta) 53] s(Y) >= Y because [54], by (Star) 54] s*(Y) >= Y because [55], by (Select) 55] Y >= Y by (Meta) We can thus remove the following rules: insert(F, G, cons(X, Y), Z) => cons(F X Z, insert(F, G, Y, G X Z)) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): sort(F, G, cons(X, Y)) >? insert(F, G, sort(F, G, Y), X) max(s(X), s(Y)) >? max(X, Y) min(X, 0) >? 0 min(s(X), s(Y)) >? min(X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, cons, insert, max, min, s, sort}, and the following precedence: min > 0 > sort > insert > cons > s > max With these choices, we have: 1] sort(F, G, cons(X, Y)) > insert(F, G, sort(F, G, Y), X) because [2], by definition 2] sort*(F, G, cons(X, Y)) >= insert(F, G, sort(F, G, Y), X) because sort > insert, [3], [5], [7] and [13], by (Copy) 3] sort*(F, G, cons(X, Y)) >= F because [4], by (Select) 4] F >= F by (Meta) 5] sort*(F, G, cons(X, Y)) >= G because [6], by (Select) 6] G >= G by (Meta) 7] sort*(F, G, cons(X, Y)) >= sort(F, G, Y) because sort in Mul, [8], [9] and [10], by (Stat) 8] F >= F by (Meta) 9] G >= G by (Meta) 10] cons(X, Y) > Y because [11], by definition 11] cons*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] sort*(F, G, cons(X, Y)) >= X because [14], by (Select) 14] cons(X, Y) >= X because [15], by (Star) 15] cons*(X, Y) >= X because [16], by (Select) 16] X >= X by (Meta) 17] max(s(X), s(Y)) >= max(X, Y) because max in Mul, [18] and [21], by (Fun) 18] s(X) >= X because [19], by (Star) 19] s*(X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] s(Y) >= Y because [22], by (Star) 22] s*(Y) >= Y because [23], by (Select) 23] Y >= Y by (Meta) 24] min(X, 0) > 0 because [25], by definition 25] min*(X, 0) >= 0 because [26], by (Select) 26] 0 >= 0 by (Fun) 27] min(s(X), s(Y)) > min(X, Y) because [28], by definition 28] min*(s(X), s(Y)) >= min(X, Y) because min in Mul, [29] and [32], by (Stat) 29] s(X) > X because [30], by definition 30] s*(X) >= X because [31], by (Select) 31] X >= X by (Meta) 32] s(Y) >= Y because [33], by (Star) 33] s*(Y) >= Y because [34], by (Select) 34] Y >= Y by (Meta) We can thus remove the following rules: sort(F, G, cons(X, Y)) => insert(F, G, sort(F, G, Y), X) min(X, 0) => 0 min(s(X), s(Y)) => min(X, Y) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): max(s(X), s(Y)) >? max(X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {max, s}, and the following precedence: max > s With these choices, we have: 1] max(s(X), s(Y)) > max(X, Y) because [2], by definition 2] max*(s(X), s(Y)) >= max(X, Y) because max in Mul, [3] and [6], by (Stat) 3] s(X) >= X because [4], by (Star) 4] s*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] s(Y) > Y because [7], by definition 7] s*(Y) >= Y because [8], by (Select) 8] Y >= Y by (Meta) We can thus remove the following rules: max(s(X), s(Y)) => max(X, Y) All rules were succesfully removed. Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.