]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/complexity.ma
Progress
[helm.git] / 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