From: Andrea Asperti Date: Tue, 29 May 2012 14:01:20 +0000 (+0000) Subject: The universal machine!!! X-Git-Tag: make_still_working~1679 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=05458990020a373abef8df4590d131c96824eac7;p=helm.git The universal machine!!! --- diff --git a/matita/matita/lib/turing/universal/universal.ma b/matita/matita/lib/turing/universal/universal.ma index 1ef5b07ef..d35283a6f 100644 --- a/matita/matita/lib/turing/universal/universal.ma +++ b/matita/matita/lib/turing/universal/universal.ma @@ -10,38 +10,135 @@ V_____________________________________________________________*) -(* COMPARE BIT +include "turing/universal/trans_to_tuples.ma". -*) +(* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *) -include "turing/universal/copy.ma". +record normalTM : Type[0] ≝ +{ no_states : nat; + pos_no_states : (0 < no_states); + ntrans : trans_source no_states → trans_target no_states; + nhalt : initN no_states → bool +}. -(* -moves: -0_ = N -10 = L -11 = R -*) +definition normalTM_to_TM ≝ λM:normalTM. + mk_TM FinBool (initN (no_states M)) + (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M). + +coercion normalTM_to_TM. + +definition nconfig ≝ λn. config FinBool (initN n). + +(* +definition normalTM ≝ λn,t,h. + λk:0Htb1 @ex_intro + [|%{tape1} % + [ % + [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1)) + % [|%] whd in ⊢ (??%?); >Hhalt % + | @Hhalt ] + | % ] + ] + |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH + #q #Htd #tape1 #Htb + lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH + #IH cases (Htc … Htb); -Htc #Hhaltq + whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???)) + #Htc change with (mk_config ????) in Htc:(???(??%)); + cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc + @(ex_intro … q1) @(ex_intro … tape2) % + [% + [cases HRTM #k * #outc1 * #Hloop #Houtc1 + @(ex_intro … (S k)) @(ex_intro … outc1) % + [>loop_S_false [2://] whd in match (step ???); + >(eq_pair_fst_snd ?? (trans ???)) @Hloop + |@Houtc1 + ] + |@Hhaltq1] + |@Houtc + ] + ] +qed. + +lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2. + WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2. +#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc * +#Hloop #Ht2 >Ht2 @(HMR … Hloop) +qed. + +axiom WRealize_to_WRealize: ∀sig,M,R1,R2. + (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2. -step : - -if is_true(current) (* current state is final *) - then nop - else - match_tuple; - if is_marked(current) = false (* match *) - then adv_mark_r; - move_l; - init_current; - move_r; - adv_to_mark_r; - copy; - ...move... - reset; - else sink; - -MANCANO MOVE E RESET - -*) \ No newline at end of file +theorem sem_universal2: ∀M:normalTM. ∀R. + WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R). +#M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize +#t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1) +#q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2) +% [% [@(R_TM_to_R … HRTM) @HMR | //] | //] +qed. +