matita/matita/lib/turing/mono.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 "basics/vectors.ma".
  13 (* include "basics/relations.ma". *)
  14
  15 record tape (sig:FinSet): Type[0] ≝
  16 { left : list sig;
  17   right: list sig
  18 }.
  19
  20 inductive move : Type[0] ≝
  21 | L : move
  22 | R : move
  23 .
  24
  25 (* We do not distinuish an input tape *)
  26
  27 record TM (sig:FinSet): Type[1] ≝
  28 { states : FinSet;
  29   trans : states × (option sig) → states × (option (sig × move));
  30   start: states;
  31   halt : states → bool
  32 }.
  33
  34 record config (sig:FinSet) (M:TM sig): Type[0] ≝
  35 { cstate : states sig M;
  36   ctape: tape sig
  37 }.
  38
  39 definition option_hd ≝ λA.λl:list A.
  40   match l with
  41   [nil ⇒ None ?
  42   |cons a _ ⇒ Some ? a
  43   ].
  44
  45 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
  46   match m with
  47   [ None ⇒ t
  48   | Some m1 ⇒
  49     match \snd m1 with
  50     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
  51     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
  52     ]
  53   ].
  54
  55 definition step ≝ λsig.λM:TM sig.λc:config sig M.
  56   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
  57   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
  58   mk_config ?? news (tape_move sig (ctape ?? c) mv).
  59
  60 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
  61   match n with
  62   [ O ⇒ None ?
  63   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
  64   ].
  65
  66 axiom loop_incr : ∀A,f,p,k1,k2,a1,a2.
  67   loop A k1 f p a1 = Some ? a2 →
  68     loop A (k2+k1) f p a1 = Some ? a2.
  69
  70 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
  71  ∀k1,k2,a1,a2,a3.
  72    loop A k1 f p a1 = Some ? a2 →
  73      loop A k2 f q a2 = Some ? a3 →
  74        loop A (k1+k2) f q a1 = Some ? a3.
  75 #Sig #f #p #q #Hpq #k1 elim k1
  76   [normalize #k2 #a1 #a2 #a3 #H destruct
  77   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
  78    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
  79    [#eqa1a2 destruct #H @loop_incr //
  80    |normalize >(Hpq … pa1) normalize
  81     #H1 #H2 @(Hind … H2) //
  82    ]
  83  ]
  84 qed.
  85
  86 definition initc ≝ λsig.λM:TM sig.λt.
  87   mk_config sig M (start sig M) t.
  88
  89 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
  90 ∀t.∃i.∃outc.
  91   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
  92   R t (ctape ?? outc).
  93
  94 (* Compositions *)
  95
  96 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
  97 λp. let 〈s,a〉 ≝ p in
  98   match s with
  99   [ inl s1 ⇒
 100       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 101       else
 102       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 103       〈inl … news1,m〉
 104   | inr s2 ⇒
 105       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 106       〈inr … news2,m〉
 107   ].
 108
 109 definition seq ≝ λsig. λM1,M2 : TM sig.
 110   mk_TM sig
 111     (FinSum (states sig M1) (states sig M2))
 112     (seq_trans sig M1 M2)
 113     (inl … (start sig M1))
 114     (λs.match s with
 115       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 116
 117 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 118   ∃am.R1 a1 am ∧ R2 am a2.
 119
 120 (*
 121 definition injectRl ≝ λsig.λM1.λM2.λR.
 122    λc1,c2. ∃c11,c12.
 123      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 124      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 125      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 126      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 127      R c11 c12.
 128
 129 definition injectRr ≝ λsig.λM1.λM2.λR.
 130    λc1,c2. ∃c21,c22.
 131      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 132      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 133      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 134      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 135      R c21 c22.
 136
 137 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 138   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 139   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 140   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 141
 142 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 143
 144 definition lift_confL ≝
 145   λsig,M1,M2,c.match c with
 146   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 147 definition lift_confR ≝
 148   λsig,M1,M2,c.match c with
 149   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 150
 151 definition halt_liftL ≝
 152   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 153   match s with
 154   [ inl s1 ⇒ halt sig M1 s1
 155   | inr _ ⇒ false ].
 156
 157 axiom loop_dec : ∀A,k1,k2,f,p,q,a1,a2,a3.
 158   loop A k1 f p a1 = Some ? a2 →
 159     loop A k2 f q a2 = Some ? a3 →
 160       loop A (k1+k2) f q a1 = Some ? a3.
 161
 162 lemma p_halt_liftL : ∀sig,M1,M2,c.
 163   halt sig M1 (cstate … c) =
 164      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 165 #sig #M1 #M2 #c cases c #s #t %
 166 qed.
 167
 168 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 169   halt ? M1 s = false →
 170   trans sig M1 〈s,a〉 = 〈news,move〉 →
 171   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 172 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 173 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 174 qed.
 175
 176 lemma config_eq :
 177   ∀sig,M,c1,c2.
 178   cstate sig M c1 = cstate sig M c2 →
 179   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 180 #sig #M1 * #s1 #t1 * #s2 #t2 //
 181 qed.
 182
 183 lemma step_lift_confL : ∀sig,M1,M2,c0.
 184  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 185  lift_confL sig M1 M2 (step sig M1 c0).
 186 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt *
 187 [ whd in ⊢ (???(????%)); whd in ⊢ (??(???%)?);
 188   whd in ⊢ (??%?); whd in ⊢ (???%);
 189   change with (mk_config ????) in ⊢ (???%);
 190
 191 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 192   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 193     loop ? k (step sig (seq sig M1 M2))
 194       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 195     Some ? (lift_confL … c2).
 196 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 197 elim k
 198 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 199 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 200  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 201  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 202  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 203    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 204    | // ]
 205  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 206    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 207    | // ]
 208
 209 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 210   Realize sig M1 R1 → Realize sig M2 R2 →
 211     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 212 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 213 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 214 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 215 @(ex_intro … (S(k1+k2))) @(ex_intro … (lift_confR … outc2))
 216 %
 217 [@(loop_dec ????????? Hloop1)
 218
 219
 220
 221
 222 definition empty_tapes ≝ λsig.λn.
 223 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 224 elim n // normalize //
 225 qed.
 226
 227 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 228   mk_config ??
 229     (start sig M)
 230     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 231     [ ].
 232
 233 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 234   halt sig M (state sig M c).
 235
 236 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 237   match n with
 238   [ O ⇒ None ?
 239   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 240   ].
 241
 242 (* Compute ? M f states that f is computed by M *)
 243 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 244 ∀l.∃i.∃c.
 245   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 246   out ?? c = f l.
 247
 248 (* for decision problems, we accept a string if on termination
 249 output is not empty *)
 250
 251 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 252 ∀l.∃i.∃c.
 253   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 254   (isnilb ? (out ?? c) = false).
 255
 256 (* alternative approach.
 257 We define the notion of computation. The notion must be constructive,
 258 since we want to define functions over it, like lenght and size
 259
 260 Perche' serve Type[2] se sposto a e b a destra? *)
 261
 262 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 263   mk_move: p a = false → b = f a → cmove A f p a b.
 264
 265 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 266 | empty : ∀a. cstar A M a a
 267 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 268
 269 definition computation ≝ λsig.λM:TM sig.
 270   cstar ? (cmove ? (step sig M) (stop sig M)).
 271
 272 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 273   ∀l.∃c.computation sig M (init sig M l) c →
 274    (stop sig M c = true) ∧ out ?? c = f l.
 275
 276 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 277   ∀l.∃c.computation sig M (init sig M l) c →
 278    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).