Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Der95/32)

The rewrite relation of the following TRS is considered.

sort(nil)	→	nil	(1)
sort(cons(x,y))	→	insert(x,sort(y))	(2)
insert(x,nil)	→	cons(x,nil)	(3)
insert(x,cons(v,w))	→	choose(x,cons(v,w),x,v)	(4)
choose(x,cons(v,w),y,0)	→	cons(x,cons(v,w))	(5)
choose(x,cons(v,w),0,s(z))	→	cons(v,insert(x,w))	(6)
choose(x,cons(v,w),s(y),s(z))	→	choose(x,cons(v,w),y,z)	(7)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n²).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

sort^#(nil)

→

(8)

originates from

sort(nil)

→

nil

(1)

sort^#(cons(z0,z1))

→

c1(insert^#(z0,sort(z1)),sort^#(z1))

(10)

originates from

sort(cons(z0,z1))

→

insert(z0,sort(z1))

(9)

insert^#(z0,nil)

→

(12)

originates from

insert(z0,nil)

→

cons(z0,nil)

(11)

insert^#(z0,cons(z1,z2))

→

c3(choose^#(z0,cons(z1,z2),z0,z1))

(14)

originates from

insert(z0,cons(z1,z2))

→

choose(z0,cons(z1,z2),z0,z1)

(13)

choose^#(z0,cons(z1,z2),z3,0)

→

(16)

originates from

choose(z0,cons(z1,z2),z3,0)

→

cons(z0,cons(z1,z2))

(15)

choose^#(z0,cons(z1,z2),0,s(z3))

→

c5(insert^#(z0,z2))

(18)

originates from

choose(z0,cons(z1,z2),0,s(z3))

→

cons(z1,insert(z0,z2))

(17)

choose^#(z0,cons(z1,z2),s(z3),s(z4))

→

c6(choose^#(z0,cons(z1,z2),z3,z4))

(20)

originates from

choose(z0,cons(z1,z2),s(z3),s(z4))

→

choose(z0,cons(z1,z2),z3,z4)

(19)

Moreover, we add the following terms to the innermost strategy.

sort^#(nil)

sort^#(cons(z0,z1))

insert^#(z0,nil)

insert^#(z0,cons(z1,z2))

choose^#(z0,cons(z1,z2),z3,0)

choose^#(z0,cons(z1,z2),0,s(z3))

choose^#(z0,cons(z1,z2),s(z3),s(z4))

1.1 Rule Shifting

The rules

sort^#(nil)	→	c	(8)
insert^#(z0,nil)	→	c2	(12)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[sort(x₁)]	=	1 + 1 · x₁
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[choose(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂
[sort^#(x₁)]	=	1 · x₁ + 0
[insert^#(x₁, x₂)]	=	1 + 1 · x₁
[choose^#(x₁,...,x₄)]	=	1 + 1 · x₁
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

sort^#(nil)	→	c	(8)
sort^#(cons(z0,z1))	→	c1(insert^#(z0,sort(z1)),sort^#(z1))	(10)
insert^#(z0,nil)	→	c2	(12)
insert^#(z0,cons(z1,z2))	→	c3(choose^#(z0,cons(z1,z2),z0,z1))	(14)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)
choose^#(z0,cons(z1,z2),0,s(z3))	→	c5(insert^#(z0,z2))	(18)
choose^#(z0,cons(z1,z2),s(z3),s(z4))	→	c6(choose^#(z0,cons(z1,z2),z3,z4))	(20)

1.1.1 Rule Shifting

The rules

sort^#(cons(z0,z1))

→

c1(insert^#(z0,sort(z1)),sort^#(z1))

(10)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[sort(x₁)]	=	1 + 1 · x₁
[insert(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[choose(x₁,...,x₄)]	=	1 + 1 · x₁ + 1 · x₂
[sort^#(x₁)]	=	1 · x₁ + 0
[insert^#(x₁, x₂)]	=	1 · x₁ + 0
[choose^#(x₁,...,x₄)]	=	1 · x₁ + 0
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

sort^#(nil)	→	c	(8)
sort^#(cons(z0,z1))	→	c1(insert^#(z0,sort(z1)),sort^#(z1))	(10)
insert^#(z0,nil)	→	c2	(12)
insert^#(z0,cons(z1,z2))	→	c3(choose^#(z0,cons(z1,z2),z0,z1))	(14)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)
choose^#(z0,cons(z1,z2),0,s(z3))	→	c5(insert^#(z0,z2))	(18)
choose^#(z0,cons(z1,z2),s(z3),s(z4))	→	c6(choose^#(z0,cons(z1,z2),z3,z4))	(20)

1.1.1.1 Rule Shifting

The rules

choose^#(z0,cons(z1,z2),0,s(z3))

→

c5(insert^#(z0,z2))

(18)

are strictly oriented by the following non-linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[sort(x₁)]	=	1 · x₁ + 0
[insert(x₁, x₂)]	=	1 + 1 · x₂
[choose(x₁,...,x₄)]	=	1 + 1 · x₂
[sort^#(x₁)]	=	2 · x₁ · x₁ + 0
[insert^#(x₁, x₂)]	=	2 · x₂ + 0
[choose^#(x₁,...,x₄)]	=	2 · x₂ + 0
[nil]	=	0
[cons(x₁, x₂)]	=	1 + 1 · x₂
[0]	=	0
[s(x₁)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

sort^#(nil)	→	c	(8)
sort^#(cons(z0,z1))	→	c1(insert^#(z0,sort(z1)),sort^#(z1))	(10)
insert^#(z0,nil)	→	c2	(12)
insert^#(z0,cons(z1,z2))	→	c3(choose^#(z0,cons(z1,z2),z0,z1))	(14)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)
choose^#(z0,cons(z1,z2),0,s(z3))	→	c5(insert^#(z0,z2))	(18)
choose^#(z0,cons(z1,z2),s(z3),s(z4))	→	c6(choose^#(z0,cons(z1,z2),z3,z4))	(20)
choose(z0,cons(z1,z2),0,s(z3))	→	cons(z1,insert(z0,z2))	(17)
sort(nil)	→	nil	(1)
insert(z0,cons(z1,z2))	→	choose(z0,cons(z1,z2),z0,z1)	(13)
sort(cons(z0,z1))	→	insert(z0,sort(z1))	(9)
insert(z0,nil)	→	cons(z0,nil)	(11)
choose(z0,cons(z1,z2),z3,0)	→	cons(z0,cons(z1,z2))	(15)
choose(z0,cons(z1,z2),s(z3),s(z4))	→	choose(z0,cons(z1,z2),z3,z4)	(19)

1.1.1.1.1 Rule Shifting

The rules

insert^#(z0,cons(z1,z2))

→

c3(choose^#(z0,cons(z1,z2),z0,z1))

(14)

are strictly oriented by the following non-linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[sort(x₁)]	=	1 · x₁ + 0
[insert(x₁, x₂)]	=	2 + 1 · x₂
[choose(x₁,...,x₄)]	=	2 + 1 · x₂
[sort^#(x₁)]	=	2 · x₁ · x₁ + 0
[insert^#(x₁, x₂)]	=	1 + 1 · x₂
[choose^#(x₁,...,x₄)]	=	1 · x₂ + 0
[nil]	=	0
[cons(x₁, x₂)]	=	2 + 1 · x₂
[0]	=	0
[s(x₁)]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

sort^#(nil)	→	c	(8)
sort^#(cons(z0,z1))	→	c1(insert^#(z0,sort(z1)),sort^#(z1))	(10)
insert^#(z0,nil)	→	c2	(12)
insert^#(z0,cons(z1,z2))	→	c3(choose^#(z0,cons(z1,z2),z0,z1))	(14)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)
choose^#(z0,cons(z1,z2),0,s(z3))	→	c5(insert^#(z0,z2))	(18)
choose^#(z0,cons(z1,z2),s(z3),s(z4))	→	c6(choose^#(z0,cons(z1,z2),z3,z4))	(20)
choose(z0,cons(z1,z2),0,s(z3))	→	cons(z1,insert(z0,z2))	(17)
sort(nil)	→	nil	(1)
insert(z0,cons(z1,z2))	→	choose(z0,cons(z1,z2),z0,z1)	(13)
sort(cons(z0,z1))	→	insert(z0,sort(z1))	(9)
insert(z0,nil)	→	cons(z0,nil)	(11)
choose(z0,cons(z1,z2),z3,0)	→	cons(z0,cons(z1,z2))	(15)
choose(z0,cons(z1,z2),s(z3),s(z4))	→	choose(z0,cons(z1,z2),z3,z4)	(19)

1.1.1.1.1.1 Rule Shifting

The rules

choose^#(z0,cons(z1,z2),s(z3),s(z4))

→

c6(choose^#(z0,cons(z1,z2),z3,z4))

(20)

are strictly oriented by the following non-linear polynomial interpretation over the naturals

[c]	=	0
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3(x₁)]	=	1 · x₁ + 0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[sort(x₁)]	=	2 + 1 · x₁
[insert(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[choose(x₁,...,x₄)]	=	2 + 1 · x₁ + 1 · x₂
[sort^#(x₁)]	=	2 · x₁ · x₁ + 0
[insert^#(x₁, x₂)]	=	2 · x₁ + 0 + 1 · x₁ · x₂
[choose^#(x₁,...,x₄)]	=	2 · x₃ + 0 + 1 · x₂ · x₁
[nil]	=	0
[cons(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[0]	=	0
[s(x₁)]	=	2 + 1 · x₁

which has the intended complexity. Here, only the following usable rules have been considered:

sort^#(nil)	→	c	(8)
sort^#(cons(z0,z1))	→	c1(insert^#(z0,sort(z1)),sort^#(z1))	(10)
insert^#(z0,nil)	→	c2	(12)
insert^#(z0,cons(z1,z2))	→	c3(choose^#(z0,cons(z1,z2),z0,z1))	(14)
choose^#(z0,cons(z1,z2),z3,0)	→	c4	(16)
choose^#(z0,cons(z1,z2),0,s(z3))	→	c5(insert^#(z0,z2))	(18)
choose^#(z0,cons(z1,z2),s(z3),s(z4))	→	c6(choose^#(z0,cons(z1,z2),z3,z4))	(20)
choose(z0,cons(z1,z2),0,s(z3))	→	cons(z1,insert(z0,z2))	(17)
sort(nil)	→	nil	(1)
insert(z0,cons(z1,z2))	→	choose(z0,cons(z1,z2),z0,z1)	(13)
sort(cons(z0,z1))	→	insert(z0,sort(z1))	(9)
insert(z0,nil)	→	cons(z0,nil)	(11)
choose(z0,cons(z1,z2),z3,0)	→	cons(z0,cons(z1,z2))	(15)
choose(z0,cons(z1,z2),s(z3),s(z4))	→	choose(z0,cons(z1,z2),z3,z4)	(19)

1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).