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