From 00101d30f0bf914a26ed2ec61a1aa38598b05209 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Sun, 20 Jan 2013 12:31:17 +0000 Subject: [PATCH] semantics of unistep --- matita/matita/lib/turing/mono.ma | 10 ++ .../lib/turing/multi_universal/normalTM.ma | 20 ++- .../lib/turing/multi_universal/tuples.ma | 24 ++- .../lib/turing/multi_universal/unistep_aux.ma | 154 +++++++++++++++++- 4 files changed, 197 insertions(+), 11 deletions(-) diff --git a/matita/matita/lib/turing/mono.ma b/matita/matita/lib/turing/mono.ma index bab3ab1ba..1508c6c9e 100644 --- a/matita/matita/lib/turing/mono.ma +++ b/matita/matita/lib/turing/mono.ma @@ -134,6 +134,16 @@ definition step ≝ λsig.λM:TM sig.λc:config sig (states sig M). let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv). +(* +lemma step_eq : ∀sig,M,c. + let current_char ≝ current ? (ctape ?? c) in + let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in + step sig M c = + mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv). +#sig #M #c + whd in match (tape_move_mono sig ??); +*) + (******************************** loop ****************************************) let rec loop (A:Type[0]) n (f:A→A) p a on n ≝ match n with diff --git a/matita/matita/lib/turing/multi_universal/normalTM.ma b/matita/matita/lib/turing/multi_universal/normalTM.ma index 13ef8a66c..8e3af494a 100644 --- a/matita/matita/lib/turing/multi_universal/normalTM.ma +++ b/matita/matita/lib/turing/multi_universal/normalTM.ma @@ -80,16 +80,34 @@ record normalTM : Type[0] ≝ nhalt : initN no_states → bool }. +lemma decomp_target : ∀n.∀tg: trans_target n. + ∃qout,cout,m. tg = 〈qout,cout,m〉. +#n * * #q #c #m %{q} %{c} %{m} // +qed. + (* A normal machine is just a special case of Turing Machine. *) +definition nstart_state ≝ λM.mk_Sig ?? 0 (pos_no_states M). + definition normalTM_to_TM ≝ λM:normalTM. mk_TM FinBool (initN (no_states M)) - (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M). + (ntrans M) (nstart_state M) (nhalt M). coercion normalTM_to_TM. definition nconfig ≝ λn. config FinBool (initN n). +(* A normal machine has a non empty graph *) + +definition sample_input: ∀M.trans_source (no_states M). +#M % [@(nstart_state M) | %] +qed. + +lemma nTM_nog: ∀M. graph_enum ?? (ntrans M) ≠ [ ]. +#M % #H lapply(graph_enum_complete ?? (ntrans M) (sample_input M) ? (refl ??)) +>H normalize #Hd destruct +qed. + (******************************** tuples **************************************) (* By general results on FinSets we know that every function f between two diff --git a/matita/matita/lib/turing/multi_universal/tuples.ma b/matita/matita/lib/turing/multi_universal/tuples.ma index 0fe4508ed..428d99ccf 100644 --- a/matita/matita/lib/turing/multi_universal/tuples.ma +++ b/matita/matita/lib/turing/multi_universal/tuples.ma @@ -21,8 +21,30 @@ lemma table_TM_cons: ∀n,h,t,o. table_TM n (t::o) h = (tuple_encoding n h t)@(table_TM n o h). // qed. +lemma initial_bar: ∀n,h,l. l ≠ [ ] → + table_TM n l h = bar :: tail ? (table_TM n l h). +#n #h * + [* #H @False_ind @H // + |#a #tl #_ >table_TM_cons lapply (is_tuple n h a) + * #qin * #cin * #qout * #cout * #mv * #_ #Htup >Htup % + ] +qed. + (************************** matching in a table *******************************) -lemma list_to_table: ∀n,l,h,tup. mem ? tup (tuples_list n h l) → +lemma list_to_table: ∀n,l,h,t. mem ? t l → + ∃ll,lr.table_TM n l h = ll@(tuple_encoding n h t)@lr. +#n #l #h #t elim l + [@False_ind + |#hd #tl #Hind * + [#Htup %{[]} %{(table_TM n tl h)} >Htup % + |#H cases (Hind H) #ll * #lr #H1 + %{((tuple_encoding n h hd)@ll)} %{lr} + >associative_append

