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