Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/fold)

The rewrite relation of the following TRS is considered.

foldl(x,Cons(S(0),xs))	→	foldl(S(x),xs)	(1)
foldl(S(0),Cons(x,xs))	→	foldl(S(x),xs)	(2)
foldr(a,Cons(x,xs))	→	op(x,foldr(a,xs))	(3)
foldr(a,Nil)	→	a	(4)
foldl(a,Nil)	→	a	(5)
notEmpty(Cons(x,xs))	→	True	(6)
notEmpty(Nil)	→	False	(7)
op(x,S(0))	→	S(x)	(8)
op(S(0),y)	→	S(y)	(9)
fold(a,xs)	→	Cons(foldl(a,xs),Cons(foldr(a,xs),Nil))	(10)

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:

foldl^#(z0,Cons(S(0),z1))

→

c(foldl^#(S(z0),z1))

(12)

originates from

foldl(z0,Cons(S(0),z1))

→

foldl(S(z0),z1)

(11)

foldl^#(S(0),Cons(z0,z1))

→

c1(foldl^#(S(z0),z1))

(14)

originates from

foldl(S(0),Cons(z0,z1))

→

foldl(S(z0),z1)

(13)

foldl^#(z0,Nil)

→

(16)

originates from

foldl(z0,Nil)

→

(15)

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

→

c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))

(18)

originates from

foldr(z0,Cons(z1,z2))

→

op(z1,foldr(z0,z2))

(17)

foldr^#(z0,Nil)

→

(20)

originates from

foldr(z0,Nil)

→

(19)

notEmpty^#(Cons(z0,z1))

→

(22)

originates from

notEmpty(Cons(z0,z1))

→

True

(21)

notEmpty^#(Nil)

→

(23)

originates from

notEmpty(Nil)

→

False

(7)

op^#(z0,S(0))

→

(25)

originates from

op(z0,S(0))

→

S(z0)

(24)

op^#(S(0),z0)

→

(27)

originates from

op(S(0),z0)

→

S(z0)

(26)

fold^#(z0,z1)

→

c9(foldl^#(z0,z1),foldr^#(z0,z1))

(29)

originates from

fold(z0,z1)

→

Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil))

(28)

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

foldl^#(z0,Cons(S(0),z1))

foldl^#(S(0),Cons(z0,z1))

foldl^#(z0,Nil)

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

foldr^#(z0,Nil)

notEmpty^#(Cons(z0,z1))

notEmpty^#(Nil)

op^#(z0,S(0))

op^#(S(0),z0)

fold^#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.

foldl(z0,Cons(S(0),z1))	→	foldl(S(z0),z1)	(11)
foldl(S(0),Cons(z0,z1))	→	foldl(S(z0),z1)	(13)
foldl(z0,Nil)	→	z0	(15)
notEmpty(Cons(z0,z1))	→	True	(21)
notEmpty(Nil)	→	False	(7)
fold(z0,z1)	→	Cons(foldl(z0,z1),Cons(foldr(z0,z1),Nil))	(28)

1.1.1 Rule Shifting

The rules

