X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fcomplexity.ma;h=7caf6178ee6da92886ac9a5dce8b7c16726ba323;hb=143c97a8fe657eb7b041dec2747b0e67b5899762;hp=fa9837a85b88bc9830d3ac8c67b625df3ed45162;hpb=1bb7e6b001ef3d712a9da6fbad0405b130e9f819;p=helm.git

diff --git a/matita/matita/lib/turing/complexity.ma b/matita/matita/lib/turing/complexity.ma
index fa9837a85..7caf6178e 100644
--- a/matita/matita/lib/turing/complexity.ma
+++ b/matita/matita/lib/turing/complexity.ma
@@ -11,7 +11,7 @@
 
 include "turing/turing.ma".
 
-
+(* this no longer works: TODO 
 (* time *) 
 let rec time_of sig (M:TM sig) a b (p:computation sig M a b) on p ≝
   match p with 
@@ -24,7 +24,7 @@ definition ComputeB_in_time ≝ λsig.λM:TM sig.λA:(list sig) → bool.λf.
   ∀l.∃c.∃p:computation sig M (init sig M l) c.
    time_of … p ≤ f (|l|) ∧
    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
-
+*)
 (* Le macchine di Turing sono a Type[1], che vorrebbe un nuovo 
 esistenziale.  
 
@@ -36,18 +36,18 @@ interpretation "Exists" 'exists x = (Ex ? x).
 definition DTIME ≝ λsig:FinSet. λL: list sig → bool. λf.
 ∃M:TM sig. ComputeB sig M L ∧ ∃c. Time_Bound sig M (λx.c + c*(f x)).
 *)
-
+(* this no longer works: TODO 
 inductive DTIME (sig:FinSet) (A:list sig → bool) (f:nat→nat) : Type[1] ≝ 
 | DTIME_intro: ∀M:TM sig.∀c.
     ComputeB_in_time sig M A (λx.c + c*(f x)) → DTIME sig A f.
-
+*)
 (* space complexity *) 
 
 definition size_of_tape ≝ λsig.λtp: tape sig.|left sig tp|+|right sig tp|.
 
 definition size_of_tapes ≝ λsig.λn.λtps: Vector (tape sig) n.
 foldr ?? (λtp.λacc.max (size_of_tape sig tp) acc) 0 tps.
-
+(* this no longer works: TODO 
 definition size_of_config ≝ λsig.λM.λc.
   size_of_tapes sig (S (tapes_no sig M)) (tapes sig M c).
 
@@ -62,8 +62,8 @@ definition ComputeB_in_space ≝ λsig.λM:TM sig.λA:(list sig) → bool.λf.
   ∀l.∃c.∃p:computation sig M (init sig M l) c.
    space_of … p ≤ f (|l|) ∧
    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
-   
+
 inductive DSPACE (sig:FinSet) (A:list sig → bool) (f:nat→nat) : Type[1] ≝ 
 | DTIME_intro: ∀M:TM sig.∀c.
     ComputeB_in_space sig M A (λx.c + c*(f x)) → DSPACE sig A f.
-
+*)
\ No newline at end of file