Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/SK90/4.05)

The rewrite relation of the following TRS is considered.

*(x,+(y,z))	→	+((x,y),(x,z))	(1)
*(+(x,y),z)	→	+((x,z),(y,z))	(2)
*(x,1)	→	x	(3)
*(1,y)	→	y	(4)

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:

*^#(z0,+(z1,z2))

→

c(*^#(z0,z1),*^#(z0,z2))

(6)

originates from

*(z0,+(z1,z2))

→

+(*(z0,z1),*(z0,z2))

(5)

*^#(+(z0,z1),z2)

→

c1(*^#(z0,z2),*^#(z1,z2))

(8)

originates from

*(+(z0,z1),z2)

→

+(*(z0,z2),*(z1,z2))

(7)

*^#(z0,1)

→

(10)

originates from

*(z0,1)

→

(9)

*^#(1,z0)

→

(12)

originates from

*(1,z0)

→

(11)

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

*^#(z0,+(z1,z2))

*^#(+(z0,z1),z2)

*^#(z0,1)

*^#(1,z0)

1.1 Usable Rules

We remove the following rules since they are not usable.

*(z0,+(z1,z2))	→	+((z0,z1),(z0,z2))	(5)
*(+(z0,z1),z2)	→	+((z0,z2),(z1,z2))	(7)
*(z0,1)	→	z0	(9)
*(1,z0)	→	z0	(11)

1.1.1 Rule Shifting

The rules

*^#(+(z0,z1),z2)	→	c1(^#(z0,z2),^#(z1,z2))	(8)
*^#(1,z0)	→	c3	(12)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[*^#(x₁, x₂)]	=	1 · x₁ + 0 + 2 · x₁ · x₂
[+(x₁, x₂)]	=	2 + 1 · x₁ + 1 · x₂
[1]	=	1

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

*^#(z0,+(z1,z2))	→	c(^#(z0,z1),^#(z0,z2))	(6)
*^#(+(z0,z1),z2)	→	c1(^#(z0,z2),^#(z1,z2))	(8)
*^#(z0,1)	→	c2	(10)
*^#(1,z0)	→	c3	(12)

1.1.1.1 Rule Shifting

The rules

*^#(z0,+(z1,z2))	→	c(^#(z0,z1),^#(z0,z2))	(6)
*^#(z0,1)	→	c2	(10)

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

[c(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c1(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂
[c2]	=	0
[c3]	=	0
[*^#(x₁, x₂)]	=	1 · x₁ + 0 + 1 · x₂ · x₂ + 1 · x₁ · x₂ + 1 · x₁ · x₁ + 1 · x₂ · x₁ · x₁ + 1 · x₂ · x₂ · x₁
[+(x₁, x₂)]	=	1 + 1 · x₁ + 1 · x₂
[1]	=	1

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

*^#(z0,+(z1,z2))	→	c(^#(z0,z1),^#(z0,z2))	(6)
*^#(+(z0,z1),z2)	→	c1(^#(z0,z2),^#(z1,z2))	(8)
*^#(z0,1)	→	c2	(10)
*^#(1,z0)	→	c3	(12)

1.1.1.1.1 R is empty

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