From 57103fa96f504f9bffca859dd60317162396657f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Wed, 9 Oct 2013 15:38:16 +0000 Subject: [PATCH] progress in the semantics of binary machines --- .../lib/turing/multi_universal/binaryTM.ma | 126 ++++++++++++++++-- 1 file changed, 114 insertions(+), 12 deletions(-) diff --git a/matita/matita/lib/turing/multi_universal/binaryTM.ma b/matita/matita/lib/turing/multi_universal/binaryTM.ma index 34c9ae4b8..b430afa4e 100644 --- a/matita/matita/lib/turing/multi_universal/binaryTM.ma +++ b/matita/matita/lib/turing/multi_universal/binaryTM.ma @@ -60,15 +60,14 @@ definition trans_binaryTM : ∀sig,states:FinSet. let (H2 : FS_crd sig < S (2*FS_crd sig)) ≝ ? in match pi1 … phase with [ O ⇒ (*** PHASE 0: read ***) - match a with - [ Some a0 ⇒ - match pi1 … count with - [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉 - | S k ⇒ if (a0 == true) - then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉 - else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 ] - | None ⇒ (* Overflow position! *) - 〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ] + match pi1 … count with + [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉 + | S k ⇒ match a with + [ Some a0 ⇒ if (a0 == true) + then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉 + else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 + | None ⇒ (* Overflow position! *) + 〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ] ] | S phase ⇒ match phase with [ O ⇒ (*** PHASE 1: restart ***) match pi1 … count with @@ -131,13 +130,15 @@ definition mk_binaryTM ≝ (trans_binaryTM sig (states sig M) (trans sig M)) (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).// qed. +definition bin_char ≝ λsig,ch.unary_of_nat (FS_crd sig) (index_of_FS sig ch). + definition bin_current ≝ λsig,t.match current ? t with -[ None ⇒ [ ] | Some c ⇒ unary_of_nat (FS_crd sig) (index_of_FS sig c) ]. +[ None ⇒ [ ] | Some c ⇒ bin_char sig c ]. definition tape_bin_lift ≝ λsig,t. -let ls' ≝ flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (left ? t)) in +let ls' ≝ flatten ? (map ?? (bin_char sig) (left ? t)) in let c' ≝ option_hd ? (bin_current sig t) in -let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (right ? t)) in +let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (bin_char sig) (right ? t)) in mk_tape ? ls' c' rs'. definition R_bin_lift ≝ λsig,R,t1,t2. @@ -148,6 +149,96 @@ definition state_bin_lift : ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M) ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉.// qed. +lemma lift_halt_binaryTM : + ∀sig,M,q.halt sig M q = halt ? (mk_binaryTM sig M) (state_bin_lift ? M q). +// qed. + +lemma binaryTM_bin0_bin1 : + ∀sig,M,t,q,ch. + step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,O〉) t) + = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) t. // +qed. + +lemma binaryTM_bin0_bin4 : + ∀sig,M,t,q,ch,k. + current ? t = None ? → S k Hcur % +qed. + +lemma binaryTM_bin0_true : + ∀sig,M,t,q,ch,k. + current ? t = Some ? true → S k Hcur % +qed. + +lemma binaryTM_bin0_false : + ∀sig,M,t,q,ch,k. + current ? t = Some ? false → S k Hcur % +qed. + +(* to be checked *) +axiom binary_to_bin_char :∀sig,csl,csr,a. + csl@true::csr=bin_char sig a → FS_nth ? (length ? csr) = Some ? a. + +lemma binaryTM_phase1_midtape_aux : + ∀sig,M,q,ls,a,rs,k. + halt sig M q=false → + ∀csr,csl,t,ch.length ? csr < S (2*FS_crd sig) → + t = mk_tape ? (reverse ? csl@ls) (option_hd ? (csr@rs)) (tail ? (csr@rs)) → + csl@csr = bin_char sig a → + loopM ? (mk_binaryTM sig M) (S (length ? csr) + k) + (mk_config ?? (〈q,bin0,ch,length ? csr〉) t) + = loopM ? (mk_binaryTM sig M) k + (mk_config ?? (〈q,bin1,Some ? a,FS_crd sig〉) + (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs))). [2,3://] +#sig #M #q #ls #a #rs #k #Hhalt #csr elim csr +[ #csl #t #ch #Hlen #Ht >append_nil #Hcsl >loopM_unfold >loop_S_false [|normalize //] + binaryTM_bin0_bin1 @eq_f >Ht + whd in match (step ???); whd in match (trans ???); loopM_unfold >loop_S_false [|normalize //] + binaryTM_bin0_true + [| >Ht % ] + lapply (IH (csl@[true]) (tape_move FinBool t R) ????) + [ // + | >Ht whd in match (option_hd ??) in ⊢ (??%?); whd in match (tail ??) in ⊢ (??%?); + cases csr0 + [ cases rs + [ normalize >rev_append_def >rev_append_def >reverse_append % + | #r1 #rs1 normalize >rev_append_def >rev_append_def >reverse_append % ] + | #c1 #csr1 normalize >rev_append_def >rev_append_def >reverse_append % ] + | /2/ + | @(Some ? a) ] + #H whd in match (plus ??); >Ha >H @eq_f @eq_f2 // + +qed. + + +lemma binaryTM_phase1_midtape : + ∀sig,M,t,q,ls,a,rs,ch. + t = mk_tape ? ls (option_hd ? (bin_char ? a)) (tail ? (bin_char sig a@rs)) → + step ? (mk_binaryTM sig M) (mk_config ?? (〈q,bin0,ch,FS_crd sig〉) t) + = mk_config ?? (〈q,bin1,ch,to_initN (FS_crd sig) ??〉) + (mk_tape ? (reverse ? (bin_char ? a)@ls) (option_hd ? rs) (tail ? rs)). [2,3://] +#sig #M #t #q #ls #a #rs #ch #Ht +whd in match (step ???); whd in match (trans ???); +>Hcur % +qed. + + lemma binaryTM_loop : ∀sig,M,i,t,q,tf,qf. loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) → @@ -157,6 +248,17 @@ lemma binaryTM_loop : #sig #M #i elim i [ #t #q #qf #tf change with (None ?) in ⊢ (??%?→?); #H destruct (H) | -i #i #IH #t #q #tf #qf + >loopM_unfold + lapply (refl ? (halt sig M (cstate ?? (mk_config ?? q t)))) + cases (halt ?? q) in ⊢ (???%→?); #Hhalt + [ >(loop_S_true ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) + #H destruct (H) %{1} >loopM_unfold >loop_S_true // ] + (* interesting case: more than one step *) + >(loop_S_false ??? (λc.halt ?? (cstate ?? c)) (mk_config ?? q t) Hhalt) + (config_expand ?? (step ???)) #Hloop + lapply (IH … Hloop) -IH * #k0 #IH