V_____________________________________________________________*)
-include "turing/universal/trans_to_tuples.ma".
include "turing/universal/uni_step.ma".
(* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
-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
-}.
-
-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:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
-
definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
λM:normalTM.λc.
let n ≝ no_states M in
let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
- let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? t)) in
+ let table ≝ flatten ? (tuples_list n h (graph_enum ?? t)) in
let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
- table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
+ table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
c_low = match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
#t #M #c #eqt
@(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
@(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
- @(ex_intro … (flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
+ @(ex_intro … (flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
@(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
@(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
@(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
| _ ⇒ None ?
].
-(* lemma high_of_lift ≝ ∀ls,c,rs.
- high_tape ls c rs = *)
-
definition map_move ≝
λc,mv.match c with [ null ⇒ None ? | _ ⇒ Some ? 〈c,false,move_of_unialpha mv〉 ].
-(* axiom high_tape_move : ∀t1,ls,c,rs, c1,mv.
- legal_tape ls c rs →
- t1 = lift_tape ls c rs →
- high_tape_from_tape (tape_move STape t1 (map_move c1 mv)) =
- tape_move FinBool (high_tape_from_tape t1) (high_move c1 mv). *)
-
definition low_step_R_true ≝ λt1,t2.
∀M:normalTM.
∀c: nconfig (no_states M).
(* sufficent conditions to have a low_level_config *)
lemma is_low_config: ∀ls,c,rs,M,s,tape,qhd,q_tl,table.
legal_tape ls c rs →
-table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
+table = flatten ? (tuples_list (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) →
lift_tape ls c rs = low_tape_aux M tape →
〈qhd,false〉::q_tl = m_bits_of_state (no_states M) (nhalt M) s →
midtape STape (〈grid,false〉::ls)
]
qed.
-lemma unistep_to_low_step: ∀t1,t2.
+lemma unistep_true_to_low_step: ∀t1,t2.
R_uni_step_true t1 t2 → low_step_R_true t1 t2.
#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
cases (low_config_eq … eqt1)
]
]
qed.
-
+
definition low_step_R_false ≝ λt1,t2.
∀M:normalTM.
∀c: nconfig (no_states M).
t1 = low_config M c → halt ? M (cstate … c) = true ∧ t1 = t2.
+lemma unistep_false_to_low_step: ∀t1,t2.
+ R_uni_step_false t1 t2 → low_step_R_false t1 t2.
+#t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step * #n #posn #t #h * #qin #tape #eqt1
+cases (low_config_eq … eqt1) #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
+***** #_ #_ #_ #Hqin #_ #Ht1 whd in match (halt ???);
+cases (Huni_step (h qin) ?) [/2/] >Ht1 whd in ⊢ (??%?); @eq_f
+normalize in Hqin; destruct (Hqin) %
+qed.
+
definition low_R ≝ λM,qstart,R,t1,t2.
∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
∃q,tape2.R tape1 tape2 ∧
halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
-definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
-∃i,outc.
- loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
- t2 = (ctape ?? outc).
-
-(*
-definition universal_R ≝ λM,R,t1,t2.
- Realize ? M R →
- ∀tape1,tape2.
- R tape1 tape 2 ∧
- t1 = low_config M (initc ? M tape1) ∧
- ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
-
-axiom uni_step: TM STape.
-axiom us_acc: states ? uni_step.
-
-axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
+lemma sem_uni_step1:
+ uni_step ⊨ [us_acc: low_step_R_true, low_step_R_false].
+@daemon (* this no longer works: TODO *) (*
+@(acc_Realize_to_acc_Realize … sem_uni_step)
+ [@unistep_true_to_low_step | @unistep_false_to_low_step ]
+*)
+qed.
definition universalTM ≝ whileTM ? uni_step us_acc.
theorem sem_universal: ∀M:normalTM. ∀qstart.
- WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
+ universalTM ⊫ (low_R M qstart (R_TM FinBool M qstart)).
+@daemon (* this no longer works: TODO *) (*
#M #q #intape #i #outc #Hloop
-lapply (sem_while … sem_uni_step intape i outc Hloop)
+lapply (sem_while … sem_uni_step1 intape i outc Hloop)
[@daemon] -Hloop
* #ta * #Hstar generalize in match q; -q
@(star_ind_l ??????? Hstar)
[%
[cases HRTM #k * #outc1 * #Hloop #Houtc1
@(ex_intro … (S k)) @(ex_intro … outc1) %
- [>loop_S_false [2://] whd in match (step FinBool ??);
+ [>loopM_unfold >loop_S_false [2://] whd in match (step FinBool ??);
>(eq_pair_fst_snd ?? (trans ???)) @Hloop
|@Houtc1
]
|@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.
-
theorem sem_universal2: ∀M:normalTM. ∀R.
- WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) 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)
% [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
qed.
+axiom terminate_UTM: ∀M:normalTM.∀t.
+ M ↓ t → universalTM ↓ (low_config M (mk_config ?? (start ? M) t)).
+
projects / helm.git / blobdiff