matita/matita/lib/turing/complexity.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "turing/turing.ma".
  13
  14
  15 (* time *)
  16 let rec time_of sig (M:TM sig) a b (p:computation sig M a b) on p ≝
  17   match p with
  18    [ empty x ⇒ 0
  19    | more a c b h tl ⇒ S (time_of sig M c b tl)
  20    ]
  21 .
  22
  23 definition ComputeB_in_time ≝ λsig.λM:TM sig.λA:(list sig) → bool.λf.
  24   ∀l.∃c.∃p:computation sig M (init sig M l) c.
  25    time_of … p ≤ f (|l|) ∧
  26    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
  27
  28 (* Le macchine di Turing sono a Type[1], che vorrebbe un nuovo
  29 esistenziale.
  30
  31 inductive Ex (A:Type[1]) (P:A → Prop) : Prop ≝
  32     Ex_intro: ∀ x:A. P x →  Ex A P.
  33
  34 interpretation "Exists" 'exists x = (Ex ? x).
  35
  36 definition DTIME ≝ λsig:FinSet. λL: list sig → bool. λf.
  37 ∃M:TM sig. ComputeB sig M L ∧ ∃c. Time_Bound sig M (λx.c + c*(f x)).
  38 *)
  39
  40 inductive DTIME (sig:FinSet) (A:list sig → bool) (f:nat→nat) : Type[1] ≝
  41 | DTIME_intro: ∀M:TM sig.∀c.
  42     ComputeB_in_time sig M A (λx.c + c*(f x)) → DTIME sig A f.
  43
  44 (* space complexity *)
  45
  46 definition size_of_tape ≝ λsig.λtp: tape sig.|left sig tp|+|right sig tp|.
  47
  48 definition size_of_tapes ≝ λsig.λn.λtps: Vector (tape sig) n.
  49 foldr ?? (λtp.λacc.max (size_of_tape sig tp) acc) 0 tps.
  50
  51 definition size_of_config ≝ λsig.λM.λc.
  52   size_of_tapes sig (S (tapes_no sig M)) (tapes sig M c).
  53
  54 let rec space_of sig (M:TM sig) ci cf (p:computation sig M ci cf) on p ≝
  55   match p with
  56    [ empty a ⇒ size_of_config sig M a
  57    | more a c b h tl ⇒ max (size_of_config sig M a) (space_of sig M c b tl)
  58    ]
  59 .
  60
  61 definition ComputeB_in_space ≝ λsig.λM:TM sig.λA:(list sig) → bool.λf.
  62   ∀l.∃c.∃p:computation sig M (init sig M l) c.
  63    space_of … p ≤ f (|l|) ∧
  64    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
  65
  66 inductive DSPACE (sig:FinSet) (A:list sig → bool) (f:nat→nat) : Type[1] ≝
  67 | DTIME_intro: ∀M:TM sig.∀c.
  68     ComputeB_in_space sig M A (λx.c + c*(f x)) → DSPACE sig A f.
  69