We consider the system h00. Alphabet: 0 : [] --> c add : [] --> a -> c -> c cons : [] --> a -> b -> b fold : [] --> (a -> c -> c) -> c -> b -> c mul : [] --> a -> c -> c nil : [] --> b plus : [] --> c -> c -> c prod : [] --> b -> c s : [] --> c -> c sum : [] --> b -> c times : [] --> c -> c -> c Rules: fold (/\x./\y.f x y) z nil => z fold (/\x./\y.f x y) z (cons u v) => f u (fold (/\w./\x'.f w x') z v) 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 sum x => fold (/\y./\z.add y z) 0 x prod x => fold (/\y./\z.mul y z) (s 0) x Using the transformations described in [Kop11], this system can be brought in a form without leading free variables in the left-hand side, and where the left-hand side of a variable is always a functional term or application headed by a functional term. We now transform the resulting AFS into an AFSM by replacing all free variables by meta-variables (with arity 0). This leads to the following AFSM: Alphabet: 0 : [] --> c add : [] --> a -> c -> c cons : [a * b] --> b fold : [a -> c -> c * c * b] --> c mul : [] --> a -> c -> c nil : [] --> b plus : [c * c] --> c prod : [b] --> c s : [c] --> c sum : [b] --> c times : [c * c] --> c ~AP1 : [a -> c -> c * a] --> c -> c Rules: fold(/\x./\y.~AP1(F, x) y, X, nil) => X fold(/\x./\y.~AP1(F, x) y, X, cons(Y, Z)) => ~AP1(F, Y) fold(/\z./\u.~AP1(F, z) u, X, Z) 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) sum(X) => fold(/\x./\y.~AP1(add, x) y, 0, X) prod(X) => fold(/\x./\y.~AP1(mul, x) y, s(0), X) ~AP1(F, X) => F X Symbol ~AP1 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 : [] --> c add : [a * c] --> c cons : [a * b] --> b fold : [a -> c -> c * c * b] --> c mul : [a * c] --> c nil : [] --> b plus : [c * c] --> c prod : [b] --> c s : [c] --> c sum : [b] --> c times : [c * c] --> c Rules: fold(/\x./\y.X(x, y), Y, nil) => Y fold(/\x./\y.X(x, y), Y, cons(Z, U)) => X(Z, fold(/\z./\u.X(z, u), Y, U)) 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) sum(X) => fold(/\x./\y.add(x, y), 0, X) prod(X) => fold(/\x./\y.mul(x, y), s(0), 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]): fold(/\x./\y.X(x, y), Y, nil) >? Y fold(/\x./\y.X(x, y), Y, cons(Z, U)) >? X(Z, fold(/\z./\u.X(z, u), Y, U)) 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) sum(X) >? fold(/\x./\y.add(x, y), 0, X) prod(X) >? fold(/\x./\y.mul(x, y), s(0), X) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {add, cons, fold, mul, nil, plus, prod, s, sum, times}, and the following precedence: cons > nil > prod > mul > sum > add > fold > times > plus > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold(/\x./\y.X(x, y), Y, nil) >= Y fold(/\x./\y.X(x, y), Y, cons(Z, U)) > X(Z, fold(/\x./\y.X(x, y), Y, U)) plus(_|_, X) > X plus(s(X), Y) >= s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) >= plus(times(X, Y), Y) sum(X) >= fold(/\x./\y.add(x, y), _|_, X) prod(X) > fold(/\x./\y.mul(x, y), s(_|_), X) With these choices, we have: 1] fold(/\x./\y.X(x, y), Y, nil) >= Y because [2], by (Star) 2] fold*(/\x./\y.X(x, y), Y, nil) >= Y because [3], by (Select) 3] Y >= Y by (Meta) 4] fold(/\x./\y.X(x, y), Y, cons(Z, U)) > X(Z, fold(/\x./\y.X(x, y), Y, U)) because [5], by definition 5] fold*(/\x./\y.X(x, y), Y, cons(Z, U)) >= X(Z, fold(/\x./\y.X(x, y), Y, U)) because [6], by (Select) 6] X(fold*(/\x./\y.X(x, y), Y, cons(Z, U)), fold*(/\z./\u.X(z, u), Y, cons(Z, U))) >= X(Z, fold(/\x./\y.X(x, y), Y, U)) because [7] and [11], by (Meta) 7] fold*(/\x./\y.X(x, y), Y, cons(Z, U)) >= Z because [8], by (Select) 8] cons(Z, U) >= Z because [9], by (Star) 9] cons*(Z, U) >= Z because [10], by (Select) 10] Z >= Z by (Meta) 11] fold*(/\x./\y.X(x, y), Y, cons(Z, U)) >= fold(/\x./\y.X(x, y), Y, U) because fold in Mul, [12], [17] and [18], by (Stat) 12] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [13], by (Abs) 13] /\z.X(y, z) >= /\z.X(y, z) because [14], by (Abs) 14] X(y, x) >= X(y, x) because [15] and [16], by (Meta) 15] y >= y by (Var) 16] x >= x by (Var) 17] Y >= Y by (Meta) 18] cons(Z, U) > U because [19], by definition 19] cons*(Z, U) >= U because [20], by (Select) 20] U >= U by (Meta) 21] plus(_|_, X) > X because [22], by definition 22] plus*(_|_, X) >= X because [23], by (Select) 23] X >= X by (Meta) 24] plus(s(X), Y) >= s(plus(X, Y)) because [25], by (Star) 25] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [26], by (Copy) 26] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [27] and [30], by (Stat) 27] s(X) > X because [28], by definition 28] s*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] Y >= Y by (Meta) 31] times(_|_, X) >= _|_ by (Bot) 32] times(s(X), Y) >= plus(times(X, Y), Y) because [33], by (Star) 33] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [34] and [39], by (Copy) 34] times*(s(X), Y) >= times(X, Y) because times in Mul, [35] and [38], by (Stat) 35] s(X) > X because [36], by definition 36] s*(X) >= X because [37], by (Select) 37] X >= X by (Meta) 38] Y >= Y by (Meta) 39] times*(s(X), Y) >= Y because [38], by (Select) 40] sum(X) >= fold(/\x./\y.add(x, y), _|_, X) because [41], by (Star) 41] sum*(X) >= fold(/\x./\y.add(x, y), _|_, X) because sum > fold, [42], [49] and [50], by (Copy) 42] sum*(X) >= /\y./\z.add(y, z) because [43], by (F-Abs) 43] sum*(X, x) >= /\z.add(x, z) because [44], by (F-Abs) 44] sum*(X, x, y) >= add(x, y) because sum > add, [45] and [47], by (Copy) 45] sum*(X, x, y) >= x because [46], by (Select) 46] x >= x by (Var) 47] sum*(X, x, y) >= y because [48], by (Select) 48] y >= y by (Var) 49] sum*(X) >= _|_ by (Bot) 50] sum*(X) >= X because [51], by (Select) 51] X >= X by (Meta) 52] prod(X) > fold(/\x./\y.mul(x, y), s(_|_), X) because [53], by definition 53] prod*(X) >= fold(/\x./\y.mul(x, y), s(_|_), X) because prod > fold, [54], [61] and [63], by (Copy) 54] prod*(X) >= /\y./\z.mul(y, z) because [55], by (F-Abs) 55] prod*(X, x) >= /\z.mul(x, z) because [56], by (F-Abs) 56] prod*(X, x, y) >= mul(x, y) because prod > mul, [57] and [59], by (Copy) 57] prod*(X, x, y) >= x because [58], by (Select) 58] x >= x by (Var) 59] prod*(X, x, y) >= y because [60], by (Select) 60] y >= y by (Var) 61] prod*(X) >= s(_|_) because prod > s and [62], by (Copy) 62] prod*(X) >= _|_ by (Bot) 63] prod*(X) >= X because [64], by (Select) 64] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.X(x, y), Y, cons(Z, U)) => X(Z, fold(/\z./\u.X(z, u), Y, U)) plus(0, X) => X prod(X) => fold(/\x./\y.mul(x, y), s(0), 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]): fold(/\x./\y.X(x, y), Y, nil) >? Y plus(s(X), Y) >? s(plus(X, Y)) times(0, X) >? 0 times(s(X), Y) >? plus(times(X, Y), Y) sum(X) >? fold(/\x./\y.add(x, y), 0, X) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {add, fold, nil, plus, s, sum, times}, and the following precedence: sum > add > fold > times > nil > plus > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold(/\x./\y.X(x, y), Y, nil) > Y plus(s(X), Y) > s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) >= plus(times(X, Y), Y) sum(X) >= fold(/\x./\y.add(x, y), _|_, X) With these choices, we have: 1] fold(/\x./\y.X(x, y), Y, nil) > Y because [2], by definition 2] fold*(/\x./\y.X(x, y), Y, nil) >= Y because [3], by (Select) 3] Y >= Y by (Meta) 4] plus(s(X), Y) > s(plus(X, Y)) because [5], by definition 5] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [6], by (Copy) 6] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [7] and [10], by (Stat) 7] s(X) > X because [8], by definition 8] s*(X) >= X because [9], by (Select) 9] X >= X by (Meta) 10] Y >= Y by (Meta) 11] times(_|_, X) >= _|_ by (Bot) 12] times(s(X), Y) >= plus(times(X, Y), Y) because [13], by (Star) 13] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [14] and [19], by (Copy) 14] times*(s(X), Y) >= times(X, Y) because times in Mul, [15] and [18], by (Stat) 15] s(X) > X because [16], by definition 16] s*(X) >= X because [17], by (Select) 17] X >= X by (Meta) 18] Y >= Y by (Meta) 19] times*(s(X), Y) >= Y because [18], by (Select) 20] sum(X) >= fold(/\x./\y.add(x, y), _|_, X) because [21], by (Star) 21] sum*(X) >= fold(/\x./\y.add(x, y), _|_, X) because sum > fold, [22], [29] and [30], by (Copy) 22] sum*(X) >= /\y./\z.add(y, z) because [23], by (F-Abs) 23] sum*(X, x) >= /\z.add(x, z) because [24], by (F-Abs) 24] sum*(X, x, y) >= add(x, y) because sum > add, [25] and [27], by (Copy) 25] sum*(X, x, y) >= x because [26], by (Select) 26] x >= x by (Var) 27] sum*(X, x, y) >= y because [28], by (Select) 28] y >= y by (Var) 29] sum*(X) >= _|_ by (Bot) 30] sum*(X) >= X because [31], by (Select) 31] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.X(x, y), Y, nil) => Y plus(s(X), Y) => s(plus(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]): times(0, X) >? 0 times(s(X), Y) >? plus(times(X, Y), Y) sum(X) >? fold(/\x./\y.add(x, y), 0, X) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {add, fold, plus, s, sum, times}, and the following precedence: s > sum > fold > times > add > plus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(_|_, X) > _|_ times(s(X), Y) >= plus(times(X, Y), Y) sum(X) >= fold(/\x./\y.add(x, y), _|_, X) With these choices, we have: 1] times(_|_, X) > _|_ because [2], by definition 2] times*(_|_, X) >= _|_ by (Bot) 3] times(s(X), Y) >= plus(times(X, Y), Y) because [4], by (Star) 4] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [5] and [10], by (Copy) 5] times*(s(X), Y) >= times(X, Y) because times in Mul, [6] and [9], by (Stat) 6] s(X) > X because [7], by definition 7] s*(X) >= X because [8], by (Select) 8] X >= X by (Meta) 9] Y >= Y by (Meta) 10] times*(s(X), Y) >= Y because [9], by (Select) 11] sum(X) >= fold(/\x./\y.add(x, y), _|_, X) because [12], by (Star) 12] sum*(X) >= fold(/\x./\y.add(x, y), _|_, X) because sum > fold, [13], [20] and [21], by (Copy) 13] sum*(X) >= /\y./\z.add(y, z) because [14], by (F-Abs) 14] sum*(X, x) >= /\z.add(x, z) because [15], by (F-Abs) 15] sum*(X, x, y) >= add(x, y) because sum > add, [16] and [18], by (Copy) 16] sum*(X, x, y) >= x because [17], by (Select) 17] x >= x by (Var) 18] sum*(X, x, y) >= y because [19], by (Select) 19] y >= y by (Var) 20] sum*(X) >= _|_ by (Bot) 21] sum*(X) >= X because [22], by (Select) 22] X >= X by (Meta) We can thus remove the following rules: times(0, X) => 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]): times(s(X), Y) >? plus(times(X, Y), Y) sum(X) >? fold(/\x./\y.add(x, y), 0, X) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {add, fold, plus, s, sum, times}, and the following precedence: sum > times > plus > fold > s > add Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: times(s(X), Y) >= plus(times(X, Y), Y) sum(X) > fold(/\x./\y.add(x, y), _|_, X) With these choices, we have: 1] times(s(X), Y) >= plus(times(X, Y), Y) because [2], by (Star) 2] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [3] and [8], by (Copy) 3] times*(s(X), Y) >= times(X, Y) because times in Mul, [4] and [7], by (Stat) 4] s(X) > X because [5], by definition 5] s*(X) >= X because [6], by (Select) 6] X >= X by (Meta) 7] Y >= Y by (Meta) 8] times*(s(X), Y) >= Y because [7], by (Select) 9] sum(X) > fold(/\x./\y.add(x, y), _|_, X) because [10], by definition 10] sum*(X) >= fold(/\x./\y.add(x, y), _|_, X) because sum > fold, [11], [18] and [19], by (Copy) 11] sum*(X) >= /\y./\z.add(y, z) because [12], by (F-Abs) 12] sum*(X, x) >= /\z.add(x, z) because [13], by (F-Abs) 13] sum*(X, x, y) >= add(x, y) because sum > add, [14] and [16], by (Copy) 14] sum*(X, x, y) >= x because [15], by (Select) 15] x >= x by (Var) 16] sum*(X, x, y) >= y because [17], by (Select) 17] y >= y by (Var) 18] sum*(X) >= _|_ by (Bot) 19] sum*(X) >= X because [20], by (Select) 20] X >= X by (Meta) We can thus remove the following rules: sum(X) => fold(/\x./\y.add(x, y), 0, 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]): times(s(X), Y) >? plus(times(X, Y), Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {plus, s, times}, and the following precedence: times > s > plus With these choices, we have: 1] times(s(X), Y) > plus(times(X, Y), Y) because [2], by definition 2] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [3] and [8], by (Copy) 3] times*(s(X), Y) >= times(X, Y) because times in Mul, [4] and [7], by (Stat) 4] s(X) > X because [5], by definition 5] s*(X) >= X because [6], by (Select) 6] X >= X by (Meta) 7] Y >= Y by (Meta) 8] times*(s(X), Y) >= Y because [7], by (Select) We can thus remove the following rules: times(s(X), Y) => plus(times(X, Y), 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 +++ [Kop11] C. Kop. Simplifying Algebraic Functional Systems. In Proceedings of CAI 2011, volume 6742 of LNCS. 201--215, Springer, 2011. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.