We consider the system h52. Alphabet: 0 : [] --> nat cons : [] --> nat -> list -> list foldl : [] --> (nat -> nat -> nat) -> nat -> list -> nat nil : [] --> list plusc : [] --> nat -> nat -> nat s : [] --> nat -> nat sum : [] --> list -> nat Rules: foldl (/\x./\y.f x y) z nil => z foldl (/\x./\y.f x y) z (cons u v) => foldl (/\w./\x'.f w x') (f z u) v plusc x 0 => x plusc x (s y) => s (plusc x y) sum x => foldl (/\y./\z.plusc y z) 0 x 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 foldl : [nat -> nat -> nat * nat * list] --> nat nil : [] --> list plusc : [nat * nat] --> nat s : [nat] --> nat sum : [list] --> nat ~AP1 : [nat -> nat -> nat * nat] --> nat -> nat Rules: foldl(/\x./\y.~AP1(F, x) y, X, nil) => X foldl(/\x./\y.~AP1(F, x) y, X, cons(Y, Z)) => foldl(/\z./\u.~AP1(F, z) u, ~AP1(F, X) Y, Z) plusc(X, 0) => X plusc(X, s(Y)) => s(plusc(X, Y)) sum(X) => foldl(/\x./\y.plusc(x, y), 0, X) foldl(/\x./\y.plusc(x, y), X, nil) => X foldl(/\x./\y.plusc(x, y), X, cons(Y, Z)) => foldl(/\z./\u.plusc(z, u), plusc(X, Y), Z) ~AP1(F, X) => F X Symbol ~AP1 is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. Additionally, we can remove some (now-)redundant rules. This gives: Alphabet: 0 : [] --> nat cons : [nat * list] --> list foldl : [nat -> nat -> nat * nat * list] --> nat nil : [] --> list plusc : [nat * nat] --> nat s : [nat] --> nat sum : [list] --> nat Rules: foldl(/\x./\y.X(x, y), Y, nil) => Y foldl(/\x./\y.X(x, y), Y, cons(Z, U)) => foldl(/\z./\u.X(z, u), X(Y, Z), U) plusc(X, 0) => X plusc(X, s(Y)) => s(plusc(X, Y)) sum(X) => foldl(/\x./\y.plusc(x, y), 0, X) We observe that the rules contain a first-order subset: plusc(X, 0) => X plusc(X, s(Y)) => s(plusc(X, Y)) Moreover, the system is orthogonal. 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 terminating when seen as a many-sorted first-order TRS. According to the external first-order termination prover, this system is indeed 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: || || plusc(%X, 0) -> %X || plusc(%X, s(%Y)) -> s(plusc(%X, %Y)) || || Q is empty. || || ---------------------------------------- || || (1) QTRSRRRProof (EQUIVALENT) || Used ordering: || Polynomial interpretation [POLO]: || || POL(0) = 2 || POL(plusc(x_1, x_2)) = 2 + 2*x_1 + 2*x_2 || POL(s(x_1)) = 1 + x_1 || With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly: || || plusc(%X, 0) -> %X || plusc(%X, s(%Y)) -> s(plusc(%X, %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 dynamic dependency pairs. We thus obtain the following dependency pair problem (P_0, R_0, minimal, formative): Dependency Pairs P_0: 0] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> foldl#(/\z./\u.X(z, u), X(Y, Z), U) 1] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> X(z, u) 2] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> X(Y, Z) 3] sum#(X) =#> foldl#(/\x./\y.plusc(x, y), 0, X) 4] sum#(X) =#> plusc#(x, y) Rules R_0: foldl(/\x./\y.X(x, y), Y, nil) => Y foldl(/\x./\y.X(x, y), Y, cons(Z, U)) => foldl(/\z./\u.X(z, u), X(Y, Z), U) plusc(X, 0) => X plusc(X, s(Y)) => s(plusc(X, Y)) sum(X) => foldl(/\x./\y.plusc(x, y), 0, X) Thus, the original system is terminating if (P_0, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_0, R_0, minimal, 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, 2 * 1 : 0, 1, 2, 3, 4 * 2 : 0, 1, 2, 3, 4 * 3 : 0, 1, 2 * 4 : This graph has the following strongly connected components: P_1: foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> foldl#(/\z./\u.X(z, u), X(Y, Z), U) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> X(z, u) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> X(Y, Z) sum#(X) =#> foldl#(/\x./\y.plusc(x, y), 0, X) 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). Thus, the original system is terminating if (P_1, R_0, minimal, formative) is finite. We consider the dependency pair problem (P_1, R_0, minimal, formative). This combination (P_1, R_0) has no formative rules! We will name the empty set of rules:R_1. By [Kop12, Thm. 7.17], we may replace the dependency pair problem (P_1, R_0, minimal, formative) by (P_1, R_1, minimal, formative). Thus, the original system is terminating if (P_1, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_1, R_1, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >? foldl#(/\z./\u.X(z, u), X(Y, Z), U) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >? X(~c0, ~c1) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >? X(Y, Z) sum#(X) >? foldl#(/\x./\y.plusc-(x, y), 0, X) plusc-(X, Y) >= plusc(X, Y) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( sum#(X) ) = #argfun-sum##(foldl#(/\x./\y.plusc-(x, y), 0, X)) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[foldl#(x_1, x_2, x_3)]] = foldl#(x_3, x_1, x_2) [[sum#(x_1)]] = x_1 [[~c0]] = _|_ [[~c1]] = _|_ We choose Lex = {foldl#} and Mul = {#argfun-sum##, cons, plusc, plusc-}, and the following precedence: cons > plusc = plusc- > foldl# > #argfun-sum## Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) > foldl#(/\x./\y.X(x, y), X(Y, Z), U) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >= X(_|_, _|_) foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) > X(Y, Z) #argfun-sum##(foldl#(/\x./\y.plusc-(x, y), _|_, X)) >= foldl#(/\x./\y.plusc-(x, y), _|_, X) plusc-(X, Y) >= plusc(X, Y) With these choices, we have: 1] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) > foldl#(/\x./\y.X(x, y), X(Y, Z), U) because [2], by definition 2] foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)) >= foldl#(/\x./\y.X(x, y), X(Y, Z), U) because [3], [6], [12] and [20], by (Stat) 3] cons(Z, U) > U because [4], by definition 4] cons*(Z, U) >= U because [5], by (Select) 5] U >= U by (Meta) 6] foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)) >= /\x./\y.X(x, y) because [7], by (Select) 7] /\x./\z.X(x, z) >= /\x./\z.X(x, z) because [8], by (Abs) 8] /\z.X(y, z) >= /\z.X(y, z) because [9], by (Abs) 9] X(y, x) >= X(y, x) because [10] and [11], by (Meta) 10] y >= y by (Var) 11] x >= x by (Var) 12] foldl#*(/\z./\u.X(z, u), Y, cons(Z, U)) >= X(Y, Z) because [13], by (Select) 13] X(foldl#*(/\z./\u.X(z, u), Y, cons(Z, U)), foldl#*(/\v./\w.X(v, w), Y, cons(Z, U))) >= X(Y, Z) because [14] and [16], by (Meta) 14] foldl#*(/\z./\u.X(z, u), Y, cons(Z, U)) >= Y because [15], by (Select) 15] Y >= Y by (Meta) 16] foldl#*(/\z./\u.X(z, u), Y, cons(Z, U)) >= Z because [17], by (Select) 17] cons(Z, U) >= Z because [18], by (Star) 18] cons*(Z, U) >= Z because [19], by (Select) 19] Z >= Z by (Meta) 20] foldl#*(/\z./\u.X(z, u), Y, cons(Z, U)) >= U because [21], by (Select) 21] cons(Z, U) >= U because [4], by (Star) 22] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >= X(_|_, _|_) because [23], by (Star) 23] foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)) >= X(_|_, _|_) because [24], by (Select) 24] X(foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)), foldl#*(/\z./\u.X(z, u), Y, cons(Z, U))) >= X(_|_, _|_) because [25] and [26], by (Meta) 25] foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)) >= _|_ by (Bot) 26] foldl#*(/\x./\y.X(x, y), Y, cons(Z, U)) >= _|_ by (Bot) 27] foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) > X(Y, Z) because [12], by definition 28] #argfun-sum##(foldl#(/\x./\y.plusc-(x, y), _|_, X)) >= foldl#(/\x./\y.plusc-(x, y), _|_, X) because [29], by (Star) 29] #argfun-sum##*(foldl#(/\x./\y.plusc-(x, y), _|_, X)) >= foldl#(/\x./\y.plusc-(x, y), _|_, X) because [30], by (Select) 30] foldl#(/\x./\y.plusc-(x, y), _|_, X) >= foldl#(/\x./\y.plusc-(x, y), _|_, X) because [31], [36] and [37], by (Fun) 31] /\x./\z.plusc-(x, z) >= /\x./\z.plusc-(x, z) because [32], by (Abs) 32] /\z.plusc-(y, z) >= /\z.plusc-(y, z) because [33], by (Abs) 33] plusc-(y, x) >= plusc-(y, x) because plusc- in Mul, [34] and [35], by (Fun) 34] y >= y by (Var) 35] x >= x by (Var) 36] _|_ >= _|_ by (Bot) 37] X >= X by (Meta) 38] plusc-(X, Y) >= plusc(X, Y) because plusc- = plusc, plusc- in Mul, [39] and [40], by (Fun) 39] X >= X by (Meta) 40] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_1, minimal, formative) by (P_2, R_1, minimal, formative), where P_2 consists of: foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) =#> X(z, u) sum#(X) =#> foldl#(/\x./\y.plusc(x, y), 0, X) Thus, the original system is terminating if (P_2, R_1, minimal, formative) is finite. We consider the dependency pair problem (P_2, R_1, minimal, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. As the system is abstraction-simple and the formative flag is set, it suffices to find a tagged reduction pair [Kop12, Def. 6.70]. Thus, we must orient: foldl#(/\x./\y.X(x, y), Y, cons(Z, U)) >? X(~c0, ~c1) sum#(X) >? foldl#(/\x./\y.plusc-(x, y), 0, X) plusc-(X, Y) >= plusc(X, Y) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( sum#(X) ) = #argfun-sum##(foldl#(/\x./\y.plusc-(x, y), 0, X)) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-sum## = \y0.3 + y0 0 = 0 cons = \y0y1.3 foldl# = \G0y1y2.3 + y2y2G0(y2,y2) plusc = \y0y1.0 plusc- = \y0y1.3 + 3y0 + 3y1 sum# = \y0.0 ~c0 = 0 ~c1 = 0 Using this interpretation, the requirements translate to: [[foldl#(/\x./\y._x0(x, y), _x1, cons(_x2, _x3))]] = 3 + 9F0(3,3) > F0(0,0) = [[_x0(~c0, ~c1)]] [[#argfun-sum##(foldl#(/\x./\y.plusc-(x, y), 0, _x0))]] = 6 + 3x0x0 + 6x0x0x0 > 3 + 3x0x0 + 6x0x0x0 = [[foldl#(/\x./\y.plusc-(x, y), 0, _x0)]] [[plusc-(_x0, _x1)]] = 3 + 3x0 + 3x1 >= 0 = [[plusc(_x0, _x1)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_2, R_1) by ({}, R_1). 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 +++ [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.