include "turing/multi_universal/match.ma".
include "turing/multi_universal/copy.ma".
include "turing/multi_universal/alphabet.ma".
+include "turing/multi_universal/tuples.ma".
(*
(midtape ? (left ? (nth obj ? t1 (niltape ?))) c (right ? (nth obj ? t1 (niltape ?)))) obj)
(mk_tape ? [ ] (option_hd ? (reverse ? (c::ls))) (tail ? (reverse ? (c::ls)))) cfg).
-axiom sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj.
-(*@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
- (sem_seq ??????
- (sem_if ??????????
- (sem_test_null_multi ?? obj ?)
- (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …))
- (sem_move_multi ? 2 cfg L ?))
- (sem_inject ???? cfg ? (sem_write FSUnialpha null)))
- (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
- (sem_move_multi ? 2 cfg R ?)))) //
+lemma sem_cfg_to_obj : cfg_to_obj ⊨ R_cfg_to_obj.
+@(sem_seq_app FSUnialpha 2 ????? (sem_move_multi ? 2 cfg L ?)
+ (sem_seq ??????
+ (sem_if ??????????
+ (acc_sem_inject ?????? cfg ? sem_test_null_char)
+ (sem_nop …)
+ (sem_seq ?????? (accRealize_to_Realize … (sem_copy_step …))
+ (sem_seq ?????? (sem_move_multi ? 2 cfg L ?) (sem_move_multi ? 2 obj L ?))))
+ (sem_seq ?????? (sem_inject ???? cfg ? (sem_move_to_end_l ?))
+ (sem_move_multi ? 2 cfg R ?)))) // [@sym_not_eq //]
#ta #tb *
#tc * whd in ⊢ (%→?); #Htc *
#td * *
-[ * #te * * #Hcurtc #Hte
- * destruct (Hte) #te * *
- [ whd in ⊢ (%→%→?); * #x * #y * * -Hcurtc #Hcurtc1 #Hcurtc2 #Hte #Htd
- * #tf * * * whd in ⊢ (%→%→%→%→?); #Htf1 #Htf2 #Htf3 #Htb
- #c #ls #Hta1 %
- [ #lso #x0 #rso #Hta2 >Hta1 in Htc; >eq_mk_tape_rightof
- whd in match (tape_move ???); #Htc
- cut (tf = change_vec ?? tc (mk_tape ? [ ] (None ?) (reverse ? ls@[x])) cfg)
- [@daemon] -Htf1 -Htf2 -Htf3 #Htf destruct (Htf Hte Htd Htc Htb)
- >change_vec_change_vec >change_vec_change_vec >change_vec_change_vec
- >nth_change_vec // >tape_move_mk_tape_R
- @daemon
- | #Hta2 >Htc in Hcurtc1; >nth_change_vec_neq [| @sym_not_eq //]
- >Hta2 #H destruct (H)
- ]
- | * #Hcurtc0 #Hte #_ #_ #c #ls #Hta1 >Hta1 in Htc; >eq_mk_tape_rightof
- whd in match (tape_move ???); #Htc >Htc in Hcurtc0; *
- [ >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //]
- #Hcurtc #Hcurtc0 >Hcurtc0 in Hcurtc; * #H @False_ind @H %
- | >nth_change_vec // normalize in ⊢ (%→?); #H destruct (H) ]
- ]
-| * #te * * #Hcurtc #Hte
- * whd in ⊢ (%→%→?); #Htd1 #Htd2
- * #tf * * * #Htf1 #Htf2 #Htf3 whd in ⊢ (%→?); #Htb
- #c #ls #Hta1 %
- [ #lso #x #rso #Hta2 >Htc in Hcurtc; >nth_change_vec_neq [|@sym_not_eq //]
- >Hta2 normalize in ⊢ (%→?); #H destruct (H)
- | #_ >Hta1 in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
- destruct (Hte) cut (td = change_vec ?? tc (midtape ? ls null []) cfg)
- [@daemon] -Htd1 -Htd2 #Htd
- -Htf1 cut (tf = change_vec ?? td (mk_tape ? [ ] (None ?) (reverse ? ls@[null])) cfg)
- [@daemon] -Htf2 -Htf3 #Htf destruct (Htf Htd Htc Htb)
+[ * #te * * * #Hcurtc #Hte1 #Hte2 whd in ⊢ (%→?); #Htd destruct (Htd)
+ * #tf * * * #Htf1 #Htf2 #Htf3
+ whd in ⊢ (%→?); #Htb
+ #c #ls #Hta %
+ [ #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ cut (te = tc) [@daemon] -Hte1 -Hte2 #Hte
+ cut (tf = change_vec ? 3 te (mk_tape ? [ ] (None ?) (reverse ? ls@[c])) cfg)
+ [@daemon] -Htf1 -Htf2 -Htf3 #Htf
+ destruct (Htf Hte Htc Htb)
>change_vec_change_vec >change_vec_change_vec >change_vec_change_vec
- >change_vec_change_vec >change_vec_change_vec >nth_change_vec //
- >reverse_cons >tape_move_mk_tape_R /2/ ]
-]
+ >nth_change_vec // >tape_move_mk_tape_R [| #_ % % ]
+ >reverse_cons %
+ | #Hc >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?);
+ #H destruct (H) @False_ind cases Hc /2/ ]
+| * #te * * * #Hcurtc #Hte1 #Hte2
+ * #tf * *
+ [ (* purtroppo copy_step assume che la destinazione sia Some (almeno come semantica) *)
+ STOP
+ * #x * #y * * #Hcurte_cfg #Hcurte_obj #Htf
+ * #tg * whd in ⊢ (%→%→?); #Htg #Htd
+ * #th * * * #Hth1 #Hth2 #Hth3
+ whd in ⊢ (%→%); #Htb
+ #c #ls #Hta % #Hc
+ [ >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ >Htc in Hcurtc; >nth_change_vec // normalize in ⊢ (%→?); >Hc
+ * #H @False_ind /2/
+ | >Hta in Htc; >eq_mk_tape_rightof whd in match (tape_move ???); #Htc
+ cut (te = tc) [@daemon] -Hte1 -Hte2 #Hte
qed.
*)
(* macchina che muove il nastro obj a destra o sinistra a seconda del valore
del current di prg, che codifica la direzione in cui ci muoviamo *)
-
+
+definition char_to_move ≝ λc.match c with
+ [ bit b ⇒ if b then R else L
+ | _ ⇒ N].
+
definition tape_move_obj : mTM FSUnialpha 2 ≝
ifTM ??
(inject_TM ? (test_char ? (λc:FSUnialpha.c == bit false)) 2 prg)
tc_true)
tc_true.
+definition restart_tape ≝ λi.
+ inject_TM ? (move_to_end FSUnialpha L) 2 i ·
+ mmove i FSUnialpha 2 R.
+
definition unistep ≝
- obj_to_cfg · match_m cfg prg FSUnialpha 2 · copy prg cfg FSUnialpha 2 ·
- cfg_to_obj · tape_move_obj.
\ No newline at end of file
+ match_m cfg prg FSUnialpha 2 ·
+ restart_tape cfg · copy prg cfg FSUnialpha 2 ·
+ cfg_to_obj · tape_move_obj · restart_tape prg · obj_to_cfg.
+
+(*
+definition legal_tape ≝ λn,l,h,t.
+ ∃state,char,table.
+ nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) →
+ is_config n (bar::state@[char]) →
+ nth prg ? t1 (niltape ?) = midtape ? [ ] bar table →
+ bar::table = table_TM n l h → *)
+
+definition list_of_tape ≝ λsig,t.
+ left sig t@option_cons ? (current ? t) (right ? t).
+
+definition low_char' ≝ λc.
+ match c with
+ [ None ⇒ null
+ | Some b ⇒ if (is_bit b) then b else null
+ ].
+
+definition R_unistep ≝ λn,l,h.λt1,t2: Vector ? 3.
+ ∀state,char,table.
+ (* cfg *)
+ nth cfg ? t1 (niltape ?) = midtape ? [ ] bar (state@[char]) →
+ is_config n (bar::state@[char]) →
+ (* prg *)
+ nth prg ? t1 (niltape ?) = midtape ? [ ] bar table →
+ bar::table = table_TM n l h →
+ (* obj *)
+ only_bits (list_of_tape ? (nth obj ? t1 (niltape ?))) →
+ let conf ≝ (bar::state@[char]) in
+ (∃ll,lr.bar::table = ll@conf@lr) →
+ ∃nstate,nchar,m,t. tuple_encoding n h t = (conf@nstate@[nchar;m]) ∧
+ mem ? t l ∧
+ let new_obj ≝
+ tape_move_mono ? (nth obj ? t1 (niltape ?))
+ 〈Some ? nchar,char_to_move m〉 in
+ let next_char ≝ low_char' (current ? new_obj) in
+ t2 =
+ change_vec ??
+ (change_vec ?? t1 (midtape ? [ ] bar (nstate@[next_char])) cfg)
+ new_obj obj.
+
+definition tape_map ≝ λA,B:FinSet.λf:A→B.λt.
+ mk_tape B (map ?? f (left ? t))
+ (option_map ?? f (current ? t))
+ (map ?? f (right ? t)).
+
+definition low_tapes ≝ λM:normalTM.λc:nconfig (no_states M).Vector_of_list ?
+ [tape_map ?? bit (ctape ?? c);
+ midtape ? [ ] bar (bits_of_state ? (nhalt M) (cstate ?? c));
+ midtape ? [ ] bar (table_TM ? (graph_enum ?? (ntrans M)) (nhalt M))
+ ].
+
+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
projects / helm.git / blobdiff