We consider the system onearg. Alphabet: 0 : [] --> nat add : [nat] --> nat -> nat eq : [nat] --> nat -> bool err : [] --> nat false : [] --> bool id : [] --> nat -> nat nul : [] --> nat -> bool pred : [nat] --> nat s : [nat] --> nat true : [] --> bool Rules: nul 0 => true nul s(x) => false nul err => false pred(0) => err pred(s(x)) => x id x => x eq(0) => nul eq(s(x)) => /\y.eq(x) pred(y) add(0) => id add(s(x)) => /\y.add(x) s(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]). In order to do so, we start by eta-expanding the system, which gives: nul(0) => true nul(s(X)) => false nul(err) => false pred(0) => err pred(s(X)) => X id(X) => X eq(0, X) => nul(X) eq(s(X), Y) => (/\x.eq(X, pred(x))) Y add(0, X) => id(X) add(s(X), Y) => (/\x.add(X, s(x))) Y We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] eq#(0, X) =#> nul#(X) 1] eq#(s(X), Y) =#> eq#(X, pred(Y)) 2] eq#(s(X), Y) =#> pred#(Y) 3] add#(0, X) =#> id#(X) 4] add#(s(X), Y) =#> add#(X, s(Y)) Rules R_0: nul(0) => true nul(s(X)) => false nul(err) => false pred(0) => err pred(s(X)) => X id(X) => X eq(0, X) => nul(X) eq(s(X), Y) => (/\x.eq(X, pred(x))) Y add(0, X) => id(X) add(s(X), Y) => (/\x.add(X, s(x))) 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 place the elements of P in a dependency graph approximation G (see e.g. [Kop12, Thm. 7.27, 7.29], as follows: * 0 : * 1 : 0, 1, 2 * 2 : * 3 : * 4 : 3, 4 This graph has the following strongly connected components: P_1: eq#(s(X), Y) =#> eq#(X, pred(Y)) P_2: add#(s(X), Y) =#> add#(X, s(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, 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: add#(s(X), Y) >? add#(X, s(Y)) nul(0) >= true nul(s(X)) >= false nul(err) >= false pred(0) >= err pred(s(X)) >= X id(X) >= X eq(0, X) >= nul(X) eq(s(X), Y) >= (/\x.eq(X, pred(x))) Y add(0, X) >= id(X) add(s(X), Y) >= (/\x.add(X, s(x))) Y We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( id(X) ) = #argfun-id#(X) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-id# = \y0.y0 0 = 3 add = \y0y1.3 + 2y1 + 3y0 add# = \y0y1.y0 eq = \y0y1.3 err = 0 false = 0 id = \y0.0 nul = \y0.0 pred = \y0.y0 s = \y0.3 + y0 true = 0 Using this interpretation, the requirements translate to: [[add#(s(_x0), _x1)]] = 3 + x0 > x0 = [[add#(_x0, s(_x1))]] [[nul(0)]] = 0 >= 0 = [[true]] [[nul(s(_x0))]] = 0 >= 0 = [[false]] [[nul(err)]] = 0 >= 0 = [[false]] [[pred(0)]] = 3 >= 0 = [[err]] [[pred(s(_x0))]] = 3 + x0 >= x0 = [[_x0]] [[#argfun-id#(_x0)]] = x0 >= x0 = [[_x0]] [[eq(0, _x0)]] = 3 >= 0 = [[nul(_x0)]] [[eq(s(_x0), _x1)]] = 3 >= 3 = [[(/\x.eq(_x0, pred(x))) _x1]] [[add(0, _x0)]] = 12 + 2x0 >= x0 = [[#argfun-id#(_x0)]] [[add(s(_x0), _x1)]] = 12 + 2x1 + 3x0 >= 9 + 2x1 + 3x0 = [[(/\x.add(_x0, s(x))) _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. 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: eq#(s(X), Y) >? eq#(X, pred(Y)) nul(0) >= true nul(s(X)) >= false nul(err) >= false pred(0) >= err pred(s(X)) >= X id(X) >= X eq(0, X) >= nul(X) eq(s(X), Y) >= (/\x.eq(X, pred(x))) Y add(0, X) >= id(X) add(s(X), Y) >= (/\x.add(X, s(x))) Y We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( id(X) ) = #argfun-id#(X) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-id# = \y0.y0 0 = 3 add = \y0y1.3 + 2y1 + 3y0 eq = \y0y1.3 eq# = \y0y1.y0 err = 0 false = 0 id = \y0.0 nul = \y0.0 pred = \y0.y0 s = \y0.3 + y0 true = 0 Using this interpretation, the requirements translate to: [[eq#(s(_x0), _x1)]] = 3 + x0 > x0 = [[eq#(_x0, pred(_x1))]] [[nul(0)]] = 0 >= 0 = [[true]] [[nul(s(_x0))]] = 0 >= 0 = [[false]] [[nul(err)]] = 0 >= 0 = [[false]] [[pred(0)]] = 3 >= 0 = [[err]] [[pred(s(_x0))]] = 3 + x0 >= x0 = [[_x0]] [[#argfun-id#(_x0)]] = x0 >= x0 = [[_x0]] [[eq(0, _x0)]] = 3 >= 0 = [[nul(_x0)]] [[eq(s(_x0), _x1)]] = 3 >= 3 = [[(/\x.eq(_x0, pred(x))) _x1]] [[add(0, _x0)]] = 12 + 2x0 >= x0 = [[#argfun-id#(_x0)]] [[add(s(_x0), _x1)]] = 12 + 2x1 + 3x0 >= 9 + 2x1 + 3x0 = [[(/\x.add(_x0, s(x))) _x1]] 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.