matita/matita/lib/turing/multi_universal/universal.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/simple_machines.ma".
  13 include "turing/multi_universal/unistep.ma".
  14
  15 definition stop ≝ λc.
  16   match c with [ bit b ⇒ notb b | _ ⇒ true].
  17
  18 definition uni_body ≝
  19   ifTM ?? (mtestR ? cfg 2 stop)
  20     (single_finalTM ?? unistep)
  21     (nop …) (mtestR_acc ? cfg 2 stop).
  22
  23 definition acc_body : states ?? uni_body ≝ (inr … (inl … (inr … start_nop))).
  24
  25 definition ub_R_true ≝ λM,t1,t2.
  26   ∀c: nconfig (no_states M).
  27   t1=low_tapes M c→
  28     t2=low_tapes M (step FinBool M c) ∧ halt ? M (cstate … c) = false.
  29
  30 definition ub_R_false ≝ λM,t1,t2.
  31   ∀c: nconfig (no_states M).
  32   t1 = low_tapes M c → t1 = t2 ∧ halt ? M (cstate … c) = true.
  33
  34 lemma sem_uni_body: ∀M.
  35   uni_body ⊨ [acc_body: ub_R_true M, ub_R_false M].
  36 #M #cf
  37 @(acc_sem_if_app ????????????
  38    (sem_mtestR ? cfg 2 stop (le_S ?? (le_n 1)))
  39    (sem_unistep M)
  40    (sem_nop …))
  41 [#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Ht2 * #q #Mt #Ht1
  42  >Ht1 in Htest; >cfg_low_tapes whd in match (bits_of_state ???);
  43  #Htest lapply (Htest … (refl ??)) * <Ht1 #Ht3 #Hstop >Ht3 in Ht2;
  44  #Ht2 % [@Ht2 //] lapply Hstop  whd in match (nhalt ??);
  45  cases (nhalt M q) whd in match (stop ?); * /2/
  46 |#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Hnop >Hnop -Hnop * #q #Mt #Ht1 >Ht1 in Htest;
  47  >cfg_low_tapes whd in match (bits_of_state ???);
  48  #Htest lapply (Htest … (refl ??)) whd in match (nhalt ??);
  49  cases (nhalt M q) whd in match (stop ?); * /2/
  50 ]
  51 qed.
  52
  53 definition universalTM ≝ whileTM ?? uni_body acc_body.
  54
  55 definition low_R ≝ λM,q,R.λt1,t2:Vector (tape FSUnialpha) 3.
  56     ∀Mt. t1 = low_tapes M (mk_config ?? q Mt) →
  57     ∃cout. R Mt (ctape … cout) ∧
  58     halt ? M (cstate … cout) = true ∧ t2 = low_tapes M cout.
  59
  60 theorem sem_universal: ∀M:normalTM. ∀q.
  61   universalTM ⊫ low_R M q (R_TM FinBool M q).
  62 #M #q #intape #i #outc #Hloop
  63 lapply (sem_while … (sem_uni_body M … ) intape i outc Hloop) [%] -Hloop
  64 * #ta * #Hstar lapply q -q @(star_ind_l ??????? Hstar) -Hstar
  65   [#q whd in ⊢ (%→?); #HFalse whd #Mt #Hta
  66    lapply (HFalse … Hta) * #Hta1 #Hhalt %{(mk_config ?? q Mt)} %
  67     [%[%{1} %{(mk_config ?? q Mt)} % // whd in ⊢ (??%?); >Hhalt % |@Hhalt]
  68     |<Hta1 @Hta
  69     ]
  70   |#t1 #t2 whd in ⊢ (%→?); #Hstep #Hstar #IH #q #Hta whd #Mt #Ht1
  71    lapply (Hstep … Ht1) * -Hstep #Ht2 #Hhalt
  72    lapply(IH (cstate … (step FinBool M (mk_config ?? q Mt))) Hta ??) [@Ht2|skip] -IH
  73    * #cout * * #HRTM #Hhalt1 #Houtc
  74    %{cout}
  75    %[%[cases HRTM #k * #outc1 * <config_expand #Hloop #Houtc1
  76        %{(S k)} %{outc1} %
  77         [whd in ⊢ (??%?); >Hhalt whd in ⊢ (??%?); @Hloop
  78         |@Houtc1
  79         ]
  80       |@Hhalt1]
  81     |@Houtc
  82     ]
  83   ]
  84 qed.
  85
  86 theorem sem_universal2: ∀M:normalTM. ∀R.
  87   M ⊫ R → universalTM ⊫ (low_R M (start ? M) R).
  88 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
  89 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
  90 #c * * #HRTM #Hhalt #Ht2 %{c}
  91 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
  92 qed.
  93
  94 (* termination *)
  95
  96
  97 lemma halting_case: ∀M:normalTM.∀t,q. halt ? M q = true →
  98   universalTM↓low_tapes M (mk_config ?? q t).
  99 #M #t #q #Hhalt
 100 @(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%]
 101 % #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhalt
 102 #Habs destruct (Habs)
 103 qed.
 104
 105 theorem terminate_UTM: ∀M:normalTM.∀t.
 106   M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)).
 107 #M #t #H @(terminate_while ?? uni_body ????? (sem_uni_body … M)) [%]
 108 lapply H -H * #x (* we need to generalize to an arbitrary initial configuration *)
 109 whd in match (initc ? M t); generalize in match (start ? M); lapply t -t
 110 elim x
 111   [#t #q * #outc whd in ⊢ (??%?→?); #Habs destruct
 112   |#n #Hind #t #q cases (true_or_false (halt ? M q)) #Hhaltq
 113     [* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #HSome destruct (HSome)
 114      % #ta whd in ⊢ (%→?); #H cases (H … (refl ??)) #_ >Hhaltq
 115      #Habs destruct (Habs)
 116   |* #outc whd in ⊢ (??%?→?); >Hhaltq whd in ⊢ (??%?→?); #Hloop
 117    % #t1 whd in ⊢ (%→?); #Hstep lapply (Hstep … (refl ??)) *
 118    #Ht1 #_ >Ht1 @Hind %{outc} <config_expand @Hloop
 119   ]
 120 qed.
 121