WORST_CASE(?,O(n^3)) * Step 1: Desugar WORST_CASE(?,O(n^3)) + Considered Problem: type bool = True | False ;; type 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type Unit = Unit ;; let ifz n th el = match n with | 0 -> th 0 | S(x) -> el x ;; let ite b th el = match b with | True()-> th | False()-> el ;; let minus n m = let rec minus' m n = match m with | 0 -> 0 | S(x) -> match n with | 0 -> m | S(y) -> minus' x y in Pair(minus' n m,m) ;; let rec plus n m = match m with | 0 -> n | S(x) -> S(plus n x) ;; type ('a,'b,'c) triple = Triple of 'a * 'b * 'c ;; let rec div_mod n m = match (minus n m) with | Pair(res,m) -> match res with | 0 -> Triple (0,n,m) | S(x) -> match (div_mod res m) with | Triple(a,rest,unusedM) -> Triple(plus S(0) a,rest,m) ;; type ('a,'b) pair = Pair of 'a * 'b (* * * * * * * * * * * * Resource Aware ML * * * * * * * * * * * * * * * * Use Cases * * * * File: * example/calculator.raml * * Author: * Jan Hoffmann (S(S(0))015) * * Description: * An evaluator for simple arithmetic expressions. * *) ;; type nat = Zero | Succ of nat ;; type expr = Nat of nat | Add of expr * expr | Sub of expr * expr ;; let rec add n1 n2 = match n1 with | Zero()-> n2 | Succ(n) -> Succ(add n n2) ;; let rec sub n1 n2 = match n2 with | Zero()-> n1 | Succ(n2') -> match n1 with | Zero()-> Zero | Succ(n1') -> sub n1' n2' ;; let rec mult n1 n2 = match n1 with | Zero()-> Zero | Succ(n) -> add n (mult n n2) ;; let rec eval expr = match expr with | Nat(n) -> n | Add(e1,e2) -> (let n1 = eval e1 in match n1 with | Zero()-> eval e2 | Succ(n) -> Succ(eval (Add (Nat(n), e2)) )) | Sub(e1,e2) -> let n2 = eval e2 in match n2 with | Zero()-> eval e1 | Succ(m) -> let n1 = eval e1 in match n1 with | Zero()-> Zero | Succ(n) -> eval (Sub (Nat(n), Nat(m))) ;; (* let rec nat_to_int n = * match n with * | Zero()-> Zero * | Succ(n) -> * let i = nat_to_int n in * plus i Succ(Zero) * * ;; * let main = * let one = Nat (Succ(Zero)) in * let two1 = Nat (Succ (Succ (Zero))) in * let two2 = Nat (Succ (Succ (Zero))) in * let two3 = Nat (Succ (Succ (Zero))) in * let two4 = Nat (Succ (Succ (Zero))) in * let n = eval (Sub ((Add (Add (two1,two2), Add (two3, one))), two4)) in * nat_to_int n * ;; *) + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^3)) + Considered Problem: λexpr : expr. (λeval : expr -> nat. eval expr) (μeval : expr -> nat. λexpr : expr. case expr of | Nat -> λn : nat. n | Add -> λe1 : expr. λe2 : expr. (λn1 : nat. case n1 of | Zero -> eval e2 | Succ -> λn : nat. Succ(eval Add(Nat(n),e2))) (eval e1) | Sub -> λe1 : expr. λe2 : expr. (λn2 : nat. case n2 of | Zero -> eval e1 | Succ -> λm : nat. (λn1 : nat. case n1 of | Zero -> Zero | Succ -> λn : nat. eval Sub(Nat(n),Nat(m))) (eval e1)) (eval e2)) : expr -> nat where Add :: expr -> expr -> expr Cons :: 'a -> 'a list -> 'a list False :: bool Nat :: nat -> expr Nil :: 'a list None :: 'a option Pair :: 'a -> 'b -> ('a,'b) pair Some :: 'a -> 'a option Sub :: expr -> expr -> expr Succ :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit Zero :: nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x3) x4 -> cond_eval_expr_1(x4, x3) 5: cond_eval_expr_3(Zero(), x5) -> Zero() 6: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 7: eval_expr_9(x5) x6 -> cond_eval_expr_3(x6, x5) 8: cond_eval_expr_2(Zero(), x2) -> eval() x2 9: cond_eval_expr_2(Succ(x5), x2) -> eval_expr_9(x5) (eval() x2) 10: eval_expr_7(x2) x4 -> cond_eval_expr_2(x4, x2) 11: cond_eval_expr(Nat(x2)) -> x2 12: cond_eval_expr(Add(x2, x3)) -> eval_expr_3(x3) (eval() x2) 13: cond_eval_expr(Sub(x2, x3)) -> eval_expr_7(x2) (eval() x3) 14: eval_1() x1 -> cond_eval_expr(x1) 15: eval() x0 -> eval_1() x0 16: main(x0) -> main_1(x0) eval() where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x3) x4 -> cond_eval_expr_1(x4, x3) 5: cond_eval_expr_3(Zero(), x5) -> Zero() 6: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 7: eval_expr_9(x5) x6 -> cond_eval_expr_3(x6, x5) 8: cond_eval_expr_2(Zero(), x2) -> eval() x2 9: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 10: eval_expr_7(x2) x4 -> cond_eval_expr_2(x4, x2) 11: cond_eval_expr(Nat(x2)) -> x2 12: cond_eval_expr(Add(x5, x6)) -> cond_eval_expr_1(eval() x5, x6) 13: cond_eval_expr(Sub(x4, x7)) -> cond_eval_expr_2(eval() x7, x4) 14: eval_1() x1 -> cond_eval_expr(x1) 15: eval() x2 -> cond_eval_expr(x2) 16: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 5: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_1(x0) x1 -> x1 x0 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 4: eval_expr_3(x6) Zero() -> eval() x6 5: eval_expr_3(x6) Succ(x10) -> Succ(eval() Add(Nat(x10), x6)) 6: cond_eval_expr_3(Zero(), x5) -> Zero() 7: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 8: eval_expr_9(x10) Zero() -> Zero() 9: eval_expr_9(x10) Succ(x14) -> eval() Sub(Nat(x14), Nat(x10)) 10: cond_eval_expr_2(Zero(), x2) -> eval() x2 11: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 12: eval_expr_7(x4) Zero() -> eval() x4 13: eval_expr_7(x10) Succ(x20) -> cond_eval_expr_3(eval() x10, x20) 14: cond_eval_expr(Nat(x2)) -> x2 15: cond_eval_expr(Add(x5, x6)) -> cond_eval_expr_1(eval() x5, x6) 16: cond_eval_expr(Sub(x4, x7)) -> cond_eval_expr_2(eval() x7, x4) 17: eval_1() Nat(x4) -> x4 18: eval_1() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 19: eval_1() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 20: eval() Nat(x4) -> x4 21: eval() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 22: eval() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 23: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat eval_1 :: expr -> nat main_1 :: expr -> (expr -> nat) -> nat eval_expr_3 :: expr -> nat -> nat eval_expr_7 :: expr -> nat -> nat eval_expr_9 :: nat -> nat -> nat cond_eval_expr :: expr -> nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 6: UncurryATRS WORST_CASE(?,O(n^3)) + Considered Problem: 2: cond_eval_expr_1(Zero(), x3) -> eval() x3 3: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval() Add(Nat(x5), x3)) 6: cond_eval_expr_3(Zero(), x5) -> Zero() 7: cond_eval_expr_3(Succ(x7), x5) -> eval() Sub(Nat(x7), Nat(x5)) 10: cond_eval_expr_2(Zero(), x2) -> eval() x2 11: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval() x5, x10) 20: eval() Nat(x4) -> x4 21: eval() Add(x10, x12) -> cond_eval_expr_1(eval() x10, x12) 22: eval() Sub(x8, x14) -> cond_eval_expr_2(eval() x14, x8) 23: main(x0) -> eval() x0 where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval :: expr -> nat main :: expr -> nat + Applied Processor: UncurryATRS + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 8: Compression WORST_CASE(?,O(n^3)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: Compression + Details: none * Step 9: ToTctProblem WORST_CASE(?,O(n^3)) + Considered Problem: 1: cond_eval_expr_1(Zero(), x3) -> eval#1(x3) 2: cond_eval_expr_1(Succ(x5), x3) -> Succ(eval#1(Add(Nat(x5), x3))) 3: cond_eval_expr_3(Zero(), x5) -> Zero() 4: cond_eval_expr_3(Succ(x7), x5) -> eval#1(Sub(Nat(x7), Nat(x5))) 5: cond_eval_expr_2(Zero(), x2) -> eval#1(x2) 6: cond_eval_expr_2(Succ(x10), x5) -> cond_eval_expr_3(eval#1(x5), x10) 7: eval#1(Nat(x4)) -> x4 8: eval#1(Add(x10, x12)) -> cond_eval_expr_1(eval#1(x10), x12) 9: eval#1(Sub(x8, x14)) -> cond_eval_expr_2(eval#1(x14), x8) 10: main(x0) -> eval#1(x0) where Add :: expr -> expr -> expr Nat :: nat -> expr Sub :: expr -> expr -> expr Succ :: nat -> nat Zero :: nat cond_eval_expr_1 :: nat -> expr -> nat cond_eval_expr_2 :: nat -> expr -> nat cond_eval_expr_3 :: nat -> nat -> nat eval#1 :: expr -> nat main :: expr -> nat + Applied Processor: ToTctProblem + Details: none * Step 10: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Succ) = {1}, uargs(cond_eval_expr_1) = {1}, uargs(cond_eval_expr_2) = {1}, uargs(cond_eval_expr_3) = {1} Following symbols are considered usable: {cond_eval_expr_1,cond_eval_expr_2,cond_eval_expr_3,eval#1,main} TcT has computed the following interpretation: p(Add) = [1] x1 + [1] x2 + [0] p(Nat) = [1] x1 + [0] p(Sub) = [1] x1 + [1] x2 + [8] p(Succ) = [1] x1 + [4] p(Zero) = [1] p(cond_eval_expr_1) = [1] x1 + [1] x2 + [0] p(cond_eval_expr_2) = [1] x1 + [1] x2 + [8] p(cond_eval_expr_3) = [1] x1 + [1] x2 + [4] p(eval#1) = [1] x1 + [0] p(main) = [1] x1 + [10] Following rules are strictly oriented: cond_eval_expr_1(Zero(),x3) = [1] x3 + [1] > [1] x3 + [0] = eval#1(x3) cond_eval_expr_2(Succ(x10),x5) = [1] x10 + [1] x5 + [12] > [1] x10 + [1] x5 + [4] = cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) = [1] x2 + [9] > [1] x2 + [0] = eval#1(x2) cond_eval_expr_3(Zero(),x5) = [1] x5 + [5] > [1] = Zero() main(x0) = [1] x0 + [10] > [1] x0 + [0] = eval#1(x0) Following rules are (at-least) weakly oriented: cond_eval_expr_1(Succ(x5),x3) = [1] x3 + [1] x5 + [4] >= [1] x3 + [1] x5 + [4] = Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_3(Succ(x7),x5) = [1] x5 + [1] x7 + [8] >= [1] x5 + [1] x7 + [8] = eval#1(Sub(Nat(x7),Nat(x5))) eval#1(Add(x10,x12)) = [1] x10 + [1] x12 + [0] >= [1] x10 + [1] x12 + [0] = cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) = [1] x4 + [0] >= [1] x4 + [0] = x4 eval#1(Sub(x8,x14)) = [1] x14 + [1] x8 + [8] >= [1] x14 + [1] x8 + [8] = cond_eval_expr_2(eval#1(x14),x8) * Step 11: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) - Weak TRS: cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Zero(),x5) -> Zero() main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Succ) = {1}, uargs(cond_eval_expr_1) = {1}, uargs(cond_eval_expr_2) = {1}, uargs(cond_eval_expr_3) = {1} Following symbols are considered usable: {cond_eval_expr_1,cond_eval_expr_2,cond_eval_expr_3,eval#1,main} TcT has computed the following interpretation: p(Add) = [1] x1 + [1] x2 + [11] p(Nat) = [1] x1 + [0] p(Sub) = [1] x1 + [1] x2 + [7] p(Succ) = [1] x1 + [14] p(Zero) = [0] p(cond_eval_expr_1) = [1] x1 + [1] x2 + [11] p(cond_eval_expr_2) = [1] x1 + [1] x2 + [0] p(cond_eval_expr_3) = [1] x1 + [1] x2 + [14] p(eval#1) = [1] x1 + [0] p(main) = [1] x1 + [1] Following rules are strictly oriented: cond_eval_expr_3(Succ(x7),x5) = [1] x5 + [1] x7 + [28] > [1] x5 + [1] x7 + [7] = eval#1(Sub(Nat(x7),Nat(x5))) eval#1(Sub(x8,x14)) = [1] x14 + [1] x8 + [7] > [1] x14 + [1] x8 + [0] = cond_eval_expr_2(eval#1(x14),x8) Following rules are (at-least) weakly oriented: cond_eval_expr_1(Succ(x5),x3) = [1] x3 + [1] x5 + [25] >= [1] x3 + [1] x5 + [25] = Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) = [1] x3 + [11] >= [1] x3 + [0] = eval#1(x3) cond_eval_expr_2(Succ(x10),x5) = [1] x10 + [1] x5 + [14] >= [1] x10 + [1] x5 + [14] = cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) = [1] x2 + [0] >= [1] x2 + [0] = eval#1(x2) cond_eval_expr_3(Zero(),x5) = [1] x5 + [14] >= [0] = Zero() eval#1(Add(x10,x12)) = [1] x10 + [1] x12 + [11] >= [1] x10 + [1] x12 + [11] = cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) = [1] x4 + [0] >= [1] x4 + [0] = x4 main(x0) = [1] x0 + [1] >= [1] x0 + [0] = eval#1(x0) * Step 12: NaturalMI WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 - Weak TRS: cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(Succ) = {1}, uargs(cond_eval_expr_1) = {1}, uargs(cond_eval_expr_2) = {1}, uargs(cond_eval_expr_3) = {1} Following symbols are considered usable: {cond_eval_expr_1,cond_eval_expr_2,cond_eval_expr_3,eval#1,main} TcT has computed the following interpretation: p(Add) = [1 3 2] [1 0 0] [2] [0 1 0] x1 + [0 1 0] x2 + [0] [0 0 1] [0 0 1] [2] p(Nat) = [1 0 0] [2] [0 1 0] x1 + [0] [0 0 1] [0] p(Sub) = [1 1 1] [1 2 0] [1] [0 1 0] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 0] [2] p(Succ) = [1 0 0] [0] [0 1 0] x1 + [1] [0 0 1] [2] p(Zero) = [0] [0] [0] p(cond_eval_expr_1) = [1 3 2] [1 0 0] [0] [0 1 0] x1 + [0 1 0] x2 + [0] [0 0 1] [0 0 1] [2] p(cond_eval_expr_2) = [1 2 0] [1 1 1] [1] [0 0 0] x1 + [0 1 0] x2 + [0] [0 0 0] [0 0 1] [2] p(cond_eval_expr_3) = [1 1 1] [1 2 0] [3] [0 1 0] x1 + [0 0 0] x2 + [0] [0 0 1] [0 0 0] [2] p(eval#1) = [1 0 0] [0] [0 1 0] x1 + [0] [0 0 1] [0] p(main) = [1 2 0] [2] [0 2 2] x1 + [1] [0 2 2] [0] Following rules are strictly oriented: cond_eval_expr_1(Succ(x5),x3) = [1 0 0] [1 3 2] [7] [0 1 0] x3 + [0 1 0] x5 + [1] [0 0 1] [0 0 1] [4] > [1 0 0] [1 3 2] [4] [0 1 0] x3 + [0 1 0] x5 + [1] [0 0 1] [0 0 1] [4] = Succ(eval#1(Add(Nat(x5),x3))) eval#1(Add(x10,x12)) = [1 3 2] [1 0 0] [2] [0 1 0] x10 + [0 1 0] x12 + [0] [0 0 1] [0 0 1] [2] > [1 3 2] [1 0 0] [0] [0 1 0] x10 + [0 1 0] x12 + [0] [0 0 1] [0 0 1] [2] = cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) = [1 0 0] [2] [0 1 0] x4 + [0] [0 0 1] [0] > [1 0 0] [0] [0 1 0] x4 + [0] [0 0 1] [0] = x4 Following rules are (at-least) weakly oriented: cond_eval_expr_1(Zero(),x3) = [1 0 0] [0] [0 1 0] x3 + [0] [0 0 1] [2] >= [1 0 0] [0] [0 1 0] x3 + [0] [0 0 1] [0] = eval#1(x3) cond_eval_expr_2(Succ(x10),x5) = [1 2 0] [1 1 1] [3] [0 0 0] x10 + [0 1 0] x5 + [0] [0 0 0] [0 0 1] [2] >= [1 2 0] [1 1 1] [3] [0 0 0] x10 + [0 1 0] x5 + [0] [0 0 0] [0 0 1] [2] = cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) = [1 1 1] [1] [0 1 0] x2 + [0] [0 0 1] [2] >= [1 0 0] [0] [0 1 0] x2 + [0] [0 0 1] [0] = eval#1(x2) cond_eval_expr_3(Succ(x7),x5) = [1 2 0] [1 1 1] [6] [0 0 0] x5 + [0 1 0] x7 + [1] [0 0 0] [0 0 1] [4] >= [1 2 0] [1 1 1] [5] [0 0 0] x5 + [0 1 0] x7 + [0] [0 0 0] [0 0 1] [2] = eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) = [1 2 0] [3] [0 0 0] x5 + [0] [0 0 0] [2] >= [0] [0] [0] = Zero() eval#1(Sub(x8,x14)) = [1 2 0] [1 1 1] [1] [0 0 0] x14 + [0 1 0] x8 + [0] [0 0 0] [0 0 1] [2] >= [1 2 0] [1 1 1] [1] [0 0 0] x14 + [0 1 0] x8 + [0] [0 0 0] [0 0 1] [2] = cond_eval_expr_2(eval#1(x14),x8) main(x0) = [1 2 0] [2] [0 2 2] x0 + [1] [0 2 2] [0] >= [1 0 0] [0] [0 1 0] x0 + [0] [0 0 1] [0] = eval#1(x0) * Step 13: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: cond_eval_expr_1(Succ(x5),x3) -> Succ(eval#1(Add(Nat(x5),x3))) cond_eval_expr_1(Zero(),x3) -> eval#1(x3) cond_eval_expr_2(Succ(x10),x5) -> cond_eval_expr_3(eval#1(x5),x10) cond_eval_expr_2(Zero(),x2) -> eval#1(x2) cond_eval_expr_3(Succ(x7),x5) -> eval#1(Sub(Nat(x7),Nat(x5))) cond_eval_expr_3(Zero(),x5) -> Zero() eval#1(Add(x10,x12)) -> cond_eval_expr_1(eval#1(x10),x12) eval#1(Nat(x4)) -> x4 eval#1(Sub(x8,x14)) -> cond_eval_expr_2(eval#1(x14),x8) main(x0) -> eval#1(x0) - Signature: {cond_eval_expr_1/2,cond_eval_expr_2/2,cond_eval_expr_3/2,eval#1/1,main/1} / {Add/2,Nat/1,Sub/2,Succ/1 ,Zero/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Add,Nat,Sub,Succ,Zero} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))