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