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: times > sum > prod > fold > mul > cons > add > plus > s > nil 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 definition 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) > _|_ because [32], by definition 32] times*(_|_, X) >= _|_ by (Bot) 33] times(s(X), Y) >= plus(times(X, Y), Y) because [34], by (Star) 34] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [35] and [40], by (Copy) 35] times*(s(X), Y) >= times(X, Y) because times in Mul, [36] and [39], by (Stat) 36] s(X) > X because [37], by definition 37] s*(X) >= X because [38], by (Select) 38] X >= X by (Meta) 39] Y >= Y by (Meta) 40] times*(s(X), Y) >= Y because [39], by (Select) 41] sum(X) > fold(/\x./\y.add(x, y), _|_, X) because [42], by definition 42] sum*(X) >= fold(/\x./\y.add(x, y), _|_, X) because sum > fold, [43], [50] and [51], by (Copy) 43] sum*(X) >= /\y./\z.add(y, z) because [44], by (F-Abs) 44] sum*(X, x) >= /\z.add(x, z) because [45], by (F-Abs) 45] sum*(X, x, y) >= add(x, y) because sum > add, [46] and [48], by (Copy) 46] sum*(X, x, y) >= x because [47], by (Select) 47] x >= x by (Var) 48] sum*(X, x, y) >= y because [49], by (Select) 49] y >= y by (Var) 50] sum*(X) >= _|_ by (Bot) 51] sum*(X) >= X because [52], by (Select) 52] X >= X by (Meta) 53] prod(X) >= fold(/\x./\y.mul(x, y), s(_|_), X) because [54], by (Star) 54] prod*(X) >= fold(/\x./\y.mul(x, y), s(_|_), X) because prod > fold, [55], [62] and [64], by (Copy) 55] prod*(X) >= /\y./\z.mul(y, z) because [56], by (F-Abs) 56] prod*(X, x) >= /\z.mul(x, z) because [57], by (F-Abs) 57] prod*(X, x, y) >= mul(x, y) because prod > mul, [58] and [60], by (Copy) 58] prod*(X, x, y) >= x because [59], by (Select) 59] x >= x by (Var) 60] prod*(X, x, y) >= y because [61], by (Select) 61] y >= y by (Var) 62] prod*(X) >= s(_|_) because prod > s and [63], by (Copy) 63] prod*(X) >= _|_ by (Bot) 64] prod*(X) >= X because [65], by (Select) 65] X >= X by (Meta) We can thus remove the following 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 times(0, X) => 0 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]): plus(s(X), Y) >? s(plus(X, Y)) times(s(X), Y) >? plus(times(X, Y), Y) 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 = {fold, mul, plus, prod, s, times}, and the following precedence: times > plus > prod > mul > fold > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: plus(s(X), Y) >= s(plus(X, Y)) times(s(X), Y) >= plus(times(X, Y), Y) prod(X) > fold(/\x./\y.mul(x, y), s(_|_), X) With these choices, we have: 1] plus(s(X), Y) >= s(plus(X, Y)) because [2], by (Star) 2] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [3], by (Copy) 3] plus*(s(X), Y) >= plus(X, Y) because plus 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) >= plus(times(X, Y), Y) because [9], by (Star) 9] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [10] and [15], by (Copy) 10] times*(s(X), Y) >= times(X, Y) because times in Mul, [11] and [14], by (Stat) 11] s(X) > X because [12], by definition 12] s*(X) >= X because [13], by (Select) 13] X >= X by (Meta) 14] Y >= Y by (Meta) 15] times*(s(X), Y) >= Y because [14], by (Select) 16] prod(X) > fold(/\x./\y.mul(x, y), s(_|_), X) because [17], by definition 17] prod*(X) >= fold(/\x./\y.mul(x, y), s(_|_), X) because prod > fold, [18], [25] and [27], by (Copy) 18] prod*(X) >= /\y./\z.mul(y, z) because [19], by (F-Abs) 19] prod*(X, x) >= /\z.mul(x, z) because [20], by (F-Abs) 20] prod*(X, x, y) >= mul(x, y) because prod > mul, [21] and [23], by (Copy) 21] prod*(X, x, y) >= x because [22], by (Select) 22] x >= x by (Var) 23] prod*(X, x, y) >= y because [24], by (Select) 24] y >= y by (Var) 25] prod*(X) >= s(_|_) because prod > s and [26], by (Copy) 26] prod*(X) >= _|_ by (Bot) 27] prod*(X) >= X because [28], by (Select) 28] X >= X by (Meta) We can thus remove the following rules: 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]): plus(s(X), Y) >? s(plus(X, Y)) 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 > plus > s With these choices, we have: 1] plus(s(X), Y) >= s(plus(X, Y)) because [2], by (Star) 2] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [3], by (Copy) 3] plus*(s(X), Y) >= plus(X, Y) because plus 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) > plus(times(X, Y), Y) because [9], by definition 9] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [10] and [15], by (Copy) 10] times*(s(X), Y) >= times(X, Y) because times in Mul, [11] and [14], by (Stat) 11] s(X) > X because [12], by definition 12] s*(X) >= X because [13], by (Select) 13] X >= X by (Meta) 14] Y >= Y by (Meta) 15] times*(s(X), Y) >= Y because [14], by (Select) We can thus remove the following rules: times(s(X), Y) => plus(times(X, Y), 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]): plus(s(X), Y) >? s(plus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {plus, s}, and the following precedence: plus > s With these choices, we have: 1] plus(s(X), Y) > s(plus(X, Y)) because [2], by definition 2] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [3], by (Copy) 3] plus*(s(X), Y) >= plus(X, Y) because plus 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) We can thus remove the following rules: plus(s(X), Y) => s(plus(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 +++ [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.