notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}.
interpretation "conditional realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
+(******************************** monotonicity ********************************)
+lemma Realize_to_Realize : ∀alpha,M,R1,R2.
+ R1 ⊆ R2 → Realize alpha M R1 → Realize alpha M R2.
+#alpha #M #R1 #R2 #Himpl #HR1 #intape
+cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
+@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
+qed.
+
+lemma WRealize_to_WRealize: ∀sig,M,R1,R2.
+ R1 ⊆ R2 → WRealize sig M R1 → WRealize ? M R2.
+#alpha #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
+@Hsub @(HR1 … i) @Hloop
+qed.
+
+lemma acc_Realize_to_acc_Realize: ∀sig,M.∀q:states sig M.∀R1,R2,R3,R4.
+ R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
+#alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
+cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse
+@(ex_intro ?? k) @(ex_intro ?? outc) %
+ [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
+qed.
+
+(**************************** A canonical relation ****************************)
+
+definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
+∃i,outc.
+ loopM ? M i (mk_config ?? q t1) = Some ? outc ∧
+ t2 = (ctape ?? outc).
+
+lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2.
+ M ⊫ R → R_TM ? M (start sig M) t1 t2 → R t1 t2.
+#sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
+#Hloop #Ht2 >Ht2 @(HMR … Hloop)
+qed.
+
(******************************** NOP Machine *********************************)
(* NO OPERATION
] ] ]
| #x #Hx @Hbits @memb_append_l1 @Hx ]
qed.
-
-lemma Realize_to_Realize :
- ∀alpha,M,R1,R2.(∀t1,t2.R1 t1 t2 → R2 t1 t2) → Realize alpha M R1 → Realize alpha M R2.
-#alpha #M #R1 #R2 #Himpl #HR1 #intape
-cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
-@(ex_intro ?? k) @(ex_intro ?? outc) % /2/
-qed.
lemma sem_move_tape_l_abstract : Realize … move_tape_l R_move_tape_l_abstract.
@(Realize_to_Realize … mtl_concrete_to_abstract) //
(******************************** tuples **************************************)
-(* By general results on FinSets we know that there is every function f between
-two finite sets A and B can be described by means of a finite graph of pairs
+(* By general results on FinSets we know that every function f between two
+finite sets A and B can be described by means of a finite graph of pairs
〈a,f a〉. Hence, the transition function of a normal turing machine can be
described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type:
(Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
-Unfortunately this description is not suitable for an Universal Machine, since
+Unfortunately this description is not suitable for a Universal Machine, since
such a machine must work with a fixed alphabet, while the size on n is unknown.
Hence, we must pass from natural numbers to a representation for them on a
finitary, e.g. binary, alphabet. In general, we shall associate
-to a pair 〈〈i,c〉,〈j,action〉〉 a tuples with the following syntactical structure
+to a pair 〈〈i,c〉,〈j,action〉〉 a tuple with the following syntactical structure
|w_ix,w_jy,z
where
1. "|" and "," are special characters used as delimiters;
2. w_i and w_j are list of booleans representing the states $i$ and $j$;
-3. x is special symbol null if C=None and is a if c=Some a
+3. x is special symbol null if c=None and is a if c=Some a
4. y and z are both null if action = None, and are equal to b,m' if
action = Some b,m;
5. finally, m' = 0 if m = L, m' = 1 if m=R and m' = null if m = N
lemma trans_to_match:
∀n.∀h.∀trans: trans_source n → trans_target n.
- ∀inp,outp,qin,cin,qout,cout,mv. trans inp = outp →
- tuple_encoding n h 〈inp,outp〉 = mk_tuple qin cin qout cout mv →
+ ∀s,t,qin,cin,qout,cout,mv. trans s = t →
+ tuple_encoding n h 〈s,t〉 = mk_tuple qin cin qout cout mv →
match_in_table (S n) qin cin qout cout mv (flatten ? (tuples_list n h (graph_enum ?? trans))).
#n #h #trans #inp #outp #qin #cin #qout #cout #mv #Htrans #Htuple
@(tuple_to_match … (refl…)) <Htuple @mem_map_forward
]
qed. *)
-definition exec_move ≝
+definition exec_action ≝
seq ? init_copy
(seq ? copy
(seq ? (move_r …) move_tape)).
mv ≠ null → c1 ≠ null
dal fatto che c1 e mv sono contenuti nella table
*)
-definition R_exec_move ≝ λt1,t2.
+definition R_exec_action ≝ λt1,t2.
∀n,curconfig,ls,rs,c0,c1,s0,s1,table1,newconfig,mv,table2.
table_TM n (table1@〈comma,false〉::〈s1,false〉::newconfig@〈c1,false〉::〈comma,false〉::〈mv,false〉::table2) →
no_marks curconfig → only_bits (curconfig@[〈s0,false〉]) →
*)
-lemma sem_exec_move : Realize ? exec_move R_exec_move.
+lemma sem_exec_action : Realize ? exec_action R_exec_action.
#intape
cases (sem_seq … sem_init_copy
(sem_seq … sem_copy
match_tuple;
if is_marked(current) = false (* match ok *)
then
- exec_move
+ exec_action
move_r;
else sink;
else nop;
(single_finalTM ? (seq ? init_match
(seq ? match_tuple
(ifTM ? (test_char ? (λc.¬is_marked ? c))
- (seq ? exec_move (move_r …))
+ (seq ? exec_action (move_r …))
(nop ?) (* sink *)
tc_true))))
(nop ?)
axiom sem_match_tuple : Realize ? match_tuple R_match_tuple.
+definition us_acc : states ? uni_step ≝ (inr … (inl … (inr … start_nop))).
+
lemma sem_uni_step :
- accRealize ? uni_step (inr … (inl … (inr … start_nop)))
+ accRealize ? uni_step us_acc
R_uni_step_true R_uni_step_false.
@(acc_sem_if_app STape … (sem_test_char ? (λc:STape.\fst c == bit false))
(sem_seq … sem_init_match
(sem_seq … sem_match_tuple
(sem_if … (* ????????? (sem_test_char … (λc.¬is_marked FSUnialpha c)) *)
- (sem_seq … sem_exec_move (sem_move_r …))
+ (sem_seq … sem_exec_action (sem_move_r …))
(sem_nop …))))
(sem_nop …)
…)
| _ ⇒ 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).
]
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].
+@(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)).
#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)
]
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 #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
projects / helm.git / commitdiff