We consider the system sort. Alphabet: 0 : [] --> nat ascending!6220sort : [list] --> list cons : [nat * list] --> list descending!6220sort : [list] --> list insert : [nat * list * nat -> nat -> nat * nat -> nat -> nat] --> list max : [nat * nat] --> nat min : [nat * nat] --> nat nil : [] --> list s : [nat] --> nat sort : [list * nat -> nat -> nat * nat -> nat -> nat] --> list Rules: max(0, x) => x max(x, 0) => x max(s(x), s(y)) => s(max(x, y)) min(0, x) => 0 min(x, 0) => 0 min(s(x), s(y)) => s(min(x, y)) insert(x, nil, f, g) => cons(x, nil) insert(x, cons(y, z), f, g) => cons(f x y, insert(g x y, z, f, g)) sort(nil, f, g) => nil sort(cons(x, y), f, g) => insert(x, sort(y, f, g), f, g) ascending!6220sort(x) => sort(x, /\y./\z.min(y, z), /\u./\v.max(u, v)) descending!6220sort(x) => sort(x, /\y./\z.max(y, z), /\u./\v.min(u, v)) 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] max#(s(X), s(Y)) =#> max#(X, Y) 1] min#(s(X), s(Y)) =#> min#(X, Y) 2] insert#(X, cons(Y, Z), F, G) =#> insert#(G X Y, Z, F, G) 3] sort#(cons(X, Y), F, G) =#> insert#(X, sort(Y, F, G), F, G) 4] sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) 5] ascending!6220sort#(X) =#> sort#(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 6] ascending!6220sort#(X) =#> min#(Y, Z) 7] ascending!6220sort#(X) =#> max#(Y, Z) 8] descending!6220sort#(X) =#> sort#(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 9] descending!6220sort#(X) =#> max#(Y, Z) 10] descending!6220sort#(X) =#> min#(Y, Z) Rules R_0: max(0, X) => X max(X, 0) => X max(s(X), s(Y)) => s(max(X, Y)) min(0, X) => 0 min(X, 0) => 0 min(s(X), s(Y)) => s(min(X, Y)) insert(X, nil, F, G) => cons(X, nil) insert(X, cons(Y, Z), F, G) => cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) => nil sort(cons(X, Y), F, G) => insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) => sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : 0 * 1 : 1 * 2 : 2 * 3 : 2 * 4 : 3, 4 * 5 : 3, 4 * 6 : 1 * 7 : 0 * 8 : 3, 4 * 9 : 0 * 10 : 1 This graph has the following strongly connected components: P_1: max#(s(X), s(Y)) =#> max#(X, Y) P_2: min#(s(X), s(Y)) =#> min#(X, Y) P_3: insert#(X, cons(Y, Z), F, G) =#> insert#(G X Y, Z, F, G) P_4: sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) By [Kop12, Thm. 7.31], we may replace any dependency pair problem (P_0, R_0, m, f) by (P_1, R_0, m, f), (P_2, R_0, m, f), (P_3, R_0, m, f) and (P_4, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative), (P_3, R_0, static, formative) and (P_4, R_0, static, formative) is finite. We consider the dependency pair problem (P_4, 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: sort#(cons(X, Y), F, G) >? sort#(Y, F, G) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 0 ascending!6220sort = \y0.0 cons = \y0y1.1 + y1 descending!6220sort = \y0.0 insert = \y0y1G2G3.2 + y1 max = \y0y1.3 + 3y0 + 3y1 min = \y0y1.3 nil = 0 s = \y0.0 sort = \y0G1G2.1 + 3y0 sort# = \y0G1G2.y0 Using this interpretation, the requirements translate to: [[sort#(cons(_x0, _x1), _F2, _F3)]] = 1 + x1 > x1 = [[sort#(_x1, _F2, _F3)]] [[max(0, _x0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 3 >= 0 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 >= 0 = [[0]] [[min(_x0, 0)]] = 3 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 3 >= 0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 2 >= 1 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 3 + x2 >= 3 + x2 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 1 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 4 + 3x1 >= 3 + 3x1 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 4 + 3x0 >= 1 + 3x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 4 + 3x0 >= 1 + 3x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_4, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, static, formative), (P_2, R_0, static, formative) and (P_3, R_0, static, formative) is finite. We consider the dependency pair problem (P_3, 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: insert#(X, cons(Y, Z), F, G) >? insert#(G X Y, Z, F, G) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 0 ascending!6220sort = \y0.0 cons = \y0y1.1 + 2y1 descending!6220sort = \y0.0 insert = \y0y1G2G3.1 + 2y1 insert# = \y0y1G2G3.2y1 max = \y0y1.3 + 3y0 + 3y1 min = \y0y1.3 nil = 0 s = \y0.0 sort = \y0G1G2.2y0 Using this interpretation, the requirements translate to: [[insert#(_x0, cons(_x1, _x2), _F3, _F4)]] = 2 + 4x2 > 2x2 = [[insert#(_F4 _x0 _x1, _x2, _F3, _F4)]] [[max(0, _x0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 3 >= 0 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 >= 0 = [[0]] [[min(_x0, 0)]] = 3 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 3 >= 0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 1 >= 1 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 3 + 4x2 >= 3 + 4x2 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 0 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 2 + 4x1 >= 1 + 4x1 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 3 + 2x0 >= 2x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 3 + 2x0 >= 2x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. Thus, the original system is terminating if each of (P_1, R_0, static, formative) and (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: min#(s(X), s(Y)) >? min#(X, Y) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 1 ascending!6220sort = \y0.0 cons = \y0y1.3y1 descending!6220sort = \y0.0 insert = \y0y1G2G3.y1y1G3(y1,y1) max = \y0y1.3 + 3y0 + 3y1 min = \y0y1.1 + y1 + 2y0 min# = \y0y1.y0 nil = 0 s = \y0.1 + y0 sort = \y0G1G2.0 Using this interpretation, the requirements translate to: [[min#(s(_x0), s(_x1))]] = 1 + x0 > x0 = [[min#(_x0, _x1)]] [[max(0, _x0)]] = 6 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 6 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 9 + 3x0 + 3x1 >= 4 + 3x0 + 3x1 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 + x0 >= 1 = [[0]] [[min(_x0, 0)]] = 2 + 2x0 >= 1 = [[0]] [[min(s(_x0), s(_x1))]] = 4 + x1 + 2x0 >= 2 + x1 + 2x0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 0 >= 0 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 9x2x2F4(3x2,3x2) >= 3x2x2F4(x2,x2) = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 0 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 0 >= 0 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 3 >= 0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 3 >= 0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] 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. 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: max#(s(X), s(Y)) >? max#(X, Y) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 1 ascending!6220sort = \y0.0 cons = \y0y1.0 descending!6220sort = \y0.0 insert = \y0y1G2G3.0 max = \y0y1.3y0 + 3y1 max# = \y0y1.y1 min = \y0y1.2y1 + 3y0 nil = 0 s = \y0.3 + y0 sort = \y0G1G2.0 Using this interpretation, the requirements translate to: [[max#(s(_x0), s(_x1))]] = 3 + x1 > x1 = [[max#(_x0, _x1)]] [[max(0, _x0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 18 + 3x0 + 3x1 >= 3 + 3x0 + 3x1 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 + 2x0 >= 1 = [[0]] [[min(_x0, 0)]] = 2 + 3x0 >= 1 = [[0]] [[min(s(_x0), s(_x1))]] = 15 + 2x1 + 3x0 >= 3 + 2x1 + 3x0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 0 >= 0 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 0 >= 0 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 0 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 0 >= 0 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 3 >= 0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 3 >= 0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_1, 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.