Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Transformed_CSR_04/Ex2_Luc03b_Z)

The rewrite relation of the following TRS is considered.

fst(0,Z)	→	nil	(1)
fst(s(X),cons(Y,Z))	→	cons(Y,n__fst(activate(X),activate(Z)))	(2)
from(X)	→	cons(X,n__from(s(X)))	(3)
add(0,X)	→	X	(4)
add(s(X),Y)	→	s(n__add(activate(X),Y))	(5)
len(nil)	→	0	(6)
len(cons(X,Z))	→	s(n__len(activate(Z)))	(7)
fst(X1,X2)	→	n__fst(X1,X2)	(8)
from(X)	→	n__from(X)	(9)
add(X1,X2)	→	n__add(X1,X2)	(10)
len(X)	→	n__len(X)	(11)
activate(n__fst(X1,X2))	→	fst(X1,X2)	(12)
activate(n__from(X))	→	from(X)	(13)
activate(n__add(X1,X2))	→	add(X1,X2)	(14)
activate(n__len(X))	→	len(X)	(15)
activate(X)	→	X	(16)

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:

fst^#(0,z0)

→

(18)

originates from

fst(0,z0)

→

nil

(17)

fst^#(s(z0),cons(z1,z2))

→

c1(activate^#(z0),activate^#(z2))

(20)

originates from

fst(s(z0),cons(z1,z2))

→

cons(z1,n__fst(activate(z0),activate(z2)))

(19)

fst^#(z0,z1)

→

(22)

originates from

fst(z0,z1)

→

n__fst(z0,z1)

(21)

from^#(z0)

→

(24)

originates from

from(z0)

→

cons(z0,n__from(s(z0)))

(23)

from^#(z0)

→

(26)

originates from

from(z0)

→

n__from(z0)

(25)

add^#(0,z0)

→

(28)

originates from

add(0,z0)

→

(27)

add^#(s(z0),z1)

→

c6(activate^#(z0))

(30)

originates from

add(s(z0),z1)

→

s(n__add(activate(z0),z1))

(29)

add^#(z0,z1)

→

(32)

originates from

add(z0,z1)

→

n__add(z0,z1)

(31)

len^#(nil)

→

(33)

originates from

len(nil)

→

(6)

len^#(cons(z0,z1))

→

c9(activate^#(z1))

(35)

originates from

len(cons(z0,z1))

→

s(n__len(activate(z1)))

(34)

len^#(z0)

→

c10

(37)

originates from

len(z0)

→

n__len(z0)

(36)

activate^#(n__fst(z0,z1))

→

c11(fst^#(z0,z1))

(39)

originates from

activate(n__fst(z0,z1))

→

fst(z0,z1)

(38)

activate^#(n__from(z0))

→

c12(from^#(z0))

(41)

originates from

activate(n__from(z0))

→

from(z0)

(40)

activate^#(n__add(z0,z1))

→

c13(add^#(z0,z1))

(43)

originates from

activate(n__add(z0,z1))

→

add(z0,z1)

(42)

activate^#(n__len(z0))

→

c14(len^#(z0))

(45)

originates from

activate(n__len(z0))

→

len(z0)

(44)

activate^#(z0)

→

c15

(47)

originates from

activate(z0)

→

(46)

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

fst^#(0,z0)

fst^#(s(z0),cons(z1,z2))

fst^#(z0,z1)

from^#(z0)

add^#(0,z0)

add^#(s(z0),z1)

add^#(z0,z1)

len^#(nil)

len^#(cons(z0,z1))

len^#(z0)

activate^#(n__fst(z0,z1))

activate^#(n__from(z0))

activate^#(n__add(z0,z1))

activate^#(n__len(z0))

activate^#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

fst(0,z0)	→	nil	(17)
fst(s(z0),cons(z1,z2))	→	cons(z1,n__fst(activate(z0),activate(z2)))	(19)
fst(z0,z1)	→	n__fst(z0,z1)	(21)
from(z0)	→	cons(z0,n__from(s(z0)))	(23)
from(z0)	→	n__from(z0)	(25)
add(0,z0)	→	z0	(27)
add(s(z0),z1)	→	s(n__add(activate(z0),z1))	(29)
add(z0,z1)	→	n__add(z0,z1)	(31)
len(nil)	→	0	(6)
len(cons(z0,z1))	→	s(n__len(activate(z1)))	(34)
len(z0)	→	n__len(z0)	(36)
activate(n__fst(z0,z1))	→	fst(z0,z1)	(38)
activate(n__from(z0))	→	from(z0)	(40)
activate(n__add(z0,z1))	→	add(z0,z1)	(42)
activate(n__len(z0))	→	len(z0)	(44)
activate(z0)	→	z0	(46)

1.1.1 Rule Shifting

The rules

fst^#(0,z0)	→	c	(18)
fst^#(s(z0),cons(z1,z2))	→	c1(activate^#(z0),activate^#(z2))	(20)
fst^#(z0,z1)	→	c2	(22)
from^#(z0)	→	c3	(24)
from^#(z0)	→	c4	(26)
add^#(0,z0)	→	c5	(28)
add^#(s(z0),z1)	→	c6(activate^#(z0))	(30)
add^#(z0,z1)	→	c7	(32)
len^#(nil)	→	c8	(33)
len^#(cons(z0,z1))	→	c9(activate^#(z1))	(35)
len^#(z0)	→	c10	(37)
activate^#(n__fst(z0,z1))	→	c11(fst^#(z0,z1))	(39)
activate^#(n__from(z0))	→	c12(from^#(z0))	(41)
activate^#(n__add(z0,z1))	→	c13(add^#(z0,z1))	(43)
activate^#(n__len(z0))	→	c14(len^#(z0))	(45)
activate^#(z0)	→	c15	(47)

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]	=	0
[c4]	=	0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[c10]	=	0
[c11(x₁)]	=	1 · x₁ + 0
[c12(x₁)]	=	1 · x₁ + 0
[c13(x₁)]	=	1 · x₁ + 0
[c14(x₁)]	=	1 · x₁ + 0
[c15]	=	0
[fst^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[from^#(x₁)]	=	1 + 1 · x₁
[add^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[len^#(x₁)]	=	1 + 1 · x₁
[activate^#(x₁)]	=	1 + 1 · x₁
[0]	=	1
[s(x₁)]	=	1 + 1 · x₁
[cons(x₁, x₂)]	=	1 + 1 · x₂
[nil]	=	1
[n__fst(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[n__from(x₁)]	=	1 + 1 · x₁
[n__add(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[n__len(x₁)]	=	1 + 1 · x₁

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

fst^#(0,z0)	→	c	(18)
fst^#(s(z0),cons(z1,z2))	→	c1(activate^#(z0),activate^#(z2))	(20)
fst^#(z0,z1)	→	c2	(22)
from^#(z0)	→	c3	(24)
from^#(z0)	→	c4	(26)
add^#(0,z0)	→	c5	(28)
add^#(s(z0),z1)	→	c6(activate^#(z0))	(30)
add^#(z0,z1)	→	c7	(32)
len^#(nil)	→	c8	(33)
len^#(cons(z0,z1))	→	c9(activate^#(z1))	(35)
len^#(z0)	→	c10	(37)
activate^#(n__fst(z0,z1))	→	c11(fst^#(z0,z1))	(39)
activate^#(n__from(z0))	→	c12(from^#(z0))	(41)
activate^#(n__add(z0,z1))	→	c13(add^#(z0,z1))	(43)
activate^#(n__len(z0))	→	c14(len^#(z0))	(45)
activate^#(z0)	→	c15	(47)

1.1.1.1 R is empty

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