1 include "turing/mono.ma".
2 include "basics/vectors.ma".
4 (* We do not distinuish an input tape *)
6 record mTM (sig:FinSet): Type[1] ≝
8 tapes_no: nat; (* additional working tapes *)
9 trans : states × (Vector (option sig) (S tapes_no)) →
10 states × (Vector (option (sig × move))(S tapes_no));
15 record mconfig (sig,states:FinSet) (n:nat): Type[0] ≝
17 ctapes : Vector (tape sig) (S n)
20 definition current_chars ≝ λsig.λn.λtapes.
21 vec_map ?? (current sig) (S n) tapes.
23 definition step ≝ λsig.λM:mTM sig.λc:mconfig sig (states ? M) (tapes_no ? M).
24 let 〈news,mvs〉 ≝ trans sig M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in
27 (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs).
29 definition empty_tapes ≝ λsig.λn.
30 mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?.
31 elim n // normalize //
34 (************************** Realizability *************************************)
35 definition loopM ≝ λsig.λM:mTM sig.λi,cin.
36 loop ? i (step sig M) (λc.halt sig M (cstate ??? c)) cin.
38 lemma loopM_unfold : ∀sig,M,i,cin.
39 loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ??? c)) cin.
42 definition initc ≝ λsig.λM:mTM sig.λtapes.
43 mk_mconfig sig (states sig M) (tapes_no sig M) (start sig M) tapes.
45 definition Realize ≝ λsig.λM:mTM sig.λR:relation (Vector (tape sig) ?).
47 loopM sig M i (initc sig M t) = Some ? outc ∧ R t (ctapes ??? outc).
49 definition WRealize ≝ λsig.λM:mTM sig.λR:relation (Vector (tape sig) ?).
51 loopM sig M i (initc sig M t) = Some ? outc → R t (ctapes ??? outc).
53 definition Terminate ≝ λsig.λM:mTM sig.λt. ∃i,outc.
54 loopM sig M i (initc sig M t) = Some ? outc.
56 (* notation "M \vDash R" non associative with precedence 45 for @{ 'models $M $R}. *)
57 interpretation "multi realizability" 'models M R = (Realize ? M R).
59 (* notation "M \VDash R" non associative with precedence 45 for @{ 'wmodels $M $R}. *)
60 interpretation "weak multi realizability" 'wmodels M R = (WRealize ? M R).
62 interpretation "multi termination" 'fintersects M t = (Terminate ? M t).
64 lemma WRealize_to_Realize : ∀sig.∀M: mTM sig.∀R.
65 (∀t.M ↓ t) → M ⊫ R → M ⊨ R.
66 #sig #M #R #HT #HW #t cases (HT … t) #i * #outc #Hloop
67 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
70 theorem Realize_to_WRealize : ∀sig.∀M:mTM sig.∀R.
72 #sig #M #R #H1 #inc #i #outc #Hloop
73 cases (H1 inc) #k * #outc1 * #Hloop1 #HR >(loop_eq … Hloop Hloop1) //
76 definition accRealize ≝ λsig.λM:mTM sig.λacc:states sig M.λRtrue,Rfalse.
78 loopM sig M i (initc sig M t) = Some ? outc ∧
79 (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
80 (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
82 (* notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}. *)
83 interpretation "conditional multi realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
85 (*************************** guarded realizablity *****************************)
86 definition GRealize ≝ λsig.λM:mTM sig.λPre:Vector (tape sig) ? →Prop.λR:relation (Vector (tape sig) ?).
88 loopM sig M i (initc sig M t) = Some ? outc ∧ R t (ctapes ??? outc).
90 definition accGRealize ≝ λsig.λM:mTM sig.λacc:states sig M.
91 λPre: Vector (tape sig) ? → Prop.λRtrue,Rfalse.
93 loopM sig M i (initc sig M t) = Some ? outc ∧
94 (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
95 (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
97 lemma WRealize_to_GRealize : ∀sig.∀M: mTM sig.∀Pre,R.
98 (∀t.Pre t → M ↓ t) → M ⊫ R → GRealize sig M Pre R.
99 #sig #M #Pre #R #HT #HW #t #HPre cases (HT … t HPre) #i * #outc #Hloop
100 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
103 lemma Realize_to_GRealize : ∀sig.∀M: mTM sig.∀P,R.
104 M ⊨ R → GRealize sig M P R.
105 #alpha #M #Pre #R #HR #t #HPre
106 cases (HR t) -HR #k * #outc * #Hloop #HR
107 @(ex_intro ?? k) @(ex_intro ?? outc) %
111 lemma acc_Realize_to_acc_GRealize: ∀sig.∀M:mTM sig.∀q:states sig M.∀P,R1,R2.
112 M ⊨ [q:R1,R2] → accGRealize sig M q P R1 R2.
113 #alpha #M #q #Pre #R1 #R2 #HR #t #HPre
114 cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse
115 @(ex_intro ?? k) @(ex_intro ?? outc) %
116 [ % [@Hloop] @HRtrue | @HRfalse]
119 (******************************** monotonicity ********************************)
120 lemma Realize_to_Realize : ∀sig.∀M:mTM sig.∀R1,R2.
121 R1 ⊆ R2 → Realize sig M R1 → Realize sig M R2.
122 #alpha #M #R1 #R2 #Himpl #HR1 #intape
123 cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
124 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
127 lemma WRealize_to_WRealize: ∀sig.∀M:mTM sig.∀R1,R2.
128 R1 ⊆ R2 → WRealize sig M R1 → WRealize ? M R2.
129 #alpha #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
130 @Hsub @(HR1 … i) @Hloop
133 lemma GRealize_to_GRealize : ∀sig.∀M:mTM sig.∀P,R1,R2.
134 R1 ⊆ R2 → GRealize sig M P R1 → GRealize sig M P R2.
135 #alpha #M #P #R1 #R2 #Himpl #HR1 #intape #HP
136 cases (HR1 intape HP) -HR1 #k * #outc * #Hloop #HR1
137 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
140 lemma GRealize_to_GRealize_2 : ∀sig.∀M:mTM sig.∀P1,P2,R1,R2.
141 P2 ⊆ P1 → R1 ⊆ R2 → GRealize sig M P1 R1 → GRealize sig M P2 R2.
142 #alpha #M #P1 #P2 #R1 #R2 #Himpl1 #Himpl2 #H1 #intape #HP
143 cases (H1 intape (Himpl1 … HP)) -H1 #k * #outc * #Hloop #H1
144 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
147 lemma acc_Realize_to_acc_Realize: ∀sig.∀M:mTM sig.∀q:states sig M.∀R1,R2,R3,R4.
148 R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
149 #alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
150 cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse
151 @(ex_intro ?? k) @(ex_intro ?? outc) %
152 [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
155 (**************************** A canonical relation ****************************)
157 definition R_mTM ≝ λsig.λM:mTM sig.λq.λt1,t2.
159 loopM ? M i (mk_mconfig ??? q t1) = Some ? outc ∧
160 t2 = (ctapes ??? outc).
162 lemma R_mTM_to_R: ∀sig.∀M:mTM sig.∀R. ∀t1,t2.
163 M ⊫ R → R_mTM ? M (start sig M) t1 t2 → R t1 t2.
164 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
165 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
168 (******************************** NOP Machine *********************************)
173 definition nop_states ≝ initN 1.
174 definition start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … 1). *)
177 λalpha:FinSet.λn.mk_mTM alpha nop_states n
178 (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
183 definition R_mnop ≝ λalpha,n.λt1,t2:Vector (tape alpha) (S n).t2 = t1.
186 ∀alpha,n.mnop alpha n⊨ R_mnop alpha n.
187 #alpha #n #intapes @(ex_intro ?? 1)
188 @(ex_intro … (mk_mconfig ??? start_nop intapes)) % %
191 lemma mnop_single_state: ∀sig,n.∀q1,q2:states ? (mnop sig n). q1 = q2.
192 normalize #sig #n0 * #n #ltn1 * #m #ltm1
193 generalize in match ltn1; generalize in match ltm1;
194 <(le_n_O_to_eq … (le_S_S_to_le … ltn1)) <(le_n_O_to_eq … (le_S_S_to_le … ltm1))
197 (************************** Sequential Composition ****************************)
199 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
203 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
204 else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in 〈inl … news1,m〉
205 | inr s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in 〈inr … news2,m〉
208 definition seq ≝ λsig. λM1,M2 : TM sig.
210 (FinSum (states sig M1) (states sig M2))
211 (seq_trans sig M1 M2)
212 (inl … (start sig M1))
214 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
216 notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
217 interpretation "sequential composition" 'middot a b = (seq ? a b).
219 definition lift_confL ≝
220 λsig,S1,S2,c.match c with
221 [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inl … s) t ].
223 definition lift_confR ≝
224 λsig,S1,S2,c.match c with
225 [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inr … s) t ].
227 definition halt_liftL ≝
228 λS1,S2,halt.λs:FinSum S1 S2.
231 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
233 definition halt_liftR ≝
234 λS1,S2,halt.λs:FinSum S1 S2.
237 | inr s2 ⇒ halt s2 ].
239 lemma p_halt_liftL : ∀sig,S1,S2,halt,c.
240 halt (cstate sig S1 c) =
241 halt_liftL S1 S2 halt (cstate … (lift_confL … c)).
242 #sig #S1 #S2 #halt #c cases c #s #t %
245 lemma trans_seq_liftL : ∀sig,M1,M2,s,a,news,move.
246 halt ? M1 s = false →
247 trans sig M1 〈s,a〉 = 〈news,move〉 →
248 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
249 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
250 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
253 lemma trans_seq_liftR : ∀sig,M1,M2,s,a,news,move.
254 halt ? M2 s = false →
255 trans sig M2 〈s,a〉 = 〈news,move〉 →
256 trans sig (seq sig M1 M2) 〈inr … s,a〉 = 〈inr … news,move〉.
257 #sig #M1 * #Q2 #T2 #init2 #halt2 #s #a #news #move
258 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
261 lemma step_seq_liftR : ∀sig,M1,M2,c0.
262 halt ? M2 (cstate ?? c0) = false →
263 step sig (seq sig M1 M2) (lift_confR sig (states ? M1) (states ? M2) c0) =
264 lift_confR sig (states ? M1) (states ? M2) (step sig M2 c0).
265 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
266 lapply (refl ? (trans ?? 〈s,current sig t〉))
267 cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
270 | 2,3: #s1 #l1 #Heq #Hhalt
271 |#ls #s1 #rs #Heq #Hhalt ]
272 whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
273 whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftR … Heq) //
276 lemma step_seq_liftL : ∀sig,M1,M2,c0.
277 halt ? M1 (cstate ?? c0) = false →
278 step sig (seq sig M1 M2) (lift_confL sig (states ? M1) (states ? M2) c0) =
279 lift_confL sig ?? (step sig M1 c0).
280 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
281 lapply (refl ? (trans ?? 〈s,current sig t〉))
282 cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
285 | 2,3: #s1 #l1 #Heq #Hhalt
286 |#ls #s1 #rs #Heq #Hhalt ]
287 whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
288 whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftL … Heq) //
291 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
293 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
294 #sig #M1 #M2 #s #a #Hhalt whd in ⊢ (??%?); >Hhalt %
297 lemma eq_ctape_lift_conf_L : ∀sig,S1,S2,outc.
298 ctape sig (FinSum S1 S2) (lift_confL … outc) = ctape … outc.
299 #sig #S1 #S2 #outc cases outc #s #t %
302 lemma eq_ctape_lift_conf_R : ∀sig,S1,S2,outc.
303 ctape sig (FinSum S1 S2) (lift_confR … outc) = ctape … outc.
304 #sig #S1 #S2 #outc cases outc #s #t %
307 theorem sem_seq: ∀sig.∀M1,M2:TM sig.∀R1,R2.
308 M1 ⊨ R1 → M2 ⊨ R2 → M1 · M2 ⊨ R1 ∘ R2.
309 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
310 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
311 cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2
312 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
314 [@(loop_merge ???????????
315 (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
316 (step sig M1) (step sig (seq sig M1 M2))
317 (λc.halt sig M1 (cstate … c))
318 (λc.halt_liftL ?? (halt sig M1) (cstate … c)) … Hloop1))
320 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
321 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
322 || #c0 #Hhalt <step_seq_liftL //
324 |6:cases outc1 #s1 #t1 %
325 |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
327 | #c0 #Hhalt <step_seq_liftR // ]
328 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
329 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
330 >(trans_liftL_true sig M1 M2 ??)
331 [ whd in ⊢ (??%?); whd in ⊢ (???%);
332 @config_eq whd in ⊢ (???%); //
333 | @(loop_Some ?????? Hloop10) ]
335 | @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
336 % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
340 theorem sem_seq_app: ∀sig.∀M1,M2:TM sig.∀R1,R2,R3.
341 M1 ⊨ R1 → M2 ⊨ R2 → R1 ∘ R2 ⊆ R3 → M1 · M2 ⊨ R3.
342 #sig #M1 #M2 #R1 #R2 #R3 #HR1 #HR2 #Hsub
343 #t cases (sem_seq … HR1 HR2 t)
344 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
345 % [@Hloop |@Hsub @Houtc]
348 (* composition with guards *)
349 theorem sem_seq_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2.
350 GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
351 (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) →
352 GRealize sig (M1 · M2) Pre1 (R1 ∘ R2).
353 #sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #HGR1 #HGR2 #Hinv #t1 #HPre1
354 cases (HGR1 t1 HPre1) #k1 * #outc1 * #Hloop1 #HM1
355 cases (HGR2 (ctape sig (states ? M1) outc1) ?)
356 [2: @(Hinv … HPre1 HM1)]
357 #k2 * #outc2 * #Hloop2 #HM2
358 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
360 [@(loop_merge ???????????
361 (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
362 (step sig M1) (step sig (seq sig M1 M2))
363 (λc.halt sig M1 (cstate … c))
364 (λc.halt_liftL ?? (halt sig M1) (cstate … c)) … Hloop1))
366 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
367 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
368 || #c0 #Hhalt <step_seq_liftL //
370 |6:cases outc1 #s1 #t1 %
371 |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
373 | #c0 #Hhalt <step_seq_liftR // ]
374 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
375 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
376 >(trans_liftL_true sig M1 M2 ??)
377 [ whd in ⊢ (??%?); whd in ⊢ (???%);
378 @config_eq whd in ⊢ (???%); //
379 | @(loop_Some ?????? Hloop10) ]
381 | @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
382 % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
386 theorem sem_seq_app_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2,R3.
387 GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
388 (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) → R1 ∘ R2 ⊆ R3 →
389 GRealize sig (M1 · M2) Pre1 R3.
390 #sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #R3 #HR1 #HR2 #Hinv #Hsub
391 #t #HPre1 cases (sem_seq_guarded … HR1 HR2 Hinv t HPre1)
392 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
393 % [@Hloop |@Hsub @Houtc]
403 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
404 halt sig M (state sig M c).
406 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
409 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
412 (* Compute ? M f states that f is computed by M *)
413 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
415 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
418 (* for decision problems, we accept a string if on termination
419 output is not empty *)
421 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
423 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
424 (isnilb ? (out ?? c) = false).
426 (* alternative approach.
427 We define the notion of computation. The notion must be constructive,
428 since we want to define functions over it, like lenght and size
430 Perche' serve Type[2] se sposto a e b a destra? *)
432 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
433 mk_move: p a = false → b = f a → cmove A f p a b.
435 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
436 | empty : ∀a. cstar A M a a
437 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
439 definition computation ≝ λsig.λM:TM sig.
440 cstar ? (cmove ? (step sig M) (stop sig M)).
442 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
443 ∀l.∃c.computation sig M (init sig M l) c →
444 (stop sig M c = true) ∧ out ?? c = f l.
446 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
447 ∀l.∃c.computation sig M (init sig M l) c →
448 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).