We consider the system kop11cai1. Alphabet: 0 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) pow(f, 0) => /\x.x pow(f, s(x)) => op(f, pow(f, x)) op(f, g) x => f (g x) /\x.f x => f 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 : [] --> nat cons : [nat * list] --> list map : [nat -> nat * list] --> list nil : [] --> list op : [nat -> nat * nat -> nat] --> nat -> nat pow : [nat -> nat * nat] --> nat -> nat s : [nat] --> nat ~AP1 : [nat -> nat * nat] --> nat ~L1 : [nat -> nat] --> nat -> nat Rules: map(F, nil) => nil map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) pow(F, 0) => ~L1(/\x.x) pow(F, s(X)) => op(F, pow(F, X)) op(F, G) X => ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) => F ~L1(/\x.op(F, G) x) => op(F, G) ~AP1(F, X) => F X ~L1(F) => F We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, nil) >? nil map(F, cons(X, Y)) >? cons(~AP1(F, X), map(F, Y)) pow(F, 0) >? ~L1(/\x.x) pow(F, s(X)) >? op(F, pow(F, X)) op(F, G) X >? ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >? F ~L1(/\x.op(F, G) x) >? op(F, G) ~AP1(F, X) >? F X ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {0, @_{o -> o}, cons, map, op, pow, s, ~AP1, ~L1}, and the following precedence: 0 > pow > s > ~L1 > op > map = ~AP1 > @_{o -> o} > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ map(F, cons(X, Y)) > cons(~AP1(F, X), map(F, Y)) pow(F, 0) > ~L1(/\x.x) pow(F, s(X)) >= op(F, pow(F, X)) @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) ~AP1(F, X) > @_{o -> o}(F, X) ~L1(F) >= F With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] map(F, cons(X, Y)) > cons(~AP1(F, X), map(F, Y)) because [3], by definition 3] map*(F, cons(X, Y)) >= cons(~AP1(F, X), map(F, Y)) because map > cons, [4] and [9], by (Copy) 4] map*(F, cons(X, Y)) >= ~AP1(F, X) because map = ~AP1, map in Mul, [5] and [6], by (Stat) 5] F >= F by (Meta) 6] cons(X, Y) > X because [7], by definition 7] cons*(X, Y) >= X because [8], by (Select) 8] X >= X by (Meta) 9] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [5] and [10], by (Stat) 10] cons(X, Y) > Y because [11], by definition 11] cons*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] pow(F, 0) > ~L1(/\x.x) because [14], by definition 14] pow*(F, 0) >= ~L1(/\x.x) because pow > ~L1 and [15], by (Copy) 15] pow*(F, 0) >= /\y.y because [16], by (F-Abs) 16] pow*(F, 0, x) >= x because [17], by (Select) 17] x >= x by (Var) 18] pow(F, s(X)) >= op(F, pow(F, X)) because [19], by (Star) 19] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [20] and [22], by (Copy) 20] pow*(F, s(X)) >= F because [21], by (Select) 21] F >= F by (Meta) 22] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [23] and [24], by (Stat) 23] F >= F by (Meta) 24] s(X) > X because [25], by definition 25] s*(X) >= X because [26], by (Select) 26] X >= X by (Meta) 27] @_{o -> o}(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [28], by (Star) 28] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [29], by (Select) 29] op(F, G) @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because [30] 30] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(F, ~AP1(G, X)) because op > ~AP1, [31] and [33], by (Copy) 31] op*(F, G, @_{o -> o}*(op(F, G), X)) >= F because [32], by (Select) 32] F >= F by (Meta) 33] op*(F, G, @_{o -> o}*(op(F, G), X)) >= ~AP1(G, X) because op > ~AP1, [34] and [36], by (Copy) 34] op*(F, G, @_{o -> o}*(op(F, G), X)) >= G because [35], by (Select) 35] G >= G by (Meta) 36] op*(F, G, @_{o -> o}*(op(F, G), X)) >= X because [37], by (Select) 37] @_{o -> o}*(op(F, G), X) >= X because [38], by (Select) 38] X >= X by (Meta) 39] ~L1(/\x.~AP1(F, x)) >= F because [40], by (Star) 40] ~L1*(/\x.~AP1(F, x)) >= F because [41], by (Select) 41] /\x.~AP1(F, x) >= F because [42], by (Eta)[Kop13:2] 42] F >= F by (Meta) 43] ~L1(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because [44], by (Star) 44] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because ~L1 > op, [45] and [50], by (Copy) 45] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= F because [46], by (Select) 46] /\x.@_{o -> o}(op(F, G), x) >= F because [47], by (Eta)[Kop13:2] 47] op(F, G) >= F because [48], by (Star) 48] op*(F, G) >= F because [49], by (Select) 49] F >= F by (Meta) 50] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= G because [51], by (Select) 51] /\x.@_{o -> o}(op(F, G), x) >= G because [52], by (Eta)[Kop13:2] 52] op(F, G) >= G because [53], by (Star) 53] op*(F, G) >= G because [54], by (Select) 54] G >= G by (Meta) 55] ~AP1(F, X) > @_{o -> o}(F, X) because [56], by definition 56] ~AP1*(F, X) >= @_{o -> o}(F, X) because ~AP1 > @_{o -> o}, [57] and [59], by (Copy) 57] ~AP1*(F, X) >= F because [58], by (Select) 58] F >= F by (Meta) 59] ~AP1*(F, X) >= X because [60], by (Select) 60] X >= X by (Meta) 61] ~L1(F) >= F because [62], by (Star) 62] ~L1*(F) >= F because [63], by (Select) 63] F >= F by (Meta) We can thus remove the following rules: map(F, cons(X, Y)) => cons(~AP1(F, X), map(F, Y)) pow(F, 0) => ~L1(/\x.x) ~AP1(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]): map(F, nil) >? nil pow(F, s(X)) >? op(F, pow(F, X)) op(F, G) X >? ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >? F ~L1(/\x.op(F, G) x) >? op(F, G) ~L1(F) >? F We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[nil]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, map, op, pow, s, ~AP1, ~L1}, and the following precedence: map > pow > s > ~L1 > @_{o -> o} > ~AP1 > op Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ pow(F, s(X)) > op(F, pow(F, X)) @_{o -> o}(op(F, G), X) > ~AP1(F, ~AP1(G, X)) ~L1(/\x.~AP1(F, x)) >= F ~L1(/\x.@_{o -> o}(op(F, G), x)) > op(F, G) ~L1(F) >= F With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] pow(F, s(X)) > op(F, pow(F, X)) because [3], by definition 3] pow*(F, s(X)) >= op(F, pow(F, X)) because pow > op, [4] and [6], by (Copy) 4] pow*(F, s(X)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] pow*(F, s(X)) >= pow(F, X) because pow in Mul, [7] and [8], by (Stat) 7] F >= F by (Meta) 8] s(X) > X because [9], by definition 9] s*(X) >= X because [10], by (Select) 10] X >= X by (Meta) 11] @_{o -> o}(op(F, G), X) > ~AP1(F, ~AP1(G, X)) because [12], by definition 12] @_{o -> o}*(op(F, G), X) >= ~AP1(F, ~AP1(G, X)) because @_{o -> o} > ~AP1, [13] and [17], by (Copy) 13] @_{o -> o}*(op(F, G), X) >= F because [14], by (Select) 14] op(F, G) >= F because [15], by (Star) 15] op*(F, G) >= F because [16], by (Select) 16] F >= F by (Meta) 17] @_{o -> o}*(op(F, G), X) >= ~AP1(G, X) because @_{o -> o} > ~AP1, [18] and [22], by (Copy) 18] @_{o -> o}*(op(F, G), X) >= G because [19], by (Select) 19] op(F, G) >= G because [20], by (Star) 20] op*(F, G) >= G because [21], by (Select) 21] G >= G by (Meta) 22] @_{o -> o}*(op(F, G), X) >= X because [23], by (Select) 23] X >= X by (Meta) 24] ~L1(/\x.~AP1(F, x)) >= F because [25], by (Star) 25] ~L1*(/\x.~AP1(F, x)) >= F because [26], by (Select) 26] /\x.~AP1(F, x) >= F because [27], by (Eta)[Kop13:2] 27] F >= F by (Meta) 28] ~L1(/\x.@_{o -> o}(op(F, G), x)) > op(F, G) because [29], by definition 29] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= op(F, G) because ~L1 > op, [30] and [35], by (Copy) 30] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= F because [31], by (Select) 31] /\x.@_{o -> o}(op(F, G), x) >= F because [32], by (Eta)[Kop13:2] 32] op(F, G) >= F because [33], by (Star) 33] op*(F, G) >= F because [34], by (Select) 34] F >= F by (Meta) 35] ~L1*(/\x.@_{o -> o}(op(F, G), x)) >= G because [36], by (Select) 36] /\x.@_{o -> o}(op(F, G), x) >= G because [37], by (Eta)[Kop13:2] 37] op(F, G) >= G because [38], by (Star) 38] op*(F, G) >= G because [39], by (Select) 39] G >= G by (Meta) 40] ~L1(F) >= F because [41], by (Star) 41] ~L1*(F) >= F because [42], by (Select) 42] F >= F by (Meta) We can thus remove the following rules: pow(F, s(X)) => op(F, pow(F, X)) op(F, G) X => ~AP1(F, ~AP1(G, X)) ~L1(/\x.op(F, G) x) => op(F, G) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, nil) >? nil ~L1(/\x.~AP1(F, x)) >? F ~L1(F) >? F We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: map = \G0y1.3 + 3y1 + G0(0) nil = 0 ~AP1 = \G0y1.3 + y1 + G0(y1) ~L1 = \G0y1.3 + G0(y1) Using this interpretation, the requirements translate to: [[map(_F0, nil)]] = 3 + F0(0) > 0 = [[nil]] [[~L1(/\x.~AP1(_F0, x))]] = \y0.6 + y0 + F0(y0) > \y0.F0(y0) = [[_F0]] [[~L1(_F0)]] = \y0.3 + F0(y0) > \y0.F0(y0) = [[_F0]] We can thus remove the following rules: map(F, nil) => nil ~L1(/\x.~AP1(F, x)) => F ~L1(F) => F 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. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.