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]. We choose Lex = {rec} and Mul = {0, @_{o -> o}, s, xplus, xtimes, yap}, and the following precedence: xtimes > 0 > rec > yap > xplus > s > @_{o -> o} With these choices, we have: 1] xplus(X, 0) > X because [2], by definition 2] xplus*(X, 0) >= 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(0, X, /\x./\y.yap(F(x), y)) >= X because [12], by (Star) 12] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [13], by (Select) 13] yap(F(rec*(0, X, /\x./\y.yap(F(x), y))), rec*(0, X, /\z./\u.yap(F(z), u))) >= X because [14], by (Star) 14] yap*(F(rec*(0, X, /\x./\y.yap(F(x), y))), rec*(0, X, /\z./\u.yap(F(z), u))) >= X because [15], by (Select) 15] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [16], by (Select) 16] yap(F(rec*(0, X, /\x./\y.yap(F(x), y))), rec*(0, X, /\z./\u.yap(F(z), u))) >= X because [17], by (Star) 17] yap*(F(rec*(0, X, /\x./\y.yap(F(x), y))), rec*(0, X, /\z./\u.yap(F(z), u))) >= X because [18], by (Select) 18] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [19], by (Select) 19] X >= X by (Meta) 20] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [21], by (Star) 21] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [22], by (Select) 22] 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, [23] and [28], by (Fun) 23] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [24], by (Meta) 24] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [25], by (Select) 25] s(X) >= X because [26], by (Star) 26] s*(X) >= X because [27], by (Select) 27] X >= X by (Meta) 28] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because [29], [24], [31] and [33], by (Stat) 29] s(X) > X because [30], by definition 30] s*(X) >= X because [27], by (Select) 31] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= Y because [32], by (Select) 32] Y >= Y by (Meta) 33] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= /\x./\y.yap(F(x), y) because [34], by (F-Abs) 34] rec*(s(X), Y, /\x./\y.yap(F(x), y), z) >= /\x.yap(F(z), x) because [35], by (F-Abs) 35] rec*(s(X), Y, /\x./\y.yap(F(x), y), z, u) >= yap(F(z), u) because rec > yap, [36] and [41], by (Copy) 36] rec*(s(X), Y, /\x./\y.yap(F(x), y), z, u) >= F(z) because [37], by (Select) 37] /\x.yap(F(rec*(s(X), Y, /\y./\v.yap(F(y), v), z, u)), x) >= F(z) because [38], by (Eta)[Kop13:2] 38] F(rec*(s(X), Y, /\x./\y.yap(F(x), y), z, u)) >= F(z) because [39], by (Meta) 39] rec*(s(X), Y, /\x./\y.yap(F(x), y), z, u) >= z because [40], by (Select) 40] z >= z by (Var) 41] rec*(s(X), Y, /\x./\y.yap(F(x), y), z, u) >= u because [42], by (Select) 42] u >= u by (Var) 43] xtimes(X, Y) > rec(Y, 0, /\x./\y.xplus(X, y)) because [44], by definition 44] xtimes*(X, Y) >= rec(Y, 0, /\x./\y.xplus(X, y)) because xtimes > rec, [45], [47] and [48], by (Copy) 45] xtimes*(X, Y) >= Y because [46], by (Select) 46] Y >= Y by (Meta) 47] xtimes*(X, Y) >= 0 because xtimes > 0, by (Copy) 48] xtimes*(X, Y) >= /\y./\z.xplus(X, z) because [49], by (F-Abs) 49] xtimes*(X, Y, x) >= /\z.xplus(X, z) because [50], by (F-Abs) 50] xtimes*(X, Y, x, y) >= xplus(X, y) because xtimes > xplus, [51] and [53], by (Copy) 51] xtimes*(X, Y, x, y) >= X because [52], by (Select) 52] X >= X by (Meta) 53] xtimes*(X, Y, x, y) >= y because [54], by (Select) 54] y >= y by (Var) 55] yap(F, X) >= @_{o -> o}(F, X) because [56], by (Star) 56] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [57] and [59], by (Copy) 57] yap*(F, X) >= F because [58], by (Select) 58] F >= F by (Meta) 59] yap*(F, X) >= X because [60], by (Select) 60] X >= X by (Meta) We can thus remove the following rules: xplus(X, 0) => X xtimes(X, Y) => rec(Y, 0, /\x./\y.xplus(X, y)) 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, 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))) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {0, @_{o -> o}, rec, s, xplus, yap}, and the following precedence: rec > @_{o -> o} = yap > 0 > xplus > s With these choices, we have: 1] xplus(X, s(Y)) >= s(xplus(X, Y)) because [2], by (Star) 2] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [3], by (Copy) 3] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [4] and [5], by (Stat) 4] X >= X by (Meta) 5] s(Y) > Y because [6], by definition 6] s*(Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) 8] rec(0, X, /\x./\y.yap(F(x), y)) > X because [9], by definition 9] rec*(0, X, /\x./\y.yap(F(x), y)) >= X because [10], by (Select) 10] X >= X by (Meta) 11] rec(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [12], by (Star) 12] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec > yap, [13] and [20], by (Copy) 13] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [14], by (Select) 14] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [15], by (Eta)[Kop13:2] 15] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [16], by (Meta) 16] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [17], by (Select) 17] s(X) >= X because [18], by (Star) 18] s*(X) >= X because [19], by (Select) 19] X >= X by (Meta) 20] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [21], [23] and [24], by (Stat) 21] s(X) > X because [22], by definition 22] s*(X) >= X because [19], by (Select) 23] Y >= Y by (Meta) 24] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [25], by (Abs) 25] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [26], by (Abs) 26] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [27] and [29], by (Fun) 27] F(y) >= F(y) because [28], by (Meta) 28] y >= y by (Var) 29] x >= x by (Var) 30] yap(F, X) >= @_{o -> o}(F, X) because yap = @_{o -> o}, yap in Mul, [31] and [32], by (Fun) 31] F >= F by (Meta) 32] X >= X by (Meta) We can thus remove the following rules: rec(0, X, /\x./\y.yap(F(x), y)) => 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, s(Y)) >? s(xplus(X, Y)) rec(s(X), Y, /\x./\y.yap(F(x), y)) >? yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) yap(F, X) >? F X We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {@_{o -> o}, rec, s, xplus, yap}, and the following precedence: xplus > rec > yap > @_{o -> o} > s With these choices, we have: 1] xplus(X, s(Y)) >= s(xplus(X, Y)) because [2], by (Star) 2] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [3], by (Copy) 3] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [4] and [5], by (Stat) 4] X >= X by (Meta) 5] s(Y) > Y because [6], by definition 6] s*(Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) 8] rec(s(X), Y, /\x./\y.yap(F(x), y)) > yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because [9], by definition 9] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= yap(F(X), rec(X, Y, /\x./\y.yap(F(x), y))) because rec > yap, [10] and [17], by (Copy) 10] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= F(X) because [11], by (Select) 11] /\x.yap(F(rec*(s(X), Y, /\y./\z.yap(F(y), z))), x) >= F(X) because [12], by (Eta)[Kop13:2] 12] F(rec*(s(X), Y, /\x./\y.yap(F(x), y))) >= F(X) because [13], by (Meta) 13] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= X because [14], by (Select) 14] s(X) >= X because [15], by (Star) 15] s*(X) >= X because [16], by (Select) 16] X >= X by (Meta) 17] rec*(s(X), Y, /\x./\y.yap(F(x), y)) >= rec(X, Y, /\x./\y.yap(F(x), y)) because rec in Mul, [18], [20] and [21], by (Stat) 18] s(X) > X because [19], by definition 19] s*(X) >= X because [16], by (Select) 20] Y >= Y by (Meta) 21] /\x./\z.yap(F(x), z) >= /\x./\z.yap(F(x), z) because [22], by (Abs) 22] /\z.yap(F(y), z) >= /\z.yap(F(y), z) because [23], by (Abs) 23] yap(F(y), x) >= yap(F(y), x) because yap in Mul, [24] and [26], by (Fun) 24] F(y) >= F(y) because [25], by (Meta) 25] y >= y by (Var) 26] x >= x by (Var) 27] yap(F, X) > @_{o -> o}(F, X) because [28], by definition 28] yap*(F, X) >= @_{o -> o}(F, X) because yap > @_{o -> o}, [29] and [31], by (Copy) 29] yap*(F, X) >= F because [30], by (Select) 30] F >= F by (Meta) 31] yap*(F, X) >= X because [32], by (Select) 32] X >= X by (Meta) We can thus remove the following rules: rec(s(X), Y, /\x./\y.yap(F(x), y)) => yap(F(X), rec(X, Y, /\z./\u.yap(F(z), u))) 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, s(Y)) >? s(xplus(X, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {s, xplus}, and the following precedence: xplus > s With these choices, we have: 1] xplus(X, s(Y)) > s(xplus(X, Y)) because [2], by definition 2] xplus*(X, s(Y)) >= s(xplus(X, Y)) because xplus > s and [3], by (Copy) 3] xplus*(X, s(Y)) >= xplus(X, Y) because xplus in Mul, [4] and [5], by (Stat) 4] X >= X by (Meta) 5] s(Y) > Y because [6], by definition 6] s*(Y) >= Y because [7], by (Select) 7] Y >= Y by (Meta) We can thus remove the following rules: xplus(X, s(Y)) => s(xplus(X, Y)) 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. [Kop13:2] C. Kop. StarHorpo with an Eta-Rule. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/etahorpo.pdf, 2013.