We consider the system Applicative_05__Ex5Sorting. Alphabet: 0 : [] --> a ascending!fac6220sort : [b] --> b cons : [a * b] --> b descending!fac6220sort : [b] --> b insert : [a -> a -> a * a -> a -> a * b * a] --> b max : [] --> a -> a -> a min : [] --> a -> a -> a nil : [] --> b s : [a] --> a sort : [a -> a -> a * a -> a -> a * b] --> b Rules: max 0 x => x max x 0 => x max s(x) s(y) => max x y min 0 x => 0 min x 0 => 0 min s(x) s(y) => min x y insert(f, g, nil, x) => cons(x, nil) insert(f, g, cons(x, y), z) => cons(f z x, insert(f, g, y, g z x)) sort(f, g, nil) => nil sort(f, g, cons(x, y)) => insert(f, g, sort(f, g, y), x) ascending!fac6220sort(x) => sort(min, max, x) descending!fac6220sort(x) => sort(max, min, x) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We observe that the rules contain a first-order subset: max(0, X) => X max(X, 0) => X max(s(X), s(Y)) => max(X, Y) min(0, X) => 0 min(X, 0) => 0 min(s(X), s(Y)) => min(X, Y) Moreover, the system is finitely branching. Thus, by [Kop12, Thm. 7.55], we may omit all first-order dependency pairs from the dependency pair problem (DP(R), R) if this first-order part is Ce-terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed Ce-terminating: || proof of resources/system.trs || # AProVE Commit ID: d84c10301d352dfd14de2104819581f4682260f5 fuhs 20130616 || || || Termination w.r.t. Q of the given QTRS could be proven: || || (0) QTRS || (1) QTRSRRRProof [EQUIVALENT] || (2) QTRS || (3) RisEmptyProof [EQUIVALENT] || (4) YES || || || ---------------------------------------- || || (0) || Obligation: || Q restricted rewrite system: || The TRS R consists of the following rules: || || max(0, %X) -> %X || max(%X, 0) -> %X || max(s(%X), s(%Y)) -> max(%X, %Y) || min(0, %X) -> 0 || min(%X, 0) -> 0 || min(s(%X), s(%Y)) -> min(%X, %Y) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Polynomial interpretation [POLO]: || || POL(0) = 0 || POL(max(x_1, x_2)) = 2 + 2*x_1 + x_2 || POL(min(x_1, x_2)) = 1 + x_1 + x_2 || POL(s(x_1)) = 1 + 2*x_1 || POL(~PAIR(x_1, x_2)) = 2 + x_1 + x_2 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || max(0, %X) -> %X || max(%X, 0) -> %X || max(s(%X), s(%Y)) -> max(%X, %Y) || min(0, %X) -> 0 || min(%X, 0) -> 0 || min(s(%X), s(%Y)) -> min(%X, %Y) || ~PAIR(%X, %Y) -> %X || ~PAIR(%X, %Y) -> %Y || || || || || ---------------------------------------- || || (2) || Obligation: || Q restricted rewrite system: || R is empty. || Q is empty. || || ---------------------------------------- || || (3) RisEmptyProof (EQUIVALENT) || The TRS R is empty. Hence, termination is trivially proven. || ---------------------------------------- || || (4) || YES || 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 [FuhKop19]). In order to do so, we start by eta-expanding the system, which gives: max(0, X) => X max(X, 0) => X max(s(X), s(Y)) => max(X, Y) min(0, X) => 0 min(X, 0) => 0 min(s(X), s(Y)) => min(X, Y) insert(F, G, nil, X) => cons(X, nil) insert(F, G, cons(X, Y), Z) => cons(F Z X, insert(F, G, Y, G Z X)) sort(F, G, nil) => nil sort(F, G, cons(X, Y)) => insert(F, G, sort(F, G, Y), X) ascending!fac6220sort(X) => sort(/\x./\y.min(x, y), /\z./\u.max(z, u), X) descending!fac6220sort(X) => sort(/\x./\y.max(x, y), /\z./\u.min(z, u), X) We thus obtain the following dependency pair problem (P_0, R_0, computable, formative): Dependency Pairs P_0: 0] insert#(F, G, cons(X, Y), Z) =#> insert#(F, G, Y, G Z X) 1] sort#(F, G, cons(X, Y)) =#> insert#(F, G, sort(F, G, Y), X) 2] sort#(F, G, cons(X, Y)) =#> sort#(F, G, Y) 3] ascending!fac6220sort#(X) =#> sort#(/\x./\y.min(x, y), /\z./\u.max(z, u), X) 4] ascending!fac6220sort#(X) =#> min#(Y, Z) 5] ascending!fac6220sort#(X) =#> max#(Y, Z) 6] descending!fac6220sort#(X) =#> sort#(/\x./\y.max(x, y), /\z./\u.min(z, u), X) 7] descending!fac6220sort#(X) =#> max#(Y, Z) 8] descending!fac6220sort#(X) =#> min#(Y, Z) Rules R_0: max(0, X) => X max(X, 0) => X max(s(X), s(Y)) => max(X, Y) min(0, X) => 0 min(X, 0) => 0 min(s(X), s(Y)) => min(X, Y) insert(F, G, nil, X) => cons(X, nil) insert(F, G, cons(X, Y), Z) => cons(F Z X, insert(F, G, Y, G Z X)) sort(F, G, nil) => nil sort(F, G, cons(X, Y)) => insert(F, G, sort(F, G, Y), X) ascending!fac6220sort(X) => sort(/\x./\y.min(x, y), /\z./\u.max(z, u), X) descending!fac6220sort(X) => sort(/\x./\y.max(x, y), /\z./\u.min(z, u), X) Thus, the original system is terminating if (P_0, R_0, computable, formative) is finite. We consider the dependency pair problem (P_0, R_0, computable, 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 : 0 * 2 : 1, 2 * 3 : 1, 2 * 4 : * 5 : * 6 : 1, 2 * 7 : * 8 : This graph has the following strongly connected components: P_1: insert#(F, G, cons(X, Y), Z) =#> insert#(F, G, Y, G Z X) P_2: sort#(F, G, cons(X, Y)) =#> sort#(F, G, Y) 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) and (P_2, R_0, m, f). Thus, the original system is terminating if each of (P_1, R_0, computable, formative) and (P_2, R_0, computable, formative) is finite. We consider the dependency pair problem (P_2, R_0, computable, formative). We apply the subterm criterion with the following projection function: nu(sort#) = 3 Thus, we can orient the dependency pairs as follows: nu(sort#(F, G, cons(X, Y))) = cons(X, Y) |> Y = nu(sort#(F, G, Y)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_2, R_0, computable, f) by ({}, R_0, computable, f). 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, computable, formative) is finite. We consider the dependency pair problem (P_1, R_0, computable, formative). We apply the subterm criterion with the following projection function: nu(insert#) = 3 Thus, we can orient the dependency pairs as follows: nu(insert#(F, G, cons(X, Y), Z)) = cons(X, Y) |> Y = nu(insert#(F, G, Y, G Z X)) By [FuhKop19, Thm. 61], we may replace a dependency pair problem (P_1, R_0, computable, f) by ({}, R_0, computable, f). 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 +++ [FuhKop19] C. Fuhs, and C. Kop. A static higher-order dependency pair framework. In Proceedings of ESOP 2019, 2019. [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [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.