From 1bb7e6b001ef3d712a9da6fbad0405b130e9f819 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 13 Apr 2012 10:24:39 +0000
Subject: [PATCH] Definition of complexity

---
 matita/matita/lib/turing/complexity.ma | 69 ++++++++++++++++++++++++++
 matita/matita/lib/turing/turing.ma     | 24 +++++++++
 2 files changed, 93 insertions(+)
 create mode 100644 matita/matita/lib/turing/complexity.ma

diff --git a/matita/matita/lib/turing/complexity.ma b/matita/matita/lib/turing/complexity.ma
new file mode 100644
index 000000000..fa9837a85
--- /dev/null
+++ b/matita/matita/lib/turing/complexity.ma
@@ -0,0 +1,69 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic   
+    ||A||  Library of Mathematics, developed at the Computer Science 
+    ||T||  Department of the University of Bologna, Italy.           
+    ||I||                                                            
+    ||T||  
+    ||A||  
+    \   /  This file is distributed under the terms of the       
+     \ /   GNU General Public License Version 2   
+      V_____________________________________________________________*)
+
+include "turing/turing.ma".
+
+
+(* time *) 
+let rec time_of sig (M:TM sig) a b (p:computation sig M a b) on p ≝
+  match p with 
+   [ empty x ⇒ 0
+   | more a c b h tl ⇒ S (time_of sig M c b tl)
+   ]
+.
+
+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.  
+
+inductive Ex (A:Type[1]) (P:A → Prop) : Prop ≝
+    Ex_intro: ∀ x:A. P x →  Ex A P.
+    
+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)).
+*)
+
+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.
+
+definition size_of_config ≝ λsig.λM.λc.
+  size_of_tapes sig (S (tapes_no sig M)) (tapes sig M c).
+
+let rec space_of sig (M:TM sig) ci cf (p:computation sig M ci cf) on p ≝
+  match p with 
+   [ empty a ⇒ size_of_config sig M a
+   | more a c b h tl ⇒ max (size_of_config sig M a) (space_of sig M c b tl)
+   ]
+.
+
+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.
+
diff --git a/matita/matita/lib/turing/turing.ma b/matita/matita/lib/turing/turing.ma
index 946999784..238924785 100644
--- a/matita/matita/lib/turing/turing.ma
+++ b/matita/matita/lib/turing/turing.ma
@@ -101,3 +101,27 @@ definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 ∀l.∃i.∃c.
   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
   (isnilb ? (out ?? c) = false).
+
+(* alternative approach.
+We define the notion of computation. The notion must be constructive,
+since we want to define functions over it, like lenght and size 
+
+Perche' serve Type[2] se sposto a e b a destra? *)
+
+inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
+  mk_move: p a = false → b = f a → cmove A f p a b.
+  
+inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
+| empty : ∀a. cstar A M a a
+| more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
+
+definition computation ≝ λsig.λM:TM sig.
+  cstar ? (cmove ? (step sig M) (stop sig M)).
+
+definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
+  ∀l.∃c.computation sig M (init sig M l) c → 
+   (stop sig M c = true) ∧ out ?? c = f l.
+
+definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
+  ∀l.∃c.computation sig M (init sig M l) c → 
+   (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
-- 
2.39.2