We consider the system h47. Alphabet: 0 : [] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat xap : [nat -> nat -> nat * nat] --> nat -> nat xplus : [nat * nat] --> nat xtimes : [nat * nat] --> nat yap : [nat -> nat * nat] --> nat Rules: xplus(x, 0) => x xplus(x, s(y)) => s(xplus(x, y)) rec(0, x, /\y./\z.yap(xap(f, y), z)) => x rec(s(x), y, /\z./\u.yap(xap(f, z), u)) => yap(xap(f, x), rec(x, y, /\v./\w.yap(xap(f, v), w))) xtimes(x, y) => rec(y, 0, /\z./\u.xplus(x, u)) xap(f, x) => f x yap(f, x) => f x This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). Symbol xap is an encoding for application that is only used in innocuous ways. We can simplify the program (without losing non-termination) by removing it. This gives: Alphabet: 0 : [] --> nat rec : [nat * nat * nat -> nat -> nat] --> nat s : [nat] --> nat xplus : [nat * nat] --> nat xtimes : [nat * nat] --> nat yap : [nat -> nat * nat] --> nat Rules: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, Y)) rec(0, X, /\x./\y.yap(F(x), y)) => X rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) yap(F, X) => F X We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): xplus(X, 0) >? X xplus(X, s(Y)) >? s(xplus(X, Y)) rec(0, X, /\x./\y.yap(F(x), y)) >? X rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) xtimes(X, Y) >? rec(Y, 0, /\x./\y.xplus(X, y)) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, rec, s, xplus, xtimes, yap}, and the following precedence: xtimes > xplus > s > rec > yap > @_{o -> o} Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: xplus(X, _|_) >= X xplus(X, s(Y)) >= s(xplus(X, Y)) rec(_|_, X, /\x./\y.yap(F(x), y)) >= X rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) xtimes(X, Y) > rec(Y, _|_, /\x./\y.xplus(X, y)) yap(F, X) > @_{o -> o}(F, X) With these choices, we have: 1] xplus(X, _|_) >= X because [2], by (Star) 2] xplus*(X, _|_) >= X because [3], by (Select) 3] X >= X by (Meta) 4] xplus(X, s(Y)) >= s(xplus(X, Y)) because [5], by (Star) 5] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [6], by (Copy) 6] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [7] and [8], by (Stat) 7] X >= X by (Meta) 8] s(Y) > Y because [9], by definition 9] s*(Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] rec(_|_, X, /\x./\y.yap(F(x), y)) >= X because [12], by (Star) 12] rec*(_|_, X, /\x./\y.yap(F(x), y)) >= X because [13], by (Select) 13] X >= X by (Meta) 14] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [15], by (Star) 15] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [16], by (Select) 16] yap(F(rec*(s(X), Y, /\x./\y.yap(F(x), y))), rec*(s(X), Y, /\z./\u.yap(F(z), u))) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because yap in Mul, [17] and [22], by (Fun) 17] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [18], by (Meta) 18] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [19], by (Select) 19] s(X) >= X because [20], by (Star) 20] s*(X) >= X because [21], by (Select) 21] X >= X by (Meta) 22] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [23], [25] and [26], by (Stat) 23] s(X) > X because [24], by definition 24] s*(X) >= X because [21], by (Select) 25] Y >= Y by (Meta) 26] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [27], by (Abs) 27] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [28], by (Abs) 28] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [29] and [31], by (Fun) 29] F(y) >= F(y) because [30], by (Meta) 30] y >= y by (Var) 31] x >= x by (Var) 32] xtimes(X, Y) > rec(Y, _|_, /\x./\y.xplus(X, y)) because [33], by definition 33] xtimes*(X, Y) >= rec(Y, _|_, /\x./\y.xplus(X, y)) because xtimes > rec, [34], [36] and [37], by (Copy) 34] xtimes*(X, Y) >= Y because [35], by (Select) 35] Y >= Y by (Meta) 36] xtimes*(X, Y) >= _|_ by (Bot) 37] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [38], by (F-Abs) 38] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [39], by (F-Abs) 39] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [40] and [42], by (Copy) 40] xtimes*(X, Y, x, y) >= X because [41], by (Select) 41] X >= X by (Meta) 42] xtimes*(X, Y, x, y) >= y because [43], by (Select) 43] y >= y by (Var) 44] yap(F, X) > @_{o -> o}(F, X) because [45], by definition 45] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [46] and [48], by (Copy) 46] yap*(F, X) >= F because [47], by (Select) 47] F >= F by (Meta) 48] yap*(F, X) >= X because [49], by (Select) 49] X >= X by (Meta) We can thus remove the following rules: xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) yap(F, X) => F X We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): xplus(X, 0) >? X xplus(X, s(Y)) >? s(xplus(X, Y)) rec(0, X, /\x./\y.yap(F(x), y)) >? X rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 3 rec = \y0y1G2.2 + y1 + 2y0 + G2(y1,y1) + 2y0y1G2(y1,y0) + 3y0y0G2(y0,y0) s = \y0.3 + y0 xplus = \y0y1.y0 + 3y1 yap = \G0y1.y1 + G0(0) Using this interpretation, the requirements translate to: [[xplus(_x0, 0)]] = 9 + x0 > x0 = [[_x0]] [[xplus(_x0, s(_x1))]] = 9 + x0 + 3x1 > 3 + x0 + 3x1 = [[s(xplus(_x0, _x1))]] [[rec(0, _x0, /\x./\y.yap(_F1(x), y))]] = 89 + 20x0 + F1(x0,0) + 6x0F1(x0,0) + 27F1(3,0) > x0 = [[_x0]] [[rec(s(_x0), _x1, /\x./\y.yap(_F2(x), y))]] = 89 + 2x0x0x1 + 3x0x0x0 + 12x0x1 + 20x1 + 27x0x0 + 83x0 + F2(x1,0) + 2x0x1F2(x1,0) + 3x0x0F2(3 + x0,0) + 6x1F2(x1,0) + 18x0F2(3 + x0,0) + 27F2(3 + x0,0) > 2 + 2x0 + 2x0x0x1 + 2x1 + 3x0x0x0 + F2(x0,0) + F2(x1,0) + 2x0x1F2(x1,0) + 3x0x0F2(x0,0) = [[yap(_F2(_x0), rec(_x0, _x1, /\x./\y.yap(_F2(x), y)))]] We can thus remove the following rules: xplus(X, 0) => X xplus(X, s(Y)) => s(xplus(X, Y)) rec(0, X, /\x./\y.yap(F(x), y)) => X rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) All rules were succesfully removed. Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.