\ / GNU General Public License Version 2
V_____________________________________________________________*)
-
+include "turing/simple_machines.ma".
include "turing/multi_universal/unistep_aux.ma".
-axiom sem_unistep: ∀M,cf. unistep ⊨ R_unistep_high M cf.
+axiom sem_unistep: ∀M. unistep ⊨ R_unistep_high M.
-definition loop_uni ≝
- ifTM ?? (inject_TM ? (test_char ? (λc.c == bit false)) 2 cfg)
+definition stop ≝ λc.
+ match c with [ bit b ⇒ notb b | _ ⇒ true].
+
+definition uni_body ≝
+ ifTM ?? (mtestR ? cfg 2 stop)
(single_finalTM ?? unistep)
- (nop …) tc_true.
+ (nop …) (mtestR_acc ? cfg 2 stop).
+
+definition acc_body : states ?? uni_body ≝ (inr … (inl … (inr … start_nop))).
-definition lu_acc : states ?? loop_uni ≝ (inr … (inl … (inr … start_nop))).
+definition ub_R_true ≝ λM,t1,t2.
+ ∀c: nconfig (no_states M).
+ t1=low_tapes M c→
+ t2=low_tapes M (step FinBool M c) ∧ halt ? M (cstate … c) = false.
+
+definition ub_R_false ≝ λM,t1,t2.
+ ∀c: nconfig (no_states M).
+ t1 = low_tapes M c → t1 = t2 ∧ halt ? M (cstate … c) = true.
-lemma sem_loop_uni: ∀M,cf.
- loop_uni ⊨ [lu_acc: R_unistep_high M cf, λt1,t2.t1=t2].
+lemma sem_uni_body: ∀M.
+ uni_body ⊨ [acc_body: ub_R_true M, ub_R_false M].
#M #cf
@(acc_sem_if_app ????????????
- (sem_test_char_multi ? (λc.c == bit false) 2 cfg (le_S ?? (le_n 1)))
- (sem_unistep M cf)
+ (sem_mtestR ? cfg 2 stop (le_S ?? (le_n 1)))
+ (sem_unistep M)
(sem_nop …))
-[#t1 #t2 #t3 * #_ #Ht3 >Ht3 // |#t1 #t2 #t3 * #_ #Ht3 whd in ⊢ (%→?); //]
+[#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Ht2 * #q #Mt #Ht1
+ >Ht1 in Htest; >cfg_low_tapes whd in match (bits_of_state ???);
+ #Htest lapply (Htest … (refl ??)) * <Ht1 #Ht3 #Hstop >Ht3 in Ht2;
+ #Ht2 % [@Ht2 //] lapply Hstop whd in match (nhalt ??);
+ cases (nhalt M q) whd in match (stop ?); * /2/
+|#t1 #t2 #t3 whd in ⊢ (%→?); #Htest #Hnop >Hnop -Hnop * #q #Mt #Ht1 >Ht1 in Htest;
+ >cfg_low_tapes whd in match (bits_of_state ???);
+ #Htest lapply (Htest … (refl ??)) whd in match (nhalt ??);
+ cases (nhalt M q) whd in match (stop ?); * /2/
+]
qed.
-definition universalTM ≝ whileTM ?? loop_uni lu_acc.
+definition universalTM ≝ whileTM ?? uni_body acc_body.
-definition low_R ≝ λM,R.λt1,t2:Vector (tape FSUnialpha) 3.
- ∀cin. t1 = low_tapes M cin →
- ∃cout. R (ctape … cin) (ctape … cout) ∧
+definition low_R ≝ λM,q,R.λt1,t2:Vector (tape FSUnialpha) 3.
+ ∀Mt. t1 = low_tapes M (mk_config ?? q Mt) →
+ ∃cout. R Mt (ctape … cout) ∧
halt ? M (cstate … cout) = true ∧ t2 = low_tapes M cout.
-theorem sem_universal: ∀M:normalTM. ∀startc.
- universalTM ⊫ (low_R M (R_TM FinBool M startc)).
-#M #cin #intape #i #outc #Hloop
-lapply (sem_while … (sem_loop_uni intape i outc Hloop)
- [@daemon] -Hloop
-* #ta * #Hstar generalize in match q; -q
-@(star_ind_l ??????? Hstar)
- [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
- cases (Htb … Htb1) -Htb #Hhalt #Htb
- <Htb >Htb1 @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 FinBool ??); >(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) %
- [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??);
- >(eq_pair_fst_snd ?? (trans ???)) @Hloop
+theorem sem_universal: ∀M:normalTM. ∀q.
+ universalTM ⊫ low_R M q (R_TM FinBool M q).
+#M #q #intape #i #outc #Hloop
+lapply (sem_while … (sem_uni_body M … ) intape i outc Hloop) [%] -Hloop
+* #ta * #Hstar lapply q -q @(star_ind_l ??????? Hstar) -Hstar
+ [#q whd in ⊢ (%→?); #HFalse whd #Mt #Hta
+ lapply (HFalse … Hta) * #Hta1 #Hhalt %{(mk_config ?? q Mt)} %
+ [%[%{1} %{(mk_config ?? q Mt)} % // whd in ⊢ (??%?); >Hhalt % |@Hhalt]
+ |<Hta1 @Hta
+ ]
+ |#t1 #t2 whd in ⊢ (%→?); #Hstep #Hstar #IH #q #Hta whd #Mt #Ht1
+ lapply (Hstep … Ht1) * -Hstep #Ht2 #Hhalt
+ lapply(IH (cstate … (step FinBool M (mk_config ?? q Mt))) Hta ??) [@Ht2|skip] -IH
+ * #cout * * #HRTM #Hhalt1 #Houtc
+ %{cout}
+ %[%[cases HRTM #k * #outc1 * <config_expand #Hloop #Houtc1
+ %{(S k)} %{outc1} %
+ [whd in ⊢ (??%?); >Hhalt whd in ⊢ (??%?); @Hloop
|@Houtc1
]
- |@Hhaltq1]
+ |@Hhalt1]
|@Houtc
]
- ]
-*)
+ ]
qed.
-qed.
-
theorem sem_universal2: ∀M:normalTM. ∀R.
M ⊫ R → 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)
+#c * * #HRTM #Hhalt #Ht2 %{c}
% [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
qed.
axiom terminate_UTM: ∀M:normalTM.∀t.
- M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
+ M ↓ t → universalTM ↓ (low_tapes M (mk_config ?? (start ? M) t)).
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department of the University of Bologna, Italy.
+ ||I||
+ ||T||
+ ||A||
+ \ / This file is distributed under the terms of the
+ \ / GNU General Public License Version 2
+ V_____________________________________________________________*)
+
+include "turing/multi_universal/match.ma".
+
+(********************** look_ahead test *************************)
+
+definition mtestR ≝ λsig,i,n,test.
+ (mmove i sig n R) ·
+ (ifTM ?? (inject_TM ? (test_char ? test) n i)
+ (single_finalTM ?? (mmove i sig n L))
+ (mmove i sig n L) tc_true).
+
+
+(* underspecified *)
+definition RmtestR_true ≝ λsig,i,n,test.λt1,t2:Vector ? n.
+ ∀ls,c,c1,rs.
+ nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
+ t1 = t2 ∧ (test c1 = true).
+
+definition RmtestR_false ≝ λsig,i,n,test.λt1,t2:Vector ? n.
+ ∀ls,c,c1,rs.
+ nth i ? t1 (niltape ?) = midtape sig ls c (c1::rs) →
+ t1 = t2 ∧ (test c1 = false).
+
+definition mtestR_acc: ∀sig,i,n,test.states ?? (mtestR sig i n test).
+#sig #i #n #test @inr @inr @inl @inr @start_nop
+qed.
+
+lemma sem_mtestR: ∀sig,i,n,test. i ≤ n →
+ mtestR sig i n test ⊨
+ [mtestR_acc sig i n test:
+ RmtestR_true sig i (S n) test, RmtestR_false sig i (S n) test].
+#sig #i #n #test #Hlein
+@(acc_sem_seq_app sig n … (sem_move_multi … R Hlein)
+ (acc_sem_if sig n ????????
+ (sem_test_char_multi sig test n i Hlein)
+ (sem_move_multi … L Hlein)
+ (sem_move_multi … L Hlein)))
+ [#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); * *
+ #cx #Hcx #Htx #Ht2 #ls #c #c1 #rs #Ht1
+ >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
+ >Ht3 in Hcx; >nth_change_vec [|@le_S_S //] * whd in ⊢ (??%?→?);
+ #Hsome destruct (Hsome) #Htest % [2:@Htest]
+ >Htx in Ht2; whd in ⊢ (%→?); #Ht2 @(eq_vec … (niltape ?))
+ #j #lejn cases (true_or_false (eqb i j)) #Hij
+ [lapply lejn <(eqb_true_to_eq … Hij) #lein >Ht2 >nth_change_vec [2://]
+ >Ht3 >nth_change_vec >Ht1 //
+ |lapply (eqb_false_to_not_eq … Hij) #Hneq >Ht2 >nth_change_vec_neq [2://]
+ >Ht3 >nth_change_vec_neq //
+ ]
+ |#t1 #t2 #t3 whd in ⊢ (%→?); #Hmove * #tx * whd in ⊢ (%→?); *
+ #Hcx #Heqtx #Htx #ls #c #c1 #rs #Ht1
+ >Ht1 in Hmove; whd in match (tape_move ???); #Ht3
+ >Ht3 in Hcx; >nth_change_vec [2:@le_S_S //] #Hcx lapply (Hcx ? (refl ??))
+ #Htest % // @(eq_vec … (niltape ?))
+ #j #lejn cases (true_or_false (eqb i j)) #Hij
+ [lapply lejn <(eqb_true_to_eq … Hij) #lein >Htx >nth_change_vec [2://]
+ >Heqtx >Ht3 >nth_change_vec >Ht1 //
+ |lapply (eqb_false_to_not_eq … Hij) #Hneq >Htx >nth_change_vec_neq [2://]
+ >Heqtx >Ht3 >nth_change_vec_neq //
+ ]
+ ]
+qed.
+
projects / helm.git / commitdiff