WORST_CASE(?,O(n^1))
* Step 1: Desugar WORST_CASE(?,O(n^1))
+ Considered Problem:
type bstring =
E | Z of bstring | O of bstring
;;
let rec flip x =
match x with
| E -> E
| Z(x') -> O(flip x')
| O(x') -> Z(flip x')
;;
+ Applied Processor:
Desugar {analysedFunction = Nothing}
+ Details:
none
* Step 2: Defunctionalization WORST_CASE(?,O(n^1))
+ Considered Problem:
[1mλx[0m : bstring.
([1mλflip[0m : bstring -> bstring. [4mflip[0m [4mx[0m)
([1mμflip[0m : bstring -> bstring.
[1mλx[0m : bstring.
[1mcase[0m [4mx[0m [1mof[0m | E -> E | Z -> [1mλx'[0m : bstring. O([4mflip[0m [4mx'[0m) | O -> [1mλx'[0m : bstring. Z([4mflip[0m [4mx'[0m)) : bstring
-> bstring
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
+ Applied Processor:
Defunctionalization
+ Details:
none
* Step 3: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_1(x0) x1 -> x1 x0
2: cond_flip_x(E()) -> E()
3: cond_flip_x(Z(x2)) -> O(flip() x2)
4: cond_flip_x(O(x2)) -> Z(flip() x2)
5: flip_1() x1 -> cond_flip_x(x1)
6: flip() x0 -> flip_1() x0
7: main(x0) -> main_1(x0) flip()
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip_1 :: bstring -> bstring
main_1 :: bstring -> (bstring -> bstring) -> bstring
cond_flip_x :: bstring -> bstring
flip :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 4: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_1(x0) x1 -> x1 x0
2: cond_flip_x(E()) -> E()
3: cond_flip_x(Z(x2)) -> O(flip() x2)
4: cond_flip_x(O(x2)) -> Z(flip() x2)
5: flip_1() x1 -> cond_flip_x(x1)
6: flip() x2 -> cond_flip_x(x2)
7: main(x0) -> flip() x0
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip_1 :: bstring -> bstring
main_1 :: bstring -> (bstring -> bstring) -> bstring
cond_flip_x :: bstring -> bstring
flip :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
+ Details:
none
* Step 5: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_1(x0) x1 -> x1 x0
2: cond_flip_x(E()) -> E()
3: cond_flip_x(Z(x2)) -> O(flip() x2)
4: cond_flip_x(O(x2)) -> Z(flip() x2)
5: flip_1() E() -> E()
6: flip_1() Z(x4) -> O(flip() x4)
7: flip_1() O(x4) -> Z(flip() x4)
8: flip() E() -> E()
9: flip() Z(x4) -> O(flip() x4)
10: flip() O(x4) -> Z(flip() x4)
11: main(x0) -> flip() x0
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip_1 :: bstring -> bstring
main_1 :: bstring -> (bstring -> bstring) -> bstring
cond_flip_x :: bstring -> bstring
flip :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 6: UncurryATRS WORST_CASE(?,O(n^1))
+ Considered Problem:
8: flip() E() -> E()
9: flip() Z(x4) -> O(flip() x4)
10: flip() O(x4) -> Z(flip() x4)
11: main(x0) -> flip() x0
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
UncurryATRS
+ Details:
none
* Step 7: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: flip#1(E()) -> E()
2: flip#1(Z(x4)) -> O(flip#1(x4))
3: flip#1(O(x4)) -> Z(flip#1(x4))
4: main(x0) -> flip#1(x0)
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip#1 :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
UsableRules {urType = DFA}
+ Details:
none
* Step 8: Compression WORST_CASE(?,O(n^1))
+ Considered Problem:
1: flip#1(E()) -> E()
2: flip#1(Z(x4)) -> O(flip#1(x4))
3: flip#1(O(x4)) -> Z(flip#1(x4))
4: main(x0) -> flip#1(x0)
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip#1 :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
Compression
+ Details:
none
* Step 9: ToTctProblem WORST_CASE(?,O(n^1))
+ Considered Problem:
1: flip#1(E()) -> E()
2: flip#1(Z(x4)) -> O(flip#1(x4))
3: flip#1(O(x4)) -> Z(flip#1(x4))
4: main(x0) -> flip#1(x0)
where
E :: bstring
O :: bstring -> bstring
Z :: bstring -> bstring
flip#1 :: bstring -> bstring
main :: bstring -> bstring
+ Applied Processor:
ToTctProblem
+ Details:
none
* Step 10: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
flip#1(E()) -> E()
flip#1(O(x4)) -> Z(flip#1(x4))
flip#1(Z(x4)) -> O(flip#1(x4))
main(x0) -> flip#1(x0)
- Signature:
{flip#1/1,main/1} / {E/0,O/1,Z/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main} and constructors {E,O,Z}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(O) = {1},
uargs(Z) = {1}
Following symbols are considered usable:
{flip#1,main}
TcT has computed the following interpretation:
p(E) = 2
p(O) = 2 + x1
p(Z) = 2 + x1
p(flip#1) = 4*x1
p(main) = 3 + 8*x1
Following rules are strictly oriented:
flip#1(E()) = 8
> 2
= E()
flip#1(O(x4)) = 8 + 4*x4
> 2 + 4*x4
= Z(flip#1(x4))
flip#1(Z(x4)) = 8 + 4*x4
> 2 + 4*x4
= O(flip#1(x4))
main(x0) = 3 + 8*x0
> 4*x0
= flip#1(x0)
Following rules are (at-least) weakly oriented:
* Step 11: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
flip#1(E()) -> E()
flip#1(O(x4)) -> Z(flip#1(x4))
flip#1(Z(x4)) -> O(flip#1(x4))
main(x0) -> flip#1(x0)
- Signature:
{flip#1/1,main/1} / {E/0,O/1,Z/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main} and constructors {E,O,Z}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))