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 lemma 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 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
  70 [normalize #a0 #Hfalse destruct
  71 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
  72  cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
  73 ]
  74 qed.
  75
  76 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
  77  ∀k1,k2,a1,a2,a3,a4.
  78    loop A k1 f p a1 = Some ? a2 →
  79      f a2 = a3 → q a2 = false →
  80        loop A k2 f q a3 = Some ? a4 →
  81          loop A (k1+k2) f q a1 = Some ? a4.
  82 #Sig #f #p #q #Hpq #k1 elim k1
  83   [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
  84   |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
  85    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
  86    [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
  87     whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
  88     whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
  89    |normalize >(Hpq … pa1) normalize
  90     #H1 #H2 #H3 @(Hind … H2) //
  91    ]
  92  ]
  93 qed.
  94
  95 (*
  96 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
  97  ∀k1,k2,a1,a2,a3.
  98    loop A k1 f p a1 = Some ? a2 →
  99      loop A k2 f q a2 = Some ? a3 →
 100        loop A (k1+k2) f q a1 = Some ? a3.
 101 #Sig #f #p #q #Hpq #k1 elim k1
 102   [normalize #k2 #a1 #a2 #a3 #H destruct
 103   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
 104    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 105    [#eqa1a2 destruct #H @loop_incr //
 106    |normalize >(Hpq … pa1) normalize
 107     #H1 #H2 @(Hind … H2) //
 108    ]
 109  ]
 110 qed.
 111 *)
 112
 113 definition initc ≝ λsig.λM:TM sig.λt.
 114   mk_config sig M (start sig M) t.
 115
 116 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 117 ∀t.∃i.∃outc.
 118   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 119   R t (ctape ?? outc).
 120
 121 (* Compositions *)
 122
 123 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 124 λp. let 〈s,a〉 ≝ p in
 125   match s with
 126   [ inl s1 ⇒
 127       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 128       else
 129       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 130       〈inl … news1,m〉
 131   | inr s2 ⇒
 132       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 133       〈inr … news2,m〉
 134   ].
 135
 136 definition seq ≝ λsig. λM1,M2 : TM sig.
 137   mk_TM sig
 138     (FinSum (states sig M1) (states sig M2))
 139     (seq_trans sig M1 M2)
 140     (inl … (start sig M1))
 141     (λs.match s with
 142       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 143
 144 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 145   ∃am.R1 a1 am ∧ R2 am a2.
 146
 147 (*
 148 definition injectRl ≝ λsig.λM1.λM2.λR.
 149    λc1,c2. ∃c11,c12.
 150      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 151      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 152      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 153      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 154      R c11 c12.
 155
 156 definition injectRr ≝ λsig.λM1.λM2.λR.
 157    λc1,c2. ∃c21,c22.
 158      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 159      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 160      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 161      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 162      R c21 c22.
 163
 164 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 165   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 166   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 167   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 168
 169 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 170
 171 definition lift_confL ≝
 172   λsig,M1,M2,c.match c with
 173   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 174 definition lift_confR ≝
 175   λsig,M1,M2,c.match c with
 176   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 177
 178 definition halt_liftL ≝
 179   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 180   match s with
 181   [ inl s1 ⇒ halt sig M1 s1
 182   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 183
 184 definition halt_liftR ≝
 185   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 186   match s with
 187   [ inl _ ⇒ false
 188   | inr s2 ⇒ halt sig M2 s2 ].
 189
 190 lemma p_halt_liftL : ∀sig,M1,M2,c.
 191   halt sig M1 (cstate … c) =
 192      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 193 #sig #M1 #M2 #c cases c #s #t %
 194 qed.
 195
 196 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 197   halt ? M1 s = false →
 198   trans sig M1 〈s,a〉 = 〈news,move〉 →
 199   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 200 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 201 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 202 qed.
 203
 204 lemma config_eq :
 205   ∀sig,M,c1,c2.
 206   cstate sig M c1 = cstate sig M c2 →
 207   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 208 #sig #M1 * #s1 #t1 * #s2 #t2 //
 209 qed.
 210
 211 lemma step_lift_confL : ∀sig,M1,M2,c0.
 212  halt ? M1 (cstate ?? c0) = false →
 213  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 214  lift_confL sig M1 M2 (step sig M1 c0).
 215 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 216 #rs #Hhalt
 217 whd in ⊢ (???(????%));whd in ⊢ (???%);
 218 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 219 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 220 #s0 #m0 #Heq whd in ⊢ (???%);
 221 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 222 >(trans_liftL … Heq)
 223 [% | //]
 224 qed.
 225
 226 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 227   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 228     loop ? k (step sig (seq sig M1 M2))
 229       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 230     Some ? (lift_confL … c2).
 231 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 232 elim k
 233 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 234 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 235  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 236  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 237  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 238    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 239    | // ]
 240  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 241    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 242     @step_lift_confL //
 243    | // ]
 244 qed.
 245
 246 STOP!
 247
 248 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
 249   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 250     loop ? k (step sig (seq sig M1 M2))
 251       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 252     Some ? (lift_confR … c2).
 253 #sig #k #M1 #M2 #c1 #c2
 254 elim k
 255 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 256 |#k0 #IH whd in ⊢ (??%? → ??%?);
 257  lapply (refl ? (halt ?? (cstate sig M2 c1)))
 258  cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
 259  [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
 260    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
 261    | (* ... *) ]
 262  | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
 263    [whd in ⊢ (??%? → ??%?); #Hc2 <IH
 264      [@eq_f (* @step_lift_confR // *)
 265      |
 266    | // ]
 267 qed. *)
 268
 269 lemma loop_Some :
 270   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 271 #A #k #f #p #a #b elim k
 272 [normalize #Hfalse destruct
 273 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
 274  [ normalize #H1 destruct
 275
 276 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 277   halt ? M1 s = true →
 278   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 279 #sig #M1 #M2 #s #a
 280 #Hhalt whd in ⊢ (??%?); >Hhalt %
 281 qed.
 282
 283 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
 284   ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
 285 #sig #M1 #M2 #outc cases outc #s #t %
 286 qed.
 287
 288 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
 289   ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
 290 #sig #M1 #M2 #outc cases outc #s #t %
 291 qed.
 292
 293 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 294   Realize sig M1 R1 → Realize sig M2 R2 →
 295     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 296 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 297 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 298 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 299 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 300 %
 301 [@(loop_split ??????????? (loop_liftL … Hloop1))
 302  [* *
 303    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 304    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 305  ||4:cases outc1 #s1 #t1 %
 306  |5:@(loop_liftR … Hloop2)
 307  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 308   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 309   >(trans_liftL_true sig M1 M2 ??)
 310   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 311     @config_eq //
 312   | @(loop_Some ?????? Hloop10) ]
 313  ]
 314 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 315   % //
 316 ]
 317 qed.
 318
 319 definition empty_tapes ≝ λsig.λn.
 320 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 321 elim n // normalize //
 322 qed.
 323
 324 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 325   mk_config ??
 326     (start sig M)
 327     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 328     [ ].
 329
 330 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 331   halt sig M (state sig M c).
 332
 333 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 334   match n with
 335   [ O ⇒ None ?
 336   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 337   ].
 338
 339 (* Compute ? M f states that f is computed by M *)
 340 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 341 ∀l.∃i.∃c.
 342   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 343   out ?? c = f l.
 344
 345 (* for decision problems, we accept a string if on termination
 346 output is not empty *)
 347
 348 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 349 ∀l.∃i.∃c.
 350   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 351   (isnilb ? (out ?? c) = false).
 352
 353 (* alternative approach.
 354 We define the notion of computation. The notion must be constructive,
 355 since we want to define functions over it, like lenght and size
 356
 357 Perche' serve Type[2] se sposto a e b a destra? *)
 358
 359 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 360   mk_move: p a = false → b = f a → cmove A f p a b.
 361
 362 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 363 | empty : ∀a. cstar A M a a
 364 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 365
 366 definition computation ≝ λsig.λM:TM sig.
 367   cstar ? (cmove ? (step sig M) (stop sig M)).
 368
 369 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 370   ∀l.∃c.computation sig M (init sig M l) c →
 371    (stop sig M c = true) ∧ out ?? c = f l.
 372
 373 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 374   ∀l.∃c.computation sig M (init sig M l) c →
 375    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).