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