2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "turing/mono.ma".
13 include "basics/star.ma".
15 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
17 if s == q then 〈start ? M, None ?〉
20 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
23 (while_trans sig M qacc)
25 (λs.halt sig M s ∧ ¬ s==qacc).
27 axiom daemon : ∀X:Prop.X.
29 lemma while_trans_false : ∀sig,M,q,p.
30 \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
31 #sig #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
34 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
35 (∀x.subh x = true → h x = true) →
36 (∀x.subh x = false → hlift (lift x) = h x) →
37 (∀x.h x = false → lift (f x) = g (lift x)) →
39 loop A k f h c1 = Some ? c2 →
40 loop B k g hlift (lift c1) = Some ? (lift … c2).
41 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
42 generalize in match c1; elim k
43 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
44 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
45 cases (true_or_false (h c0)) #Hc0 >Hc0
46 [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
47 | normalize >(Hlift c0)
48 [>Hc0 normalize <(Hfg … Hc0) @IH
49 |cases (true_or_false (subh c0)) //
50 #H <Hc0 @sym_eq >H @Hsubh //
55 axiom tech1: ∀A.∀R1,R2:relation A.
56 ∀a,b. (R1 ∘ ((star ? R1) ∘ R2)) a b → ((star ? R1) ∘ R2) a b.
58 lemma halt_while_acc :
59 ∀sig,M,acc.halt sig (whileTM sig M acc) acc = false.
60 #sig #M #acc normalize >(\b ?) //
61 cases (halt sig M acc) %
64 lemma step_while_acc :
65 ∀sig,M,acc,c.cstate ?? c = acc →
66 step sig (whileTM sig M acc) c = initc … (ctape ?? c).
67 #sig #M #acc * #s #t #Hs normalize >(\b Hs) %
71 ∀A,k,f,p,a.p a = true → loop A (S k) f p a = Some ? a.
72 #A #k #f #p #a #Ha normalize >Ha %
75 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
76 halt sig M acc = true →
77 accRealize sig M acc Rtrue Rfalse →
78 WRealize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse).
79 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t #i
80 generalize in match t;
81 @(nat_elim1 … i) #m #Hind #intape #outc #Hloop
82 cases (loop_split ?? (λc. halt sig M (cstate ?? c)) ????? Hloop)
83 [#k1 * #outc1 * #Hloop1 #Hloop2
84 cases (HaccR intape) #k * #outcM * * #HloopM #HMtrue #HMfalse
86 [ @(loop_eq … k … Hloop1)
87 @(loop_lift ?? k (λc.c) ?
88 (step ? (whileTM ? M acc)) ?
89 (λc.halt sig M (cstate ?? c)) ??
92 | * #s #t #Hx whd in ⊢ (??%%); >while_trans_false
94 |% #Hfalse <Hfalse in Hacctrue; >Hx #H0 destruct ]
96 | #HoutcM1 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
97 [@tech1 @(ex_intro … (ctape ?? outc1)) %
98 [ <HoutcM1 @HMtrue >HoutcM1 @(\P Hacc)
101 [normalize #H destruct (H) ]
102 #m' #_ cases k1 in Hloop1;
103 [normalize #H destruct (H) ]
104 #k1' #_ normalize /2/
105 | <Hloop2 whd in ⊢ (???%);
106 >(\P Hacc) >halt_while_acc whd in ⊢ (???%);
107 normalize in match (halt ?? acc);
108 >step_while_acc // @(\P Hacc)
111 |@(ex_intro … intape) % //
112 cut (Some ? outc1 = Some ? outc)
113 [ <Hloop1 <Hloop2 >loop_p_true in ⊢ (???%); //
114 normalize >(loop_Some ?????? Hloop1) >Hacc %
115 | #Houtc1c destruct @HMfalse @(\Pf Hacc)
119 | * #s0 #t0 normalize cases (s0 == acc) normalize
120 [ cases (halt sig M s0) normalize #Hfalse destruct
121 | cases (halt sig M s0) normalize //
127 (* We do not distinuish an input tape *)
129 record TM (sig:FinSet): Type[1] ≝
131 trans : states × (option sig) → states × (option (sig × move));
136 record config (sig:FinSet) (M:TM sig): Type[0] ≝
137 { cstate : states sig M;
141 definition option_hd ≝ λA.λl:list A.
147 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
152 [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
153 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
157 definition step ≝ λsig.λM:TM sig.λc:config sig M.
158 let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
159 let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
160 mk_config ?? news (tape_move sig (ctape ?? c) mv).
162 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
165 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
168 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
169 loop A k1 f p a1 = Some ? a2 →
170 loop A (k2+k1) f p a1 = Some ? a2.
171 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
172 [normalize #a0 #Hfalse destruct
173 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
174 cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
178 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
180 loop A k1 f p a1 = Some ? a2 →
181 f a2 = a3 → q a2 = false →
182 loop A k2 f q a3 = Some ? a4 →
183 loop A (k1+k2) f q a1 = Some ? a4.
184 #Sig #f #p #q #Hpq #k1 elim k1
185 [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
186 |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
187 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
188 [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
189 whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
190 whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
191 |normalize >(Hpq … pa1) normalize
192 #H1 #H2 #H3 @(Hind … H2) //
198 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
200 loop A k1 f p a1 = Some ? a2 →
201 loop A k2 f q a2 = Some ? a3 →
202 loop A (k1+k2) f q a1 = Some ? a3.
203 #Sig #f #p #q #Hpq #k1 elim k1
204 [normalize #k2 #a1 #a2 #a3 #H destruct
205 |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
206 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
207 [#eqa1a2 destruct #H @loop_incr //
208 |normalize >(Hpq … pa1) normalize
209 #H1 #H2 @(Hind … H2) //
215 definition initc ≝ λsig.λM:TM sig.λt.
216 mk_config sig M (start sig M) t.
218 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
220 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
225 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
229 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
231 let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
234 let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
238 definition seq ≝ λsig. λM1,M2 : TM sig.
240 (FinSum (states sig M1) (states sig M2))
241 (seq_trans sig M1 M2)
242 (inl … (start sig M1))
244 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
246 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
247 ∃am.R1 a1 am ∧ R2 am a2.
250 definition injectRl ≝ λsig.λM1.λM2.λR.
252 inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
253 inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
254 ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
255 ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
258 definition injectRr ≝ λsig.λM1.λM2.λR.
260 inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
261 inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
262 ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
263 ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
266 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
267 ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
268 cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
269 cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
271 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
273 definition lift_confL ≝
274 λsig,M1,M2,c.match c with
275 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
276 definition lift_confR ≝
277 λsig,M1,M2,c.match c with
278 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
280 definition halt_liftL ≝
281 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
283 [ inl s1 ⇒ halt sig M1 s1
284 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
286 definition halt_liftR ≝
287 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
290 | inr s2 ⇒ halt sig M2 s2 ].
292 lemma p_halt_liftL : ∀sig,M1,M2,c.
293 halt sig M1 (cstate … c) =
294 halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
295 #sig #M1 #M2 #c cases c #s #t %
298 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
299 halt ? M1 s = false →
300 trans sig M1 〈s,a〉 = 〈news,move〉 →
301 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
302 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
303 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
308 cstate sig M c1 = cstate sig M c2 →
309 ctape sig M c1 = ctape sig M c2 → c1 = c2.
310 #sig #M1 * #s1 #t1 * #s2 #t2 //
313 lemma step_lift_confL : ∀sig,M1,M2,c0.
314 halt ? M1 (cstate ?? c0) = false →
315 step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
316 lift_confL sig M1 M2 (step sig M1 c0).
317 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
319 whd in ⊢ (???(????%));whd in ⊢ (???%);
320 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
321 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
322 #s0 #m0 #Heq whd in ⊢ (???%);
323 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
328 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
329 loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
330 loop ? k (step sig (seq sig M1 M2))
331 (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
332 Some ? (lift_confL … c2).
333 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
335 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
336 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
337 lapply (refl ? (halt ?? (cstate sig M1 c0)))
338 cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
339 [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
340 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
342 | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
343 [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
350 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
351 loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
352 loop ? k (step sig (seq sig M1 M2))
353 (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
354 Some ? (lift_confR … c2).
355 #sig #k #M1 #M2 #c1 #c2
357 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
358 |#k0 #IH whd in ⊢ (??%? → ??%?);
359 lapply (refl ? (halt ?? (cstate sig M2 c1)))
360 cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
361 [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
362 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
364 | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
365 [whd in ⊢ (??%? → ??%?); #Hc2 <IH
366 [@eq_f (* @step_lift_confR // *)
372 ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
373 #A #k #f #p #a #b elim k
374 [normalize #Hfalse destruct
375 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
376 [ normalize #H1 destruct
378 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
380 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
382 #Hhalt whd in ⊢ (??%?); >Hhalt %
385 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
386 ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
387 #sig #M1 #M2 #outc cases outc #s #t %
390 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
391 ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
392 #sig #M1 #M2 #outc cases outc #s #t %
395 theorem sem_seq: ∀sig,M1,M2,R1,R2.
396 Realize sig M1 R1 → Realize sig M2 R2 →
397 Realize sig (seq sig M1 M2) (R1 ∘ R2).
398 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
399 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
400 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
401 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
403 [@(loop_split ??????????? (loop_liftL … Hloop1))
405 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
406 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
407 ||4:cases outc1 #s1 #t1 %
408 |5:@(loop_liftR … Hloop2)
409 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
410 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
411 >(trans_liftL_true sig M1 M2 ??)
412 [ whd in ⊢ (??%?); whd in ⊢ (???%);
414 | @(loop_Some ?????? Hloop10) ]
416 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
421 (* boolean machines: machines with two distinguished halting states *)
426 definition empty_tapes ≝ λsig.λn.
427 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
428 elim n // normalize //
431 definition init ≝ λsig.λM:TM sig.λi:(list sig).
434 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
437 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
438 halt sig M (state sig M c).
440 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
443 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
446 (* Compute ? M f states that f is computed by M *)
447 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
449 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
452 (* for decision problems, we accept a string if on termination
453 output is not empty *)
455 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
457 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
458 (isnilb ? (out ?? c) = false).
460 (* alternative approach.
461 We define the notion of computation. The notion must be constructive,
462 since we want to define functions over it, like lenght and size
464 Perche' serve Type[2] se sposto a e b a destra? *)
466 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
467 mk_move: p a = false → b = f a → cmove A f p a b.
469 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
470 | empty : ∀a. cstar A M a a
471 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
473 definition computation ≝ λsig.λM:TM sig.
474 cstar ? (cmove ? (step sig M) (stop sig M)).
476 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
477 ∀l.∃c.computation sig M (init sig M l) c →
478 (stop sig M c = true) ∧ out ?? c = f l.
480 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
481 ∀l.∃c.computation sig M (init sig M l) c →
482 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).