foldl^#(z0,Cons(S(0),z1))	→	c(foldl^#(S(z0),z1))	(12)
foldl^#(S(0),Cons(z0,z1))	→	c1(foldl^#(S(z0),z1))	(14)
foldl^#(z0,Nil)	→	c2	(16)
notEmpty^#(Cons(z0,z1))	→	c5	(22)
notEmpty^#(Nil)	→	c6	(23)
fold^#(z0,z1)	→	c9(foldl^#(z0,z1),foldr^#(z0,z1))	(29)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[op(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldl^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr^#(x₁, x₂)]	=	0
[notEmpty^#(x₁)]	=	1 + 1 · x₁
[op^#(x₁, x₂)]	=	0
[fold^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Cons(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[Nil]	=	1
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

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

foldl^#(z0,Cons(S(0),z1))	→	c(foldl^#(S(z0),z1))	(12)
foldl^#(S(0),Cons(z0,z1))	→	c1(foldl^#(S(z0),z1))	(14)
foldl^#(z0,Nil)	→	c2	(16)
foldr^#(z0,Cons(z1,z2))	→	c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))	(18)
foldr^#(z0,Nil)	→	c4	(20)
notEmpty^#(Cons(z0,z1))	→	c5	(22)
notEmpty^#(Nil)	→	c6	(23)
op^#(z0,S(0))	→	c7	(25)
op^#(S(0),z0)	→	c8	(27)
fold^#(z0,z1)	→	c9(foldl^#(z0,z1),foldr^#(z0,z1))	(29)

1.1.1.1 Rule Shifting

The rules

foldr^#(z0,Nil)

→

(20)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[op(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[foldl^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr^#(x₁, x₂)]	=	1
[notEmpty^#(x₁)]	=	0
[op^#(x₁, x₂)]	=	0
[fold^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Nil]	=	1
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

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

foldl^#(z0,Cons(S(0),z1))	→	c(foldl^#(S(z0),z1))	(12)
foldl^#(S(0),Cons(z0,z1))	→	c1(foldl^#(S(z0),z1))	(14)
foldl^#(z0,Nil)	→	c2	(16)
foldr^#(z0,Cons(z1,z2))	→	c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))	(18)
foldr^#(z0,Nil)	→	c4	(20)
notEmpty^#(Cons(z0,z1))	→	c5	(22)
notEmpty^#(Nil)	→	c6	(23)
op^#(z0,S(0))	→	c7	(25)
op^#(S(0),z0)	→	c8	(27)
fold^#(z0,z1)	→	c9(foldl^#(z0,z1),foldr^#(z0,z1))	(29)

1.1.1.1.1 Rule Shifting

The rules

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

→

c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))

(18)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[op(x₁, x₂)]	=	3
[foldl^#(x₁, x₂)]	=	1 + 3 · x₁ + 2 · x₂
[foldr^#(x₁, x₂)]	=	2 + 1 · x₂
[notEmpty^#(x₁)]	=	0
[op^#(x₁, x₂)]	=	0
[fold^#(x₁, x₂)]	=	3 + 3 · x₁ + 3 · x₂
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[Nil]	=	0
[S(x₁)]	=	0
[0]	=	0

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

foldl^#(z0,Cons(S(0),z1))	→	c(foldl^#(S(z0),z1))	(12)
foldl^#(S(0),Cons(z0,z1))	→	c1(foldl^#(S(z0),z1))	(14)
foldl^#(z0,Nil)	→	c2	(16)
foldr^#(z0,Cons(z1,z2))	→	c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))	(18)
foldr^#(z0,Nil)	→	c4	(20)
notEmpty^#(Cons(z0,z1))	→	c5	(22)
notEmpty^#(Nil)	→	c6	(23)
op^#(z0,S(0))	→	c7	(25)
op^#(S(0),z0)	→	c8	(27)
fold^#(z0,z1)	→	c9(foldl^#(z0,z1),foldr^#(z0,z1))	(29)

1.1.1.1.1.1 Rule Shifting

The rules

op^#(z0,S(0))	→	c7	(25)
op^#(S(0),z0)	→	c8	(27)

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

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c4]	=	0
[c5]	=	0
[c6]	=	0
[c7]	=	0
[c8]	=	0
[c9(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[foldr(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[op(x₁, x₂)]	=	1 + 1 · x₁
[foldl^#(x₁, x₂)]	=	1
[foldr^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[notEmpty^#(x₁)]	=	0
[op^#(x₁, x₂)]	=	1 + 1 · x₁
[fold^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Cons(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[Nil]	=	0
[S(x₁)]	=	1
[0]	=	1

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

foldl^#(z0,Cons(S(0),z1))	→	c(foldl^#(S(z0),z1))	(12)
foldl^#(S(0),Cons(z0,z1))	→	c1(foldl^#(S(z0),z1))	(14)
foldl^#(z0,Nil)	→	c2	(16)
foldr^#(z0,Cons(z1,z2))	→	c3(op^#(z1,foldr(z0,z2)),foldr^#(z0,z2))	(18)
foldr^#(z0,Nil)	→	c4	(20)
notEmpty^#(Cons(z0,z1))	→	c5	(22)
notEmpty^#(Nil)	→	c6	(23)
op^#(z0,S(0))	→	c7	(25)
op^#(S(0),z0)	→	c8	(27)
fold^#(z0,z1)	→	c9(foldl^#(z0,z1),foldr^#(z0,z1))	(29)

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