map_write >map_move % +qed. + +lemma map_move_mono: ∀t,cout,m. + tape_move_mono ? (tape_map FinBool ? bit t) + 〈char_to_bit_option (low_char cout), char_to_move (low_mv m)〉 + = tape_map ?? bit (tape_move_mono ? t 〈cout,m〉). +@map_action +qed. definition R_unistep_high ≝ λM:normalTM.λc:nconfig (no_states M).λt1,t2. t1 = low_tapes M c → t2 = low_tapes M (step ? M c). - - - \ No newline at end of file +lemma R_unistep_equiv : ∀M,c,t1,t2. + R_unistep (no_states M) (graph_enum ?? (ntrans M)) (nhalt M) t1 t2 → + R_unistep_high M c t1 t2. +#M #c #t1 #t2 #H #Ht1 +lapply (initial_bar ? (nhalt M) (graph_enum ?? (ntrans M)) (nTM_nog ?)) #Htable +(* tup = current tuple *) +cut (∃t.t = 〈〈cstate … c,current ? (ctape … c)〉, + ntrans M 〈cstate … c,current ? (ctape … c)〉〉) [% //] * #tup #Htup +(* tup is in the graph *) +cut (mem ? tup (graph_enum ?? (ntrans M))) + [@memb_to_mem >Htup @(graph_enum_complete … (ntrans M)) %] #Hingraph +(* tupe target = 〈qout,cout,m〉 *) +lapply (decomp_target ? (ntrans M 〈cstate … c,current ? (ctape … c)〉)) +* #qout * #cout * #m #Htg >Htg in Htup; #Htup +(* new config *) +cut (step FinBool M c = mk_config ?? qout (tape_move ? (tape_write ? (ctape … c) cout) m)) + [>(config_expand … c) whd in ⊢ (??%?); (* >Htg ?? why not?? *) + cut (trans ? M 〈cstate … c, current ? (ctape … c)〉 = 〈qout,cout,m〉) [Heq1 %] #Hstep +(* new state *) +cut (cstate ?? (step FinBool M c) = qout) [>Hstep %] #Hnew_state +(* new tape *) +cut (ctape ?? (step FinBool M c) = tape_move ? (tape_write ? (ctape … c) cout) m) + [>Hstep %] #Hnew_tape +lapply(H (bits_of_state ? (nhalt M) (cstate ?? c)) + (low_char (current ? (ctape ?? c))) + (tail ? (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))) + ??????) +[Htable1 @eq_f Htup + whd in ⊢ (??%?); @eq_f >associative_append % +|>Ht1 >obj_low_tapes >map_list_of_tape elim (list_of_tape ??) + [#b @False_ind | #b #tl #Hind #a * [#Ha >Ha //| @Hind]] +|@sym_eq @Htable +|>Ht1 % +|%{(bits_of_state ? (nhalt M) (cstate ?? c))} %{(low_char (current ? (ctape ?? c)))} + % [% [% [// | cases (current ??) normalize [|#b] % #Hd destruct (Hd)] + |>length_map whd in match (length ??); @eq_f //] + |//] +|>Ht1 >cfg_low_tapes //] -H #H +lapply(H (bits_of_state … (nhalt M) qout) (low_char … cout) + (low_mv … m) tup ? Hingraph) + [>Htup whd in ⊢ (??%?); @eq_f >associative_append %] -H +#Ht2 >Ht2 @(eq_vec ? 3 … (niltape ?)) #i #Hi +cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi + [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi + [cases (le_to_or_lt_eq … (le_S_S_to_le … Hi)) -Hi #Hi + [@False_ind /2/ + |>Hi >obj_low_tapes >nth_change_vec // + >Ht1 >obj_low_tapes >Hstep @map_action + ] + |>Hi >cfg_low_tapes >nth_change_vec_neq + [|% whd in ⊢ (??%?→?); #H destruct (H)] + >nth_change_vec // >Hnew_state @eq_f @eq_f >Hnew_tape + @eq_f2 [|2:%] >Ht1 >obj_low_tapes >map_move_mono >low_char_current % + ] + |(* program tapes do not change *) + >Hi >prg_low_tapes + >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)] + >nth_change_vec_neq [|% whd in ⊢ (??%?→?); #H destruct (H)] + >Ht1 >prg_low_tapes // + ] +qed. + + + + \ No newline at end of file -- 2.39.2