We consider the system h03. 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 xap : [c -> a -> c * c] --> a -> c yap : [a -> c * a] --> c Rules: fold(/\x./\y.yap(xap(f, x), y), nil, z) => z fold(/\x./\y.yap(xap(f, x), y), cons(z, u), v) => fold(/\w./\x'.yap(xap(f, w), x'), u, yap(xap(f, v), z)) sum(x) => fold(/\y./\z.yap(xap(add, y), z), x, 0) fold(mul, x, 1) => prod(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 : [] --> 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 yap : [a -> c * a] --> c Rules: fold(/\x./\y.yap(F(x), y), nil, X) => X fold(/\x./\y.yap(F(x), y), cons(X, Y), Z) => fold(/\z./\u.yap(F(z), u), Y, yap(F(Z), X)) sum(X) => fold(/\x./\y.yap(add(x), y), X, 0) fold(mul, X, 1) => prod(X) yap(F, X) => F 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.yap(F(x), y), nil, X) >? X fold(/\x./\y.yap(F(x), y), cons(X, Y), Z) >? fold(/\z./\u.yap(F(z), u), Y, yap(F(Z), X)) sum(X) >? fold(/\x./\y.yap(add(x), y), X, 0) fold(mul, X, 1) >? prod(X) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[fold(x_1, x_2, x_3)]] = fold(x_2, x_3, x_1) We choose Lex = {fold} and Mul = {1, @_{o -> o}, add, cons, mul, nil, prod, sum, yap}, and the following precedence: 1 = cons > nil > sum > add > fold > prod > @_{o -> o} = yap > mul Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold(/\x./\y.yap(F(x), y), nil, X) >= X fold(/\x./\y.yap(F(x), y), cons(X, Y), Z) > fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) sum(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) fold(mul, X, 1) > prod(X) yap(F, X) >= @_{o -> o}(F, X) With these choices, we have: 1] fold(/\x./\y.yap(F(x), y), nil, X) >= X because [2], by (Star) 2] fold*(/\x./\y.yap(F(x), y), nil, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] fold(/\x./\y.yap(F(x), y), cons(X, Y), Z) > fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) because [5], by definition 5] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) because [6], by (Select) 6] yap(F(fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z)), fold*(/\z./\u.yap(F(z), u), cons(X, Y), Z)) >= fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) because [7], by (Star) 7] yap*(F(fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z)), fold*(/\z./\u.yap(F(z), u), cons(X, Y), Z)) >= fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) because [8], by (Select) 8] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= fold(/\x./\y.yap(F(x), y), Y, yap(F(Z), X)) because [9], [12], [22] and [24], by (Stat) 9] cons(X, Y) > Y because [10], by definition 10] cons*(X, Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= /\x./\y.yap(F(x), y) because [13], by (F-Abs) 13] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z) >= /\x.yap(F(z), x) because [14], by (F-Abs) 14] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z, u) >= yap(F(z), u) because fold > yap, [15] and [20], by (Copy) 15] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z, u) >= F(z) because [16], by (Select) 16] /\x.yap(F(fold*(/\y./\v.yap(F(y), v), cons(X, Y), Z, z, u)), x) >= F(z) because [17], by (Eta)[Kop13:2] 17] F(fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z, u)) >= F(z) because [18], by (Meta) 18] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z, u) >= z because [19], by (Select) 19] z >= z by (Var) 20] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z, z, u) >= u because [21], by (Select) 21] u >= u by (Var) 22] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= Y because [23], by (Select) 23] cons(X, Y) >= Y because [10], by (Star) 24] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= yap(F(Z), X) because fold > yap, [25] and [30], by (Copy) 25] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= F(Z) because [26], by (Select) 26] /\x.yap(F(fold*(/\y./\v.yap(F(y), v), cons(X, Y), Z)), x) >= F(Z) because [27], by (Eta)[Kop13:2] 27] F(fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z)) >= F(Z) because [28], by (Meta) 28] fold*(/\x./\y.yap(F(x), y), cons(X, Y), Z) >= Z because [29], by (Select) 29] Z >= Z by (Meta) 30] fold*(/\x./\y.yap(F(x), y), 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] sum(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) because [35], by (Star) 35] sum*(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) because sum > fold, [36], [44] and [46], by (Copy) 36] sum*(X) >= /\y./\z.yap(add(y), z) because [37], by (F-Abs) 37] sum*(X, x) >= /\z.yap(add(x), z) because [38], by (F-Abs) 38] sum*(X, x, y) >= yap(add(x), y) because sum > yap, [39] and [42], by (Copy) 39] sum*(X, x, y) >= add(x) because sum > add and [40], by (Copy) 40] sum*(X, x, y) >= x because [41], by (Select) 41] x >= x by (Var) 42] sum*(X, x, y) >= y because [43], by (Select) 43] y >= y by (Var) 44] sum*(X) >= X because [45], by (Select) 45] X >= X by (Meta) 46] sum*(X) >= _|_ by (Bot) 47] fold(mul, X, 1) > prod(X) because [48], by definition 48] fold*(mul, X, 1) >= prod(X) because fold > prod and [49], by (Copy) 49] fold*(mul, X, 1) >= X because [50], by (Select) 50] X >= X by (Meta) 51] yap(F, X) >= @_{o -> o}(F, X) because yap = @_{o -> o}, yap in Mul, [52] and [53], by (Fun) 52] F >= F by (Meta) 53] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.yap(F(x), y), cons(X, Y), Z) => fold(/\z./\u.yap(F(z), u), Y, yap(F(Z), X)) fold(mul, X, 1) => prod(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.yap(F(x), y), nil, X) >? X sum(X) >? fold(/\x./\y.yap(add(x), y), X, 0) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, fold, nil, sum, yap}, and the following precedence: sum > add > yap > fold > @_{o -> o} > nil Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold(/\x./\y.yap(F(x), y), nil, X) >= X sum(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) yap(F, X) > @_{o -> o}(F, X) With these choices, we have: 1] fold(/\x./\y.yap(F(x), y), nil, X) >= X because [2], by (Star) 2] fold*(/\x./\y.yap(F(x), y), nil, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] sum(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) because [5], by (Star) 5] sum*(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) because sum > fold, [6], [14] and [16], by (Copy) 6] sum*(X) >= /\y./\z.yap(add(y), z) because [7], by (F-Abs) 7] sum*(X, x) >= /\z.yap(add(x), z) because [8], by (F-Abs) 8] sum*(X, x, y) >= yap(add(x), y) because sum > yap, [9] and [12], by (Copy) 9] sum*(X, x, y) >= add(x) because sum > add and [10], by (Copy) 10] sum*(X, x, y) >= x because [11], by (Select) 11] x >= x by (Var) 12] sum*(X, x, y) >= y because [13], by (Select) 13] y >= y by (Var) 14] sum*(X) >= X because [15], by (Select) 15] X >= X by (Meta) 16] sum*(X) >= _|_ by (Bot) 17] yap(F, X) > @_{o -> o}(F, X) because [18], by definition 18] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [19] and [21], by (Copy) 19] yap*(F, X) >= F because [20], by (Select) 20] F >= F by (Meta) 21] yap*(F, X) >= X because [22], by (Select) 22] X >= X by (Meta) We can thus remove the following rules: yap(F, X) => F 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.yap(F(x), y), nil, X) >? X sum(X) >? fold(/\x./\y.yap(add(x), y), X, 0) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {add, fold, nil, sum, yap}, and the following precedence: nil > sum > yap > add > fold Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: fold(/\x./\y.yap(F(x), y), nil, X) >= X sum(X) > fold(/\x./\y.yap(add(x), y), X, _|_) With these choices, we have: 1] fold(/\x./\y.yap(F(x), y), nil, X) >= X because [2], by (Star) 2] fold*(/\x./\y.yap(F(x), y), nil, X) >= X because [3], by (Select) 3] X >= X by (Meta) 4] sum(X) > fold(/\x./\y.yap(add(x), y), X, _|_) because [5], by definition 5] sum*(X) >= fold(/\x./\y.yap(add(x), y), X, _|_) because sum > fold, [6], [14] and [16], by (Copy) 6] sum*(X) >= /\y./\z.yap(add(y), z) because [7], by (F-Abs) 7] sum*(X, x) >= /\z.yap(add(x), z) because [8], by (F-Abs) 8] sum*(X, x, y) >= yap(add(x), y) because sum > yap, [9] and [12], by (Copy) 9] sum*(X, x, y) >= add(x) because sum > add and [10], by (Copy) 10] sum*(X, x, y) >= x because [11], by (Select) 11] x >= x by (Var) 12] sum*(X, x, y) >= y because [13], by (Select) 13] y >= y by (Var) 14] sum*(X) >= X because [15], by (Select) 15] X >= X by (Meta) 16] sum*(X) >= _|_ by (Bot) We can thus remove the following rules: sum(X) => fold(/\x./\y.yap(add(x), y), 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]): fold(/\x./\y.yap(F(x), y), nil, X) >? X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {fold, nil, yap}, and the following precedence: fold > nil > yap With these choices, we have: 1] fold(/\x./\y.yap(F(x), y), nil, X) > X because [2], by definition 2] fold*(/\x./\y.yap(F(x), y), nil, X) >= X because [3], by (Select) 3] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.yap(F(x), y), nil, X) => X 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. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.