Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/CiME_04/append)

The rewrite relation of the following TRS is considered.

is_empty(nil)	→	true	(1)
is_empty(cons(x,l))	→	false	(2)
hd(cons(x,l))	→	x	(3)
tl(cons(x,l))	→	l	(4)
append(l1,l2)	→	ifappend(l1,l2,l1)	(5)
ifappend(l1,l2,nil)	→	l2	(6)
ifappend(l1,l2,cons(x,l))	→	cons(x,append(l,l2))	(7)

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:

is_empty^#(nil)

→

(8)

originates from

is_empty(nil)

→

true

(1)

is_empty^#(cons(z0,z1))

→

(10)

originates from

is_empty(cons(z0,z1))

→

false

(9)

hd^#(cons(z0,z1))

→

(12)

originates from

hd(cons(z0,z1))

→

(11)

tl^#(cons(z0,z1))

→

(14)

originates from

tl(cons(z0,z1))

→

(13)

append^#(z0,z1)

→

c4(ifappend^#(z0,z1,z0))

(16)

originates from

append(z0,z1)

→

ifappend(z0,z1,z0)

(15)

ifappend^#(z0,z1,nil)

→

(18)

originates from

ifappend(z0,z1,nil)

→

(17)

ifappend^#(z0,z1,cons(z2,z3))

→

c6(append^#(z3,z1))

(20)

originates from

ifappend(z0,z1,cons(z2,z3))

→

cons(z2,append(z3,z1))

(19)

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

is_empty^#(nil)

is_empty^#(cons(z0,z1))

hd^#(cons(z0,z1))

tl^#(cons(z0,z1))

append^#(z0,z1)

ifappend^#(z0,z1,nil)

ifappend^#(z0,z1,cons(z2,z3))

1.1 Usable Rules

We remove the following rules since they are not usable.

is_empty(nil)	→	true	(1)
is_empty(cons(z0,z1))	→	false	(9)
hd(cons(z0,z1))	→	z0	(11)
tl(cons(z0,z1))	→	z1	(13)
append(z0,z1)	→	ifappend(z0,z1,z0)	(15)
ifappend(z0,z1,nil)	→	z1	(17)
ifappend(z0,z1,cons(z2,z3))	→	cons(z2,append(z3,z1))	(19)

1.1.1 Rule Shifting

The rules

is_empty^#(nil)	→	c	(8)
is_empty^#(cons(z0,z1))	→	c1	(10)
hd^#(cons(z0,z1))	→	c2	(12)
tl^#(cons(z0,z1))	→	c3	(14)
append^#(z0,z1)	→	c4(ifappend^#(z0,z1,z0))	(16)
ifappend^#(z0,z1,nil)	→	c5	(18)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[is_empty^#(x₁)]	=	1 + 1 · x₁
[hd^#(x₁)]	=	1 · x₁ + 0
[tl^#(x₁)]	=	1 · x₁ + 0
[append^#(x₁, x₂)]	=	1 + 1 · x₁
[ifappend^#(x₁, x₂, x₃)]	=	1 · x₃ + 0
[nil]	=	1
[cons(x₁, x₂)]	=	1 + 1 · x₂

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

is_empty^#(nil)	→	c	(8)
is_empty^#(cons(z0,z1))	→	c1	(10)
hd^#(cons(z0,z1))	→	c2	(12)
tl^#(cons(z0,z1))	→	c3	(14)
append^#(z0,z1)	→	c4(ifappend^#(z0,z1,z0))	(16)
ifappend^#(z0,z1,nil)	→	c5	(18)
ifappend^#(z0,z1,cons(z2,z3))	→	c6(append^#(z3,z1))	(20)

1.1.1.1 Rule Shifting

The rules

ifappend^#(z0,z1,cons(z2,z3))

→

c6(append^#(z3,z1))

(20)

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

[c]	=	0
[c1]	=	0
[c2]	=	0
[c3]	=	0
[c4(x₁)]	=	1 · x₁ + 0
[c5]	=	0
[c6(x₁)]	=	1 · x₁ + 0
[is_empty^#(x₁)]	=	0
[hd^#(x₁)]	=	0
[tl^#(x₁)]	=	0
[append^#(x₁, x₂)]	=	1 + 1 · x₁
[ifappend^#(x₁, x₂, x₃)]	=	1 + 1 · x₃
[nil]	=	0
[cons(x₁, x₂)]	=	1 + 1 · x₂

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

is_empty^#(nil)	→	c	(8)
is_empty^#(cons(z0,z1))	→	c1	(10)
hd^#(cons(z0,z1))	→	c2	(12)
tl^#(cons(z0,z1))	→	c3	(14)
append^#(z0,z1)	→	c4(ifappend^#(z0,z1,z0))	(16)
ifappend^#(z0,z1,nil)	→	c5	(18)
ifappend^#(z0,z1,cons(z2,z3))	→	c6(append^#(z3,z1))	(20)

1.1.1.1.1 R is empty

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