We consider the system Applicative_05__TreeHeight. Alphabet: 0 : [] --> d cons : [d * c] --> c false : [] --> a height : [] --> d -> d if : [a * d] --> d le : [d * d] --> a map : [d -> d * c] --> c maxlist : [d * c] --> d nil : [] --> c node : [b * c] --> d s : [d] --> d true : [] --> a Rules: map(f, nil) => nil map(f, cons(x, y)) => cons(f x, map(f, y)) le(0, x) => true le(s(x), 0) => false le(s(x), s(y)) => le(x, y) maxlist(x, cons(y, z)) => if(le(x, y), maxlist(y, z)) maxlist(x, nil) => x height node(x, y) => s(maxlist(0, map(height, y))) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) le(0, X) >? true le(s(X), 0) >? false le(s(X), s(Y)) >? le(X, Y) maxlist(X, cons(Y, Z)) >? if(le(X, Y), maxlist(Y, Z)) maxlist(X, nil) >? X height node(X, Y) >? s(maxlist(0, map(height, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[height]] = _|_ [[nil]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, if, le, map, maxlist, node}, and the following precedence: @_{o -> o} = map > node > cons > maxlist > if > le Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, _|_) >= _|_ map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) le(_|_, X) >= _|_ le(X, _|_) >= _|_ le(X, Y) >= le(X, Y) maxlist(X, cons(Y, Z)) >= if(le(X, Y), maxlist(Y, Z)) maxlist(X, _|_) > X @_{o -> o}(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) With these choices, we have: 1] map(F, _|_) >= _|_ by (Bot) 2] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [3], by (Star) 3] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [4] and [9], by (Copy) 4] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map = @_{o -> o}, map in Mul, [5] and [6], by (Stat) 5] F >= F by (Meta) 6] cons(X, Y) > X because [7], by definition 7] cons*(X, Y) >= X because [8], by (Select) 8] X >= X by (Meta) 9] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [5] and [10], by (Stat) 10] cons(X, Y) > Y because [11], by definition 11] cons*(X, Y) >= Y because [12], by (Select) 12] Y >= Y by (Meta) 13] le(_|_, X) >= _|_ by (Bot) 14] le(X, _|_) >= _|_ by (Bot) 15] le(X, Y) >= le(X, Y) because le in Mul, [16] and [17], by (Fun) 16] X >= X by (Meta) 17] Y >= Y by (Meta) 18] maxlist(X, cons(Y, Z)) >= if(le(X, Y), maxlist(Y, Z)) because [19], by (Star) 19] maxlist*(X, cons(Y, Z)) >= if(le(X, Y), maxlist(Y, Z)) because maxlist > if, [20] and [27], by (Copy) 20] maxlist*(X, cons(Y, Z)) >= le(X, Y) because maxlist > le, [21] and [23], by (Copy) 21] maxlist*(X, cons(Y, Z)) >= X because [22], by (Select) 22] X >= X by (Meta) 23] maxlist*(X, cons(Y, Z)) >= Y because [24], by (Select) 24] cons(Y, Z) >= Y because [25], by (Star) 25] cons*(Y, Z) >= Y because [26], by (Select) 26] Y >= Y by (Meta) 27] maxlist*(X, cons(Y, Z)) >= maxlist(Y, Z) because [28], by (Select) 28] cons(Y, Z) >= maxlist(Y, Z) because [29], by (Star) 29] cons*(Y, Z) >= maxlist(Y, Z) because cons > maxlist, [30] and [31], by (Copy) 30] cons*(Y, Z) >= Y because [26], by (Select) 31] cons*(Y, Z) >= Z because [32], by (Select) 32] Z >= Z by (Meta) 33] maxlist(X, _|_) > X because [34], by definition 34] maxlist*(X, _|_) >= X because [35], by (Select) 35] X >= X by (Meta) 36] @_{o -> o}(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) because [37], by (Star) 37] @_{o -> o}*(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) because @_{o -> o} > maxlist, [38] and [39], by (Copy) 38] @_{o -> o}*(_|_, node(X, Y)) >= _|_ by (Bot) 39] @_{o -> o}*(_|_, node(X, Y)) >= map(_|_, Y) because @_{o -> o} = map, @_{o -> o} in Mul, [40] and [41], by (Stat) 40] _|_ >= _|_ by (Bot) 41] node(X, Y) > Y because [42], by definition 42] node*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) We can thus remove the following rules: maxlist(X, nil) => 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]): map(F, nil) >? nil map(F, cons(X, Y)) >? cons(F X, map(F, Y)) le(0, X) >? true le(s(X), 0) >? false le(s(X), s(Y)) >? le(X, Y) maxlist(X, cons(Y, Z)) >? if(le(X, Y), maxlist(Y, Z)) height node(X, Y) >? s(maxlist(0, map(height, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[height]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, if, le, map, maxlist, nil, node}, and the following precedence: nil > node > @_{o -> o} = map = maxlist > if > le > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, nil) > nil map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) le(_|_, X) >= _|_ le(X, _|_) >= _|_ le(X, Y) >= le(X, Y) maxlist(X, cons(Y, Z)) > if(le(X, Y), maxlist(Y, Z)) @_{o -> o}(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) With these choices, we have: 1] map(F, nil) > nil because [2], by definition 2] map*(F, nil) >= nil because [3], by (Select) 3] nil >= nil by (Fun) 4] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [5], by (Star) 5] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [6] and [11], by (Copy) 6] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map = @_{o -> o}, map in Mul, [7] and [8], by (Stat) 7] F >= F by (Meta) 8] cons(X, Y) > X because [9], by definition 9] cons*(X, Y) >= X because [10], by (Select) 10] X >= X by (Meta) 11] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [7] and [12], by (Stat) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] le(_|_, X) >= _|_ by (Bot) 16] le(X, _|_) >= _|_ by (Bot) 17] le(X, Y) >= le(X, Y) because le in Mul, [18] and [19], by (Fun) 18] X >= X by (Meta) 19] Y >= Y by (Meta) 20] maxlist(X, cons(Y, Z)) > if(le(X, Y), maxlist(Y, Z)) because [21], by definition 21] maxlist*(X, cons(Y, Z)) >= if(le(X, Y), maxlist(Y, Z)) because maxlist > if, [22] and [29], by (Copy) 22] maxlist*(X, cons(Y, Z)) >= le(X, Y) because maxlist > le, [23] and [25], by (Copy) 23] maxlist*(X, cons(Y, Z)) >= X because [24], by (Select) 24] X >= X by (Meta) 25] maxlist*(X, cons(Y, Z)) >= Y because [26], by (Select) 26] cons(Y, Z) >= Y because [27], by (Star) 27] cons*(Y, Z) >= Y because [28], by (Select) 28] Y >= Y by (Meta) 29] maxlist*(X, cons(Y, Z)) >= maxlist(Y, Z) because maxlist in Mul, [30] and [32], by (Stat) 30] cons(Y, Z) > Y because [31], by definition 31] cons*(Y, Z) >= Y because [28], by (Select) 32] cons(Y, Z) > Z because [33], by definition 33] cons*(Y, Z) >= Z because [34], by (Select) 34] Z >= Z by (Meta) 35] @_{o -> o}(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) because [36], by (Star) 36] @_{o -> o}*(_|_, node(X, Y)) >= maxlist(_|_, map(_|_, Y)) because @_{o -> o} = maxlist, @_{o -> o} in Mul, [37] and [39], by (Stat) 37] node(X, Y) > _|_ because [38], by definition 38] node*(X, Y) >= _|_ by (Bot) 39] node(X, Y) > map(_|_, Y) because [40], by definition 40] node*(X, Y) >= map(_|_, Y) because node > map, [41] and [42], by (Copy) 41] node*(X, Y) >= _|_ by (Bot) 42] node*(X, Y) >= Y because [43], by (Select) 43] Y >= Y by (Meta) We can thus remove the following rules: map(F, nil) => nil maxlist(X, cons(Y, Z)) => if(le(X, Y), maxlist(Y, Z)) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, cons(X, Y)) >? cons(F X, map(F, Y)) le(0, X) >? true le(s(X), 0) >? false le(s(X), s(Y)) >? le(X, Y) height node(X, Y) >? s(maxlist(0, map(height, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, height, le, map, maxlist, node}, and the following precedence: node > map > maxlist > height > @_{o -> o} > cons > le Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) le(_|_, X) > _|_ le(X, _|_) >= _|_ le(X, Y) >= le(X, Y) @_{o -> o}(height, node(X, Y)) >= maxlist(_|_, map(height, Y)) With these choices, we have: 1] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [2], by (Star) 2] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [3] and [10], by (Copy) 3] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [4] and [6], by (Copy) 4] map*(F, cons(X, Y)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] map*(F, cons(X, Y)) >= X because [7], by (Select) 7] cons(X, Y) >= X because [8], by (Star) 8] cons*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] le(_|_, X) > _|_ because [16], by definition 16] le*(_|_, X) >= _|_ by (Bot) 17] le(X, _|_) >= _|_ by (Bot) 18] le(X, Y) >= le(X, Y) because le in Mul, [19] and [20], by (Fun) 19] X >= X by (Meta) 20] Y >= Y by (Meta) 21] @_{o -> o}(height, node(X, Y)) >= maxlist(_|_, map(height, Y)) because [22], by (Star) 22] @_{o -> o}*(height, node(X, Y)) >= maxlist(_|_, map(height, Y)) because [23], by (Select) 23] node(X, Y) >= maxlist(_|_, map(height, Y)) because [24], by (Star) 24] node*(X, Y) >= maxlist(_|_, map(height, Y)) because node > maxlist, [25] and [26], by (Copy) 25] node*(X, Y) >= _|_ by (Bot) 26] node*(X, Y) >= map(height, Y) because node > map, [27] and [28], by (Copy) 27] node*(X, Y) >= height because node > height, by (Copy) 28] node*(X, Y) >= Y because [29], by (Select) 29] Y >= Y by (Meta) We can thus remove the following rules: le(0, X) => true We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): map(F, cons(X, Y)) >? cons(F X, map(F, Y)) le(s(X), 0) >? false le(s(X), s(Y)) >? le(X, Y) height node(X, Y) >? s(maxlist(0, map(height, Y))) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, cons, height, le, map, maxlist, node, s}, and the following precedence: node > maxlist > s > le > height > @_{o -> o} = map > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) le(s(X), _|_) > _|_ le(s(X), s(Y)) >= le(X, Y) @_{o -> o}(height, node(X, Y)) > s(maxlist(_|_, map(height, Y))) With these choices, we have: 1] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [2], by (Star) 2] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [3] and [8], by (Copy) 3] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map = @_{o -> o}, map in Mul, [4] and [5], by (Stat) 4] F >= F by (Meta) 5] cons(X, Y) > X because [6], by definition 6] cons*(X, Y) >= X because [7], by (Select) 7] X >= X by (Meta) 8] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [4] and [9], by (Stat) 9] cons(X, Y) > Y because [10], by definition 10] cons*(X, Y) >= Y because [11], by (Select) 11] Y >= Y by (Meta) 12] le(s(X), _|_) > _|_ because [13], by definition 13] le*(s(X), _|_) >= _|_ by (Bot) 14] le(s(X), s(Y)) >= le(X, Y) because [15], by (Star) 15] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [16] and [19], by (Stat) 16] s(X) > X because [17], by definition 17] s*(X) >= X because [18], by (Select) 18] X >= X by (Meta) 19] s(Y) >= Y because [20], by (Star) 20] s*(Y) >= Y because [21], by (Select) 21] Y >= Y by (Meta) 22] @_{o -> o}(height, node(X, Y)) > s(maxlist(_|_, map(height, Y))) because [23], by definition 23] @_{o -> o}*(height, node(X, Y)) >= s(maxlist(_|_, map(height, Y))) because [24], by (Select) 24] node(X, Y) >= s(maxlist(_|_, map(height, Y))) because [25], by (Star) 25] node*(X, Y) >= s(maxlist(_|_, map(height, Y))) because node > s and [26], by (Copy) 26] node*(X, Y) >= maxlist(_|_, map(height, Y)) because node > maxlist, [27] and [28], by (Copy) 27] node*(X, Y) >= _|_ by (Bot) 28] node*(X, Y) >= map(height, Y) because node > map, [29] and [30], by (Copy) 29] node*(X, Y) >= height because node > height, by (Copy) 30] node*(X, Y) >= Y because [31], by (Select) 31] Y >= Y by (Meta) We can thus remove the following rules: le(s(X), 0) => false height node(X, Y) => s(maxlist(0, map(height, 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]): map(F, cons(X, Y)) >? cons(F X, map(F, Y)) le(s(X), s(Y)) >? le(X, Y) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {} and Mul = {@_{o -> o}, cons, le, map, s}, and the following precedence: map > cons > le > @_{o -> o} > s With these choices, we have: 1] map(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because [2], by (Star) 2] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [3] and [10], by (Copy) 3] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [4] and [6], by (Copy) 4] map*(F, cons(X, Y)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] map*(F, cons(X, Y)) >= X because [7], by (Select) 7] cons(X, Y) >= X because [8], by (Star) 8] cons*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map*(F, cons(X, Y)) >= map(F, Y) because map in Mul, [11] and [12], by (Stat) 11] F >= F by (Meta) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] le(s(X), s(Y)) > le(X, Y) because [16], by definition 16] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [17] and [20], by (Stat) 17] s(X) > X because [18], by definition 18] s*(X) >= X because [19], by (Select) 19] X >= X by (Meta) 20] s(Y) >= Y because [21], by (Star) 21] s*(Y) >= Y because [22], by (Select) 22] Y >= Y by (Meta) We can thus remove the following rules: le(s(X), s(Y)) => le(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]): map(F, cons(X, Y)) >? cons(F X, map(F, Y)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. We choose Lex = {map} and Mul = {@_{o -> o}, cons}, and the following precedence: map > @_{o -> o} > cons With these choices, we have: 1] map(F, cons(X, Y)) > cons(@_{o -> o}(F, X), map(F, Y)) because [2], by definition 2] map*(F, cons(X, Y)) >= cons(@_{o -> o}(F, X), map(F, Y)) because map > cons, [3] and [10], by (Copy) 3] map*(F, cons(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [4] and [6], by (Copy) 4] map*(F, cons(X, Y)) >= F because [5], by (Select) 5] F >= F by (Meta) 6] map*(F, cons(X, Y)) >= X because [7], by (Select) 7] cons(X, Y) >= X because [8], by (Star) 8] cons*(X, Y) >= X because [9], by (Select) 9] X >= X by (Meta) 10] map*(F, cons(X, Y)) >= map(F, Y) because [11], [12], [4] and [15], by (Stat) 11] F >= F by (Meta) 12] cons(X, Y) > Y because [13], by definition 13] cons*(X, Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] map*(F, cons(X, Y)) >= Y because [16], by (Select) 16] cons(X, Y) >= Y because [13], by (Star) We can thus remove the following rules: map(F, cons(X, Y)) => cons(F X, map(F, 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.