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