Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/match)

The relative rewrite relation R/S is considered where R is the following TRS

loop(Cons(x,xs),Nil,pp,ss)	→	False	(1)
loop(Cons(x',xs'),Cons(x,xs),pp,ss)	→	loop[Ite](!EQ(x',x),Cons(x',xs'),Cons(x,xs),pp,ss)	(2)
loop(Nil,s,pp,ss)	→	True	(3)
match1(p,s)	→	loop(p,s,p,s)	(4)

and S is the following TRS.

!EQ(S(x),S(y))	→	!EQ(x,y)	(5)
!EQ(0,S(y))	→	False	(6)
!EQ(S(x),0)	→	False	(7)
!EQ(0,0)	→	True	(8)
loop[Ite](False,p,s,pp,Cons(x,xs))	→	loop(pp,xs,pp,xs)	(9)
loop[Ite](True,Cons(x',xs'),Cons(x,xs),pp,ss)	→	loop(xs',xs,pp,ss)	(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:

loop^#(Cons(z0,z1),Nil,z2,z3)

→

(12)

originates from

loop(Cons(z0,z1),Nil,z2,z3)

→

False

(11)

loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)

→

c7(loop[Ite]^#(!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5),!EQ^#(z0,z2))

(14)

originates from

loop(Cons(z0,z1),Cons(z2,z3),z4,z5)

→

loop[Ite](!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5)

(13)

loop^#(Nil,z0,z1,z2)

→

(16)

originates from

loop(Nil,z0,z1,z2)

→

True

(15)

match1^#(z0,z1)

→

c9(loop^#(z0,z1,z0,z1))

(18)

originates from

match1(z0,z1)

→

loop(z0,z1,z0,z1)

(17)

!EQ^#(S(z0),S(z1))

→

c(!EQ^#(z0,z1))

(20)

originates from

!EQ(S(z0),S(z1))

→

!EQ(z0,z1)

(19)

!EQ^#(0,S(z0))

→

(22)

originates from

!EQ(0,S(z0))

→

False

(21)

!EQ^#(S(z0),0)

→

(24)

originates from

!EQ(S(z0),0)

→

False

(23)

!EQ^#(0,0)

→

(25)

originates from

!EQ(0,0)

→

True

(8)

loop[Ite]^#(False,z0,z1,z2,Cons(z3,z4))

→

c4(loop^#(z2,z4,z2,z4))

(27)

originates from

loop[Ite](False,z0,z1,z2,Cons(z3,z4))

→

loop(z2,z4,z2,z4)

(26)

loop[Ite]^#(True,Cons(z0,z1),Cons(z2,z3),z4,z5)

→

c5(loop^#(z1,z3,z4,z5))

(29)

originates from

loop[Ite](True,Cons(z0,z1),Cons(z2,z3),z4,z5)

→

loop(z1,z3,z4,z5)

(28)

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

!EQ^#(S(z0),S(z1))

!EQ^#(0,S(z0))

!EQ^#(S(z0),0)

!EQ^#(0,0)

loop[Ite]^#(False,z0,z1,z2,Cons(z3,z4))

loop[Ite]^#(True,Cons(z0,z1),Cons(z2,z3),z4,z5)

loop^#(Cons(z0,z1),Nil,z2,z3)

loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)

loop^#(Nil,z0,z1,z2)

match1^#(z0,z1)

1.1 Usable Rules

We remove the following rules since they are not usable.

loop[Ite](False,z0,z1,z2,Cons(z3,z4))	→	loop(z2,z4,z2,z4)	(26)
loop[Ite](True,Cons(z0,z1),Cons(z2,z3),z4,z5)	→	loop(z1,z3,z4,z5)	(28)
loop(Cons(z0,z1),Nil,z2,z3)	→	False	(11)
loop(Cons(z0,z1),Cons(z2,z3),z4,z5)	→	loop[Ite](!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5)	(13)
loop(Nil,z0,z1,z2)	→	True	(15)
match1(z0,z1)	→	loop(z0,z1,z0,z1)	(17)

1.1.1 Rule Shifting

The rules

match1^#(z0,z1)

→

c9(loop^#(z0,z1,z0,z1))

(18)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[!EQ(x₁, x₂)]	=	3 + 3 · x₁
[!EQ^#(x₁, x₂)]	=	0
[loop[Ite]^#(x₁,...,x₅)]	=	3 · x₂ + 0 + 2 · x₄
[loop^#(x₁,...,x₄)]	=	2 · x₃ + 0
[match1^#(x₁, x₂)]	=	1 + 3 · x₁
[S(x₁)]	=	3 + 1 · x₁
[0]	=	3
[False]	=	3
[True]	=	3
[Cons(x₁, x₂)]	=	0
[Nil]	=	3

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

!EQ^#(S(z0),S(z1))	→	c(!EQ^#(z0,z1))	(20)
!EQ^#(0,S(z0))	→	c1	(22)
!EQ^#(S(z0),0)	→	c2	(24)
!EQ^#(0,0)	→	c3	(25)
loop[Ite]^#(False,z0,z1,z2,Cons(z3,z4))	→	c4(loop^#(z2,z4,z2,z4))	(27)
loop[Ite]^#(True,Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c5(loop^#(z1,z3,z4,z5))	(29)
loop^#(Cons(z0,z1),Nil,z2,z3)	→	c6	(12)
loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c7(loop[Ite]^#(!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5),!EQ^#(z0,z2))	(14)
loop^#(Nil,z0,z1,z2)	→	c8	(16)
match1^#(z0,z1)	→	c9(loop^#(z0,z1,z0,z1))	(18)

1.1.1.1 Rule Shifting

The rules

loop^#(Cons(z0,z1),Nil,z2,z3)	→	c6	(12)
loop^#(Nil,z0,z1,z2)	→	c8	(16)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[!EQ(x₁, x₂)]	=	0
[!EQ^#(x₁, x₂)]	=	0
[loop[Ite]^#(x₁,...,x₅)]	=	1 + 1 · x₁ + 1 · x₄ + 1 · x₅
[loop^#(x₁,...,x₄)]	=	1 + 1 · x₃ + 1 · x₄
[match1^#(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1
[False]	=	0
[True]	=	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:

!EQ^#(S(z0),S(z1))	→	c(!EQ^#(z0,z1))	(20)
!EQ^#(0,S(z0))	→	c1	(22)
!EQ^#(S(z0),0)	→	c2	(24)
!EQ^#(0,0)	→	c3	(25)
loop[Ite]^#(False,z0,z1,z2,Cons(z3,z4))	→	c4(loop^#(z2,z4,z2,z4))	(27)
loop[Ite]^#(True,Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c5(loop^#(z1,z3,z4,z5))	(29)
loop^#(Cons(z0,z1),Nil,z2,z3)	→	c6	(12)
loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c7(loop[Ite]^#(!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5),!EQ^#(z0,z2))	(14)
loop^#(Nil,z0,z1,z2)	→	c8	(16)
match1^#(z0,z1)	→	c9(loop^#(z0,z1,z0,z1))	(18)
!EQ(0,S(z0))	→	False	(21)
!EQ(S(z0),0)	→	False	(23)
!EQ(S(z0),S(z1))	→	!EQ(z0,z1)	(19)
!EQ(0,0)	→	True	(8)

1.1.1.1.1 Rule Shifting

The rules

loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)

→

c7(loop[Ite]^#(!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5),!EQ^#(z0,z2))

(14)

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

[c(x₁)]	=	1 · x₁ + 0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5(x₁)]	=	1 · x₁ + 0
[c6]	=	0
[c7(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c8]	=	0
[c9(x₁)]	=	1 · x₁ + 0
[!EQ(x₁, x₂)]	=	0
[!EQ^#(x₁, x₂)]	=	0
[loop[Ite]^#(x₁,...,x₅)]	=	1 · x₃ + 0 + 2 · x₅ · x₅ + 2 · x₄ · x₄
[loop^#(x₁,...,x₄)]	=	1 + 1 · x₂ + 2 · x₄ · x₄ + 2 · x₃ · x₃
[match1^#(x₁, x₂)]	=	2 + 2 · x₁ + 1 · x₂ + 2 · x₂ · x₂ + 1 · x₁ · x₂ + 2 · x₁ · x₁
[S(x₁)]	=	0
[0]	=	0
[False]	=	0
[True]	=	0
[Cons(x₁, x₂)]	=	2 + 1 · x₂
[Nil]	=	0

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

!EQ^#(S(z0),S(z1))	→	c(!EQ^#(z0,z1))	(20)
!EQ^#(0,S(z0))	→	c1	(22)
!EQ^#(S(z0),0)	→	c2	(24)
!EQ^#(0,0)	→	c3	(25)
loop[Ite]^#(False,z0,z1,z2,Cons(z3,z4))	→	c4(loop^#(z2,z4,z2,z4))	(27)
loop[Ite]^#(True,Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c5(loop^#(z1,z3,z4,z5))	(29)
loop^#(Cons(z0,z1),Nil,z2,z3)	→	c6	(12)
loop^#(Cons(z0,z1),Cons(z2,z3),z4,z5)	→	c7(loop[Ite]^#(!EQ(z0,z2),Cons(z0,z1),Cons(z2,z3),z4,z5),!EQ^#(z0,z2))	(14)
loop^#(Nil,z0,z1,z2)	→	c8	(16)
match1^#(z0,z1)	→	c9(loop^#(z0,z1,z0,z1))	(18)

1.1.1.1.1.1 R is empty

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