Runtime Complexity proof of /tmp/tmpywLtF3/prefix-bf.pl

Runtime Complexity of the query pattern
prefix(g,a)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^1)).

0 Prolog

↳1 LPReorderTransformerProof (⇔, 0 ms)

↳2 Prolog

↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 72 ms)

↳4 CdtProblem

    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 122 ms)

    ↳12 CdtProblem

    ↳13 SIsEmptyProof (⇔, 0 ms)

    ↳14 BOUNDS(O(1), O(1))

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 60 ms)

↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 0 ms)

    ↳22 CdtProblem

    ↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 91 ms)

    ↳24 CdtProblem

(0) Obligation:

Clauses:

prefix(Xs, Ys) :- app(Xs, X1, Ys).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: prefix(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

app([], X, X).
prefix(Xs, Ys) :- app(Xs, X1, Ys).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: prefix(g,a)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: prefix(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: prefix(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: app(T10, X13, T12)\n\nT10 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: app(T10, X13, T12), SCOPE: 2, CLAUSE: 0 | app(T10, X13, T12), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true | app([], X13, T12), SCOPE: 2, CLAUSE: 2\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: app(T10, X13, T12), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX13 is free\nX22 is free\napp(T10, X13, T12) !=? app([], X22, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: app([], X13, T12), SCOPE: 2, CLAUSE: 2\n\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(T25, X42, T27)\n\nT25 is ground\nX42 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 21 [arrowhead = none ];
21 -> 4;

22 [label="ONLY EVAL with clause\nprefix(X11, X12) :- app(X11, X13, X12).\nand substitutionT1 -> T10,\nX11 -> T10,\nT2 -> T12,\nX12 -> T12,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 22 [arrowhead = none ];
22 -> 7;

23 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 23 [arrowhead = none ];
23 -> 12;

24 [label="EVAL with clause\napp([], X22, X22).\nand substitutionT10 -> [],\nX13 -> T17,\nX22 -> T17,\nT12 -> T17,\nX23 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 24 [arrowhead = none ];
24 -> 13;

25 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 25 [arrowhead = none ];
25 -> 15;

26 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 26 [arrowhead = none ];
26 -> 16;

27 [label="EVAL with clause\napp(.(X38, X39), X40, .(X38, X41)) :- app(X39, X40, X41).\nand substitutionX38 -> T24,\nX39 -> T25,\nT10 -> .(T24, T25),\nX13 -> X42,\nX40 -> X42,\nX41 -> T27,\nT12 -> .(T24, T27),\nT26 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 27 [arrowhead = none ];
27 -> 19;

28 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 28 [arrowhead = none ];
28 -> 20;

29 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 29 [arrowhead = none ];
29 -> 17;

30 [label="INSTANCE with matching:\nT10 -> T25\nX13 -> X42\nT12 -> T27", fontsize=14, style = filled, fillcolor = lightgrey];
19 -> 30 [arrowhead = none , style=dashed];
30 -> 7[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f7_in([]) → f7_out1
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
U2(f7_out1, .(z0, z1)) → f7_out1

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))

S tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2

Defined Pair Symbols:

F1_IN, F7_IN

Compound Symbols:

c, c3

(5) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f7_in([]) → f7_out1
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
U2(f7_out1, .(z0, z1)) → f7_out1

Tuples:

F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F1_IN(z0) → c1(U1'(f7_in(z0), z0))
F1_IN(z0) → c1(F7_IN(z0))

S tuples:

F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F1_IN(z0) → c1(U1'(f7_in(z0), z0))
F1_IN(z0) → c1(F7_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2

Defined Pair Symbols:

F7_IN, F1_IN

Compound Symbols:

c3, c1

(7) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f7_in([]) → f7_out1
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
U2(f7_out1, .(z0, z1)) → f7_out1

Tuples:

F1_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F1_IN(z0) → c1

S tuples:

F1_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F1_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2

Defined Pair Symbols:

F1_IN, F7_IN

Compound Symbols:

c1, c3, c1

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(z0) → c1(F7_IN(z0))
F1_IN(z0) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f7_in([]) → f7_out1
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
U2(f7_out1, .(z0, z1)) → f7_out1

Tuples:

F1_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F1_IN(z0) → c1

S tuples:

F7_IN(.(z0, z1)) → c3(F7_IN(z1))

K tuples:

F1_IN(z0) → c1(F7_IN(z0))
F1_IN(z0) → c1

Defined Rule Symbols:

f1_in, U1, f7_in, U2

Defined Pair Symbols:

F1_IN, F7_IN

Compound Symbols:

c1, c3, c1

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F7_IN(.(z0, z1)) → c3(F7_IN(z1))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F1_IN(z0) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂
POL(F1_IN(x₁)) = [1] + x₁
POL(F7_IN(x₁)) = x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c3(x₁)) = x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1, z0) → f1_out1
f7_in([]) → f7_out1
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
U2(f7_out1, .(z0, z1)) → f7_out1

Tuples:

F1_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F1_IN(z0) → c1

S tuples:none
K tuples:

F1_IN(z0) → c1(F7_IN(z0))
F1_IN(z0) → c1
F7_IN(.(z0, z1)) → c3(F7_IN(z1))

Defined Rule Symbols:

f1_in, U1, f7_in, U2

Defined Pair Symbols:

F1_IN, F7_IN

Compound Symbols:

c1, c3, c1

(13) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(14) BOUNDS(O(1), O(1))

(15) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: prefix(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: prefix(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: app(T5, X6, T7)\n\nT5 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: app(T5, X6, T7), SCOPE: 2, CLAUSE: 0 | app(T5, X6, T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | app([], X6, T7), SCOPE: 2, CLAUSE: 2\n\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: app(T5, X6, T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground\nX6 is free\nX11 is free\napp(T5, X6, T7) !=? app([], X11, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: app([], X6, T7), SCOPE: 2, CLAUSE: 2\n\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: app(T18, X31, T20)\n\nT18 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 19 [arrowhead = none ];
19 -> 3;

20 [label="ONLY EVAL with clause\nprefix(X4, X5) :- app(X4, X6, X5).\nand substitutionT1 -> T5,\nX4 -> T5,\nT2 -> T7,\nX5 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 20 [arrowhead = none ];
20 -> 5;

21 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 21 [arrowhead = none ];
21 -> 6;

22 [label="EVAL with clause\napp([], X11, X11).\nand substitutionT5 -> [],\nX6 -> T10,\nX11 -> T10,\nT7 -> T10,\nX12 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 22 [arrowhead = none ];
22 -> 8;

23 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 23 [arrowhead = none ];
23 -> 9;

24 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 24 [arrowhead = none ];
24 -> 10;

25 [label="EVAL with clause\napp(.(X27, X28), X29, .(X27, X30)) :- app(X28, X29, X30).\nand substitutionX27 -> T17,\nX28 -> T18,\nT5 -> .(T17, T18),\nX6 -> X31,\nX29 -> X31,\nX30 -> T20,\nT7 -> .(T17, T20),\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 25 [arrowhead = none ];
25 -> 14;

26 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 26 [arrowhead = none ];
26 -> 18;

27 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 27 [arrowhead = none ];
27 -> 11;

28 [label="INSTANCE with matching:\nT5 -> T18\nX6 -> X31\nT7 -> T20", fontsize=14, style = filled, fillcolor = lightgrey];
14 -> 28 [arrowhead = none , style=dashed];
28 -> 5[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1, z0) → f2_out1
f5_in([]) → f5_out1
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
U2(f5_out1, .(z0, z1)) → f5_out1

Tuples:

F2_IN(z0) → c(U1'(f5_in(z0), z0), F5_IN(z0))
F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))

S tuples:

F2_IN(z0) → c(U1'(f5_in(z0), z0), F5_IN(z0))
F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2

Defined Pair Symbols:

F2_IN, F5_IN

Compound Symbols:

c, c3

(17) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1, z0) → f2_out1
f5_in([]) → f5_out1
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
U2(f5_out1, .(z0, z1)) → f5_out1

Tuples:

F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F2_IN(z0) → c1(U1'(f5_in(z0), z0))
F2_IN(z0) → c1(F5_IN(z0))

S tuples:

F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F2_IN(z0) → c1(U1'(f5_in(z0), z0))
F2_IN(z0) → c1(F5_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2

Defined Pair Symbols:

F5_IN, F2_IN

Compound Symbols:

c3, c1

(19) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1, z0) → f2_out1
f5_in([]) → f5_out1
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
U2(f5_out1, .(z0, z1)) → f5_out1

Tuples:

F2_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F2_IN(z0) → c1

S tuples:

F2_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F2_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f5_in, U2

Defined Pair Symbols:

F2_IN, F5_IN

Compound Symbols:

c1, c3, c1

(21) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(z0) → c1(F5_IN(z0))
F2_IN(z0) → c1

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1, z0) → f2_out1
f5_in([]) → f5_out1
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
U2(f5_out1, .(z0, z1)) → f5_out1

Tuples:

F2_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F2_IN(z0) → c1

S tuples:

F5_IN(.(z0, z1)) → c3(F5_IN(z1))

K tuples:

F2_IN(z0) → c1(F5_IN(z0))
F2_IN(z0) → c1

Defined Rule Symbols:

f2_in, U1, f5_in, U2

Defined Pair Symbols:

F2_IN, F5_IN

Compound Symbols:

c1, c3, c1

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F5_IN(.(z0, z1)) → c3(F5_IN(z1))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F2_IN(z0) → c1

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂
POL(F2_IN(x₁)) = [1] + x₁
POL(F5_IN(x₁)) = x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c3(x₁)) = x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1, z0) → f2_out1
f5_in([]) → f5_out1
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
U2(f5_out1, .(z0, z1)) → f5_out1

Tuples:

F2_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F2_IN(z0) → c1

S tuples:none
K tuples:

F2_IN(z0) → c1(F5_IN(z0))
F2_IN(z0) → c1
F5_IN(.(z0, z1)) → c3(F5_IN(z1))

Defined Rule Symbols:

f2_in, U1, f5_in, U2

Defined Pair Symbols:

F2_IN, F5_IN

Compound Symbols:

c1, c3, c1