Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Glenstrup/shuffle)

The rewrite relation of the following TRS is considered.

shuffle(Cons(x,xs)) → Cons(x,shuffle(reverse(xs))) (1)
reverse(Cons(x,xs)) → append(reverse(xs),Cons(x,Nil)) (2)
append(Cons(x,xs),ys) → Cons(x,append(xs,ys)) (3)
shuffle(Nil) → Nil (4)
reverse(Nil) → Nil (5)
append(Nil,ys) → ys (6)
goal(xs) → shuffle(xs) (7)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n3).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
originates from
shuffle(Cons(z0,z1)) → Cons(z0,shuffle(reverse(z1))) (8)
shuffle#(Nil) → c1 (10)
originates from
shuffle(Nil) → Nil (4)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
originates from
reverse(Cons(z0,z1)) → append(reverse(z1),Cons(z0,Nil)) (11)
reverse#(Nil) → c3 (13)
originates from
reverse(Nil) → Nil (5)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
originates from
append(Cons(z0,z1),z2) → Cons(z0,append(z1,z2)) (14)
append#(Nil,z0) → c5 (17)
originates from
append(Nil,z0) → z0 (16)
goal#(z0) → c6(shuffle#(z0)) (19)
originates from
goal(z0) → shuffle(z0) (18)
Moreover, we add the following terms to the innermost strategy.
shuffle#(Cons(z0,z1))
shuffle#(Nil)
reverse#(Cons(z0,z1))
reverse#(Nil)
append#(Cons(z0,z1),z2)
append#(Nil,z0)
goal#(z0)

1.1 Usable Rules

We remove the following rules since they are not usable.
shuffle(Cons(z0,z1)) → Cons(z0,shuffle(reverse(z1))) (8)
shuffle(Nil) → Nil (4)
goal(z0) → shuffle(z0) (18)

1.1.1 Rule Shifting

The rules
goal#(z0) → c6(shuffle#(z0)) (19)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1
[append(x1, x2)] = 1 · x2 + 0
[shuffle#(x1)] = 0
[reverse#(x1)] = 0
[append#(x1, x2)] = 3 · x2 + 0
[goal#(x1)] = 1
[Cons(x1, x2)] = 0
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)

1.1.1.1 Rule Shifting

The rules
shuffle#(Nil) → c1 (10)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1
[append(x1, x2)] = 1 + 1 · x1 + 1 · x2
[shuffle#(x1)] = 1
[reverse#(x1)] = 0
[append#(x1, x2)] = 0
[goal#(x1)] = 1
[Cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[Nil] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)

1.1.1.1.1 Rule Shifting

The rules
reverse#(Nil) → c3 (13)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[shuffle#(x1)] = 1 + 1 · x1
[reverse#(x1)] = 1
[append#(x1, x2)] = 0
[goal#(x1)] = 1 + 1 · x1
[Cons(x1, x2)] = 1 + 1 · x1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)
append(Cons(z0,z1),z2) → Cons(z0,append(z1,z2)) (14)
reverse(Cons(z0,z1)) → append(reverse(z1),Cons(z0,Nil)) (11)
reverse(Nil) → Nil (5)
append(Nil,z0) → z0 (16)

1.1.1.1.1.1 Rule Shifting

The rules
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[shuffle#(x1)] = 3 + 2 · x1
[reverse#(x1)] = 1
[append#(x1, x2)] = 0
[goal#(x1)] = 3 + 2 · x1
[Cons(x1, x2)] = 2 + 1 · x1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)
append(Cons(z0,z1),z2) → Cons(z0,append(z1,z2)) (14)
reverse(Cons(z0,z1)) → append(reverse(z1),Cons(z0,Nil)) (11)
reverse(Nil) → Nil (5)
append(Nil,z0) → z0 (16)

1.1.1.1.1.1.1 Rule Shifting

The rules
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
append#(Nil,z0) → c5 (17)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[shuffle#(x1)] = 2 + 2 · x1 · x1
[reverse#(x1)] = 2 · x1 + 0
[append#(x1, x2)] = 1 + 1 · x2
[goal#(x1)] = 2 + 1 · x1 + 2 · x1 · x1
[Cons(x1, x2)] = 2 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)
append(Cons(z0,z1),z2) → Cons(z0,append(z1,z2)) (14)
reverse(Cons(z0,z1)) → append(reverse(z1),Cons(z0,Nil)) (11)
reverse(Nil) → Nil (5)
append(Nil,z0) → z0 (16)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1] = 0
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3] = 0
[c4(x1)] = 1 · x1 + 0
[c5] = 0
[c6(x1)] = 1 · x1 + 0
[reverse(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[shuffle#(x1)] = 1 + 1 · x1 · x1 + 1 · x1 · x1 · x1
[reverse#(x1)] = 1 + 1 · x1 · x1
[append#(x1, x2)] = 1 · x1 + 0
[goal#(x1)] = 1 + 1 · x1 · x1 + 1 · x1 · x1 · x1
[Cons(x1, x2)] = 1 + 1 · x2
[Nil] = 0
which has the intended complexity. Here, only the following usable rules have been considered:
shuffle#(Cons(z0,z1)) → c(shuffle#(reverse(z1)),reverse#(z1)) (9)
shuffle#(Nil) → c1 (10)
reverse#(Cons(z0,z1)) → c2(append#(reverse(z1),Cons(z0,Nil)),reverse#(z1)) (12)
reverse#(Nil) → c3 (13)
append#(Cons(z0,z1),z2) → c4(append#(z1,z2)) (15)
append#(Nil,z0) → c5 (17)
goal#(z0) → c6(shuffle#(z0)) (19)
append(Cons(z0,z1),z2) → Cons(z0,append(z1,z2)) (14)
reverse(Cons(z0,z1)) → append(reverse(z1),Cons(z0,Nil)) (11)
reverse(Nil) → Nil (5)
append(Nil,z0) → z0 (16)

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