Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/select)

The rewrite relation of the following TRS is considered.

selects(x',revprefix,Cons(x,xs))	→	Cons(Cons(x',revapp(revprefix,Cons(x,xs))),selects(x,Cons(x',revprefix),xs))	(1)
select(Cons(x,xs))	→	selects(x,Nil,xs)	(2)
revapp(Cons(x,xs),rest)	→	revapp(xs,Cons(x,rest))	(3)
selects(x,revprefix,Nil)	→	Cons(Cons(x,revapp(revprefix,Nil)),Nil)	(4)
select(Nil)	→	Nil	(5)
revapp(Nil,rest)	→	rest	(6)

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:

selects^#(z0,z1,Cons(z2,z3))

→

c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))

(8)

originates from

selects(z0,z1,Cons(z2,z3))

→

Cons(Cons(z0,revapp(z1,Cons(z2,z3))),selects(z2,Cons(z0,z1),z3))

(7)

selects^#(z0,z1,Nil)

→

c1(revapp^#(z1,Nil))

(10)

originates from

selects(z0,z1,Nil)

→

Cons(Cons(z0,revapp(z1,Nil)),Nil)

(9)

select^#(Cons(z0,z1))

→

c2(selects^#(z0,Nil,z1))

(12)

originates from

select(Cons(z0,z1))

→

selects(z0,Nil,z1)

(11)

select^#(Nil)

→

(13)

originates from

select(Nil)

→

Nil

(5)

revapp^#(Cons(z0,z1),z2)

→

c4(revapp^#(z1,Cons(z0,z2)))

(15)

originates from

revapp(Cons(z0,z1),z2)

→

revapp(z1,Cons(z0,z2))

(14)

revapp^#(Nil,z0)

→

(17)

originates from

revapp(Nil,z0)

→

(16)

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

selects^#(z0,z1,Cons(z2,z3))

selects^#(z0,z1,Nil)

select^#(Cons(z0,z1))

select^#(Nil)

revapp^#(Cons(z0,z1),z2)

revapp^#(Nil,z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

selects(z0,z1,Cons(z2,z3))	→	Cons(Cons(z0,revapp(z1,Cons(z2,z3))),selects(z2,Cons(z0,z1),z3))	(7)
selects(z0,z1,Nil)	→	Cons(Cons(z0,revapp(z1,Nil)),Nil)	(9)
select(Cons(z0,z1))	→	selects(z0,Nil,z1)	(11)
select(Nil)	→	Nil	(5)
revapp(Cons(z0,z1),z2)	→	revapp(z1,Cons(z0,z2))	(14)
revapp(Nil,z0)	→	z0	(16)

1.1.1 Rule Shifting

The rules

select^#(Nil)

→

(13)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[selects^#(x₁, x₂, x₃)]	=	0
[select^#(x₁)]	=	1 · x₁ + 0 + 1 · x₁ · x₁ + 1 · x₁ · x₁ · x₁
[revapp^#(x₁, x₂)]	=	0
[Cons(x₁, x₂)]	=	0
[Nil]	=	1

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

selects^#(z0,z1,Cons(z2,z3))	→	c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))	(8)
selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)
select^#(Nil)	→	c3	(13)
revapp^#(Cons(z0,z1),z2)	→	c4(revapp^#(z1,Cons(z0,z2)))	(15)
revapp^#(Nil,z0)	→	c5	(17)

1.1.1.1 Rule Shifting

The rules

selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[selects^#(x₁, x₂, x₃)]	=	3
[select^#(x₁)]	=	2 + 3 · x₁
[revapp^#(x₁, x₂)]	=	0
[Cons(x₁, x₂)]	=	3 + 1 · x₁
[Nil]	=	0

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

selects^#(z0,z1,Cons(z2,z3))	→	c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))	(8)
selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)
select^#(Nil)	→	c3	(13)
revapp^#(Cons(z0,z1),z2)	→	c4(revapp^#(z1,Cons(z0,z2)))	(15)
revapp^#(Nil,z0)	→	c5	(17)

1.1.1.1.1 Rule Shifting

The rules

selects^#(z0,z1,Cons(z2,z3))

→

c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))

(8)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[selects^#(x₁, x₂, x₃)]	=	1 + 1 · x₁ + 1 · x₃
[select^#(x₁)]	=	1 · x₁ + 0
[revapp^#(x₁, x₂)]	=	0
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Nil]	=	1

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

selects^#(z0,z1,Cons(z2,z3))	→	c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))	(8)
selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)
select^#(Nil)	→	c3	(13)
revapp^#(Cons(z0,z1),z2)	→	c4(revapp^#(z1,Cons(z0,z2)))	(15)
revapp^#(Nil,z0)	→	c5	(17)

1.1.1.1.1.1 Rule Shifting

The rules

revapp^#(Nil,z0)

→

(17)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[selects^#(x₁, x₂, x₃)]	=	1 · x₁ + 0 + 1 · x₃
[select^#(x₁)]	=	1 + 1 · x₁
[revapp^#(x₁, x₂)]	=	1
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Nil]	=	1

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

selects^#(z0,z1,Cons(z2,z3))	→	c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))	(8)
selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)
select^#(Nil)	→	c3	(13)
revapp^#(Cons(z0,z1),z2)	→	c4(revapp^#(z1,Cons(z0,z2)))	(15)
revapp^#(Nil,z0)	→	c5	(17)

1.1.1.1.1.1.1 Rule Shifting

The rules

revapp^#(Cons(z0,z1),z2)

→

c4(revapp^#(z1,Cons(z0,z2)))

(15)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁)]	=	1 · x₁ + 0
[c2(x₁)]	=	1 · x₁ + 0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[selects^#(x₁, x₂, x₃)]	=	1 · x₂ + 0 + 1 · x₃ · x₃ + 2 · x₂ · x₃
[select^#(x₁)]	=	2 · x₁ · x₁ + 0
[revapp^#(x₁, x₂)]	=	1 · x₁ + 0
[Cons(x₁, x₂)]	=	1 + 1 · x₂
[Nil]	=	0

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

selects^#(z0,z1,Cons(z2,z3))	→	c(revapp^#(z1,Cons(z2,z3)),selects^#(z2,Cons(z0,z1),z3))	(8)
selects^#(z0,z1,Nil)	→	c1(revapp^#(z1,Nil))	(10)
select^#(Cons(z0,z1))	→	c2(selects^#(z0,Nil,z1))	(12)
select^#(Nil)	→	c3	(13)
revapp^#(Cons(z0,z1),z2)	→	c4(revapp^#(z1,Cons(z0,z2)))	(15)
revapp^#(Nil,z0)	→	c5	(17)

1.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).