We consider the system h01. 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 xap : [a -> c -> c * a] --> c -> c yap : [c -> c * c] --> c Rules: fold(/\x./\y.yap(xap(f, x), y), z) nil => z fold(/\x./\y.yap(xap(f, x), y), z) cons(u, v) => yap(xap(f, u), fold(/\w./\x'.yap(xap(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 => fold(/\x./\y.yap(xap(add, x), y), 0) prod => fold(/\x./\y.yap(xap(mul, x), y), s(0)) 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 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 yap : [c -> c * c] --> c Rules: fold(/\x./\y.yap(F(x), y), X) nil => X fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) => yap(F(Y), fold(/\z./\u.yap(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 => fold(/\x./\y.yap(add(x), y), 0) prod => fold(/\x./\y.yap(mul(x), y), s(0)) 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), X) nil >? X fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) >? yap(F(Y), fold(/\z./\u.yap(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 >? fold(/\x./\y.yap(add(x), y), 0) prod >? fold(/\x./\y.yap(mul(x), y), s(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, cons, fold, mul, nil, plus, prod, s, sum, times, yap}, and the following precedence: sum > prod > yap > nil > mul > fold > times > plus > s > @_{o -> o} > cons > add Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) >= X @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) > yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) plus(_|_, X) >= X plus(s(X), Y) > s(plus(X, Y)) times(_|_, X) >= _|_ times(s(X), Y) > plus(times(X, Y), Y) sum > fold(/\x./\y.yap(add(x), y), _|_) prod >= fold(/\x./\y.yap(mul(x), y), s(_|_)) yap(F, X) >= @_{o -> o}(F, X) With these choices, we have: 1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) >= X because [2], by (Star) 2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X because [3], by (Select) 3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X because [4] 4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X because [5], by (Select) 5] X >= X by (Meta) 6] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) > yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) because [7], by definition 7] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) because [8], by (Select) 8] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) because [9] 9] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) because [10], by (Select) 10] yap(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= yap(F(Y), @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z)) because yap in Mul, [11] and [17], by (Fun) 11] F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))) >= F(Y) because [12], by (Meta) 12] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= Y because [13], by (Select) 13] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= Y because [14], by (Select) 14] cons(Y, Z) >= Y because [15], by (Star) 15] cons*(Y, Z) >= Y because [16], by (Select) 16] Y >= Y by (Meta) 17] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z) because [18], by (Select) 18] yap(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z) because [19], by (Star) 19] yap*(F(fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z)))), fold*(/\v./\w.yap(F(v), w), X, @_{o -> o}*(fold(/\x'./\y'.yap(F(x'), y'), X), cons(Y, Z)))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z) because [20], by (Select) 20] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), cons(Y, Z))) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z) because [21], by (Select) 21] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), cons(Y, Z)) >= @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), Z) because @_{o -> o} in Mul, [22] and [30], by (Stat) 22] fold(/\x./\y.yap(F(x), y), X) >= fold(/\x./\y.yap(F(x), y), X) because fold in Mul, [23] and [29], by (Fun) 23] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [24], by (Abs) 24] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [25], by (Abs) 25] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [26] and [28], by (Fun) 26] F(y) >= F(y) because [27], by (Meta) 27] y >= y by (Var) 28] x >= x by (Var) 29] X >= X by (Meta) 30] cons(Y, Z) > Z because [31], by definition 31] cons*(Y, Z) >= Z because [32], by (Select) 32] Z >= Z by (Meta) 33] plus(_|_, X) >= X because [34], by (Star) 34] plus*(_|_, X) >= X because [35], by (Select) 35] X >= X by (Meta) 36] plus(s(X), Y) > s(plus(X, Y)) because [37], by definition 37] plus*(s(X), Y) >= s(plus(X, Y)) because plus > s and [38], by (Copy) 38] plus*(s(X), Y) >= plus(X, Y) because plus in Mul, [39] and [42], by (Stat) 39] s(X) > X because [40], by definition 40] s*(X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] Y >= Y by (Meta) 43] times(_|_, X) >= _|_ by (Bot) 44] times(s(X), Y) > plus(times(X, Y), Y) because [45], by definition 45] times*(s(X), Y) >= plus(times(X, Y), Y) because times > plus, [46] and [51], by (Copy) 46] times*(s(X), Y) >= times(X, Y) because times in Mul, [47] and [50], by (Stat) 47] s(X) > X because [48], by definition 48] s*(X) >= X because [49], by (Select) 49] X >= X by (Meta) 50] Y >= Y by (Meta) 51] times*(s(X), Y) >= Y because [50], by (Select) 52] sum > fold(/\x./\y.yap(add(x), y), _|_) because [53], by definition 53] sum* >= fold(/\x./\y.yap(add(x), y), _|_) because sum > fold, [54] and [62], by (Copy) 54] sum* >= /\y./\z.yap(add(y), z) because [55], by (F-Abs) 55] sum*(x) >= /\z.yap(add(x), z) because [56], by (F-Abs) 56] sum*(x, y) >= yap(add(x), y) because sum > yap, [57] and [60], by (Copy) 57] sum*(x, y) >= add(x) because sum > add and [58], by (Copy) 58] sum*(x, y) >= x because [59], by (Select) 59] x >= x by (Var) 60] sum*(x, y) >= y because [61], by (Select) 61] y >= y by (Var) 62] sum* >= _|_ by (Bot) 63] prod >= fold(/\x./\y.yap(mul(x), y), s(_|_)) because [64], by (Star) 64] prod* >= fold(/\x./\y.yap(mul(x), y), s(_|_)) because prod > fold, [65] and [73], by (Copy) 65] prod* >= /\y./\z.yap(mul(y), z) because [66], by (F-Abs) 66] prod*(x) >= /\z.yap(mul(x), z) because [67], by (F-Abs) 67] prod*(x, y) >= yap(mul(x), y) because prod > yap, [68] and [71], by (Copy) 68] prod*(x, y) >= mul(x) because prod > mul and [69], by (Copy) 69] prod*(x, y) >= x because [70], by (Select) 70] x >= x by (Var) 71] prod*(x, y) >= y because [72], by (Select) 72] y >= y by (Var) 73] prod* >= s(_|_) because prod > s and [74], by (Copy) 74] prod* >= _|_ by (Bot) 75] yap(F, X) >= @_{o -> o}(F, X) because [76], by (Star) 76] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [77] and [79], by (Copy) 77] yap*(F, X) >= F because [78], by (Select) 78] F >= F by (Meta) 79] yap*(F, X) >= X because [80], by (Select) 80] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.yap(F(x), y), X) cons(Y, Z) => yap(F(Y), fold(/\z./\u.yap(F(z), u), X) Z) plus(s(X), Y) => s(plus(X, Y)) times(s(X), Y) => plus(times(X, Y), Y) sum => fold(/\x./\y.yap(add(x), y), 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), X) nil >? X plus(0, X) >? X times(0, X) >? 0 prod >? fold(/\x./\y.yap(mul(x), y), s(0)) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[s(x_1)]] = x_1 We choose Lex = {} and Mul = {@_{o -> o}, fold, mul, nil, plus, prod, times, yap}, and the following precedence: prod > fold > yap > mul > nil > @_{o -> o} > times > plus Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) > X plus(_|_, X) >= X times(_|_, X) > _|_ prod > fold(/\x./\y.yap(mul(x), y), _|_) yap(F, X) > @_{o -> o}(F, X) With these choices, we have: 1] @_{o -> o}(fold(/\x./\y.yap(F(x), y), X), nil) > X because [2], by definition 2] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X because [3], by (Select) 3] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X because [4] 4] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X because [5], by (Select) 5] @_{o -> o}*(fold(/\x./\y.yap(F(x), y), X), nil) >= X because [6], by (Select) 6] fold(/\x./\y.yap(F(x), y), X) @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil) >= X because [7] 7] fold*(/\x./\y.yap(F(x), y), X, @_{o -> o}*(fold(/\z./\u.yap(F(z), u), X), nil)) >= X because [8], by (Select) 8] X >= X by (Meta) 9] plus(_|_, X) >= X because [10], by (Star) 10] plus*(_|_, X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] times(_|_, X) > _|_ because [13], by definition 13] times*(_|_, X) >= _|_ by (Bot) 14] prod > fold(/\x./\y.yap(mul(x), y), _|_) because [15], by definition 15] prod* >= fold(/\x./\y.yap(mul(x), y), _|_) because prod > fold, [16] and [24], by (Copy) 16] prod* >= /\y./\z.yap(mul(y), z) because [17], by (F-Abs) 17] prod*(x) >= /\z.yap(mul(x), z) because [18], by (F-Abs) 18] prod*(x, y) >= yap(mul(x), y) because prod > yap, [19] and [22], by (Copy) 19] prod*(x, y) >= mul(x) because prod > mul and [20], by (Copy) 20] prod*(x, y) >= x because [21], by (Select) 21] x >= x by (Var) 22] prod*(x, y) >= y because [23], by (Select) 23] y >= y by (Var) 24] prod* >= _|_ by (Bot) 25] yap(F, X) > @_{o -> o}(F, X) because [26], by definition 26] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [27] and [29], by (Copy) 27] yap*(F, X) >= F because [28], by (Select) 28] F >= F by (Meta) 29] yap*(F, X) >= X because [30], by (Select) 30] X >= X by (Meta) We can thus remove the following rules: fold(/\x./\y.yap(F(x), y), X) nil => X times(0, X) => 0 prod => fold(/\x./\y.yap(mul(x), y), s(0)) 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]): plus(0, X) >? X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, plus}, and the following precedence: 0 > plus With these choices, we have: 1] plus(0, X) > X because [2], by definition 2] plus*(0, X) >= X because [3], by (Select) 3] X >= X by (Meta) We can thus remove the following rules: plus(0, 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.