We consider the system filter. Alphabet: 0 : [] --> nat bool : [nat] --> boolean cons : [nat * list] --> list consif : [boolean * nat * list] --> list false : [] --> boolean filter : [nat -> boolean * list] --> list nil : [] --> list rand : [nat] --> nat s : [nat] --> nat true : [] --> boolean Rules: rand(x) => x rand(s(x)) => rand(x) bool(0) => false bool(s(0)) => true filter(f, nil) => nil filter(f, cons(x, y)) => consif(f x, x, filter(f, y)) consif(true, x, y) => cons(x, y) consif(false, x, y) => y This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]). We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] rand#(s(X)) =#> rand#(X) 1] filter#(F, cons(X, Y)) =#> consif#(F X, X, filter(F, Y)) 2] filter#(F, cons(X, Y)) =#> filter#(F, Y) Rules R_0: rand(X) => X rand(s(X)) => rand(X) bool(0) => false bool(s(0)) => true filter(F, nil) => nil filter(F, cons(X, Y)) => consif(F X, X, filter(F, Y)) consif(true, X, Y) => cons(X, Y) consif(false, X, Y) => Y Thus, the original system is terminating if (P_0, R_0, static, formative) is finite. We consider the dependency pair problem (P_0, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: rand#(s(X)) >? rand#(X) filter#(F, cons(X, Y)) >? consif#(F X, X, filter(F, Y)) filter#(F, cons(X, Y)) >? filter#(F, Y) rand(X) >= X rand(s(X)) >= rand(X) bool(0) >= false bool(s(0)) >= true filter(F, nil) >= nil filter(F, cons(X, Y)) >= consif(F X, X, filter(F, Y)) consif(true, X, Y) >= cons(X, Y) consif(false, X, Y) >= Y We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 bool = \y0.3 cons = \y0y1.2y1 consif = \y0y1y2.2y2 consif# = \y0y1y2.0 false = 0 filter = \G0y1.0 filter# = \G0y1.3 + y1 + 2y1G0(y1) nil = 0 rand = \y0.y0 rand# = \y0.0 s = \y0.3 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[rand#(s(_x0))]] = 0 >= 0 = [[rand#(_x0)]] [[filter#(_F0, cons(_x1, _x2))]] = 3 + 2x2 + 4x2F0(2x2) > 0 = [[consif#(_F0 _x1, _x1, filter(_F0, _x2))]] [[filter#(_F0, cons(_x1, _x2))]] = 3 + 2x2 + 4x2F0(2x2) >= 3 + x2 + 2x2F0(x2) = [[filter#(_F0, _x2)]] [[rand(_x0)]] = x0 >= x0 = [[_x0]] [[rand(s(_x0))]] = 3 + 2x0 >= x0 = [[rand(_x0)]] [[bool(0)]] = 3 >= 0 = [[false]] [[bool(s(0))]] = 3 >= 0 = [[true]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[consif(_F0 _x1, _x1, filter(_F0, _x2))]] [[consif(true, _x0, _x1)]] = 2x1 >= 2x1 = [[cons(_x0, _x1)]] [[consif(false, _x0, _x1)]] = 2x1 >= x1 = [[_x1]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, static, formative) by (P_1, R_0, static, formative), where P_1 consists of: rand#(s(X)) =#> rand#(X) filter#(F, cons(X, Y)) =#> filter#(F, Y) Thus, the original system is terminating if (P_1, R_0, static, formative) is finite. We consider the dependency pair problem (P_1, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: rand#(s(X)) >? rand#(X) filter#(F, cons(X, Y)) >? filter#(F, Y) rand(X) >= X rand(s(X)) >= rand(X) bool(0) >= false bool(s(0)) >= true filter(F, nil) >= nil filter(F, cons(X, Y)) >= consif(F X, X, filter(F, Y)) consif(true, X, Y) >= cons(X, Y) consif(false, X, Y) >= Y We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 bool = \y0.3 cons = \y0y1.2y1 consif = \y0y1y2.2y2 false = 0 filter = \G0y1.0 filter# = \G0y1.2y1 nil = 0 rand = \y0.2y0 rand# = \y0.y0 s = \y0.3 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[rand#(s(_x0))]] = 3 + 2x0 > x0 = [[rand#(_x0)]] [[filter#(_F0, cons(_x1, _x2))]] = 4x2 >= 2x2 = [[filter#(_F0, _x2)]] [[rand(_x0)]] = 2x0 >= x0 = [[_x0]] [[rand(s(_x0))]] = 6 + 4x0 >= 2x0 = [[rand(_x0)]] [[bool(0)]] = 3 >= 0 = [[false]] [[bool(s(0))]] = 3 >= 0 = [[true]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, cons(_x1, _x2))]] = 0 >= 0 = [[consif(_F0 _x1, _x1, filter(_F0, _x2))]] [[consif(true, _x0, _x1)]] = 2x1 >= 2x1 = [[cons(_x0, _x1)]] [[consif(false, _x0, _x1)]] = 2x1 >= x1 = [[_x1]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, static, formative) by (P_2, R_0, static, formative), where P_2 consists of: filter#(F, cons(X, Y)) =#> filter#(F, Y) Thus, the original system is terminating if (P_2, R_0, static, formative) is finite. We consider the dependency pair problem (P_2, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: filter#(F, cons(X, Y)) >? filter#(F, Y) rand(X) >= X rand(s(X)) >= rand(X) bool(0) >= false bool(s(0)) >= true filter(F, nil) >= nil filter(F, cons(X, Y)) >= consif(F X, X, filter(F, Y)) consif(true, X, Y) >= cons(X, Y) consif(false, X, Y) >= Y We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 bool = \y0.3 cons = \y0y1.1 + y1 consif = \y0y1y2.1 + y2 false = 0 filter = \G0y1.2y1 filter# = \G0y1.2y1 nil = 0 rand = \y0.y0 s = \y0.3 + 2y0 true = 0 Using this interpretation, the requirements translate to: [[filter#(_F0, cons(_x1, _x2))]] = 2 + 2x2 > 2x2 = [[filter#(_F0, _x2)]] [[rand(_x0)]] = x0 >= x0 = [[_x0]] [[rand(s(_x0))]] = 3 + 2x0 >= x0 = [[rand(_x0)]] [[bool(0)]] = 3 >= 0 = [[false]] [[bool(s(0))]] = 3 >= 0 = [[true]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, cons(_x1, _x2))]] = 2 + 2x2 >= 1 + 2x2 = [[consif(_F0 _x1, _x1, filter(_F0, _x2))]] [[consif(true, _x0, _x1)]] = 1 + x1 >= 1 + x1 = [[cons(_x0, _x1)]] [[consif(false, _x0, _x1)]] = 1 + x1 >= x1 = [[_x1]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13] C. Kop. Static Dependency Pairs with Accessibility. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013. [KusIsoSakBla09] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems. In volume 92(10) of IEICE Transactions on Information and Systems. 2007--2015, 2009.