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".
14 definition if_trans ≝ λsig. λM1,M2,M3 : TM sig. λq:states sig M1.
18 if halt sig M1 s1 then
19 if s1==q then 〈inr … (inl … (start sig M2)), None ?〉
20 else 〈inr … (inr … (start sig M3)), None ?〉
21 else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
25 [ inl s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
26 〈inr … (inl … news2),m〉
27 | inr s3 ⇒ let 〈news3,m〉 ≝ trans sig M3 〈s3,a〉 in
28 〈inr … (inr … news3),m〉
32 definition ifTM ≝ λsig. λcondM,thenM,elseM : TM sig.
33 λqacc: states sig condM.
35 (FinSum (states sig condM) (FinSum (states sig thenM) (states sig elseM)))
36 (if_trans sig condM thenM elseM qacc)
37 (inl … (start sig condM))
40 | inr s' ⇒ match s' with
41 [ inl s2 ⇒ halt sig thenM s2
42 | inr s3 ⇒ halt sig elseM s3 ]]).
44 theorem sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
45 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
46 Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
47 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
48 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
49 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
50 [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
51 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
53 [@(loop_split ??????????? (loop_liftL … Hloop1))
55 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
56 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
57 ||4:cases outc1 #s1 #t1 %
58 |5:@(loop_liftR … Hloop2)
59 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
60 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
61 >(trans_liftL_true sig M1 M2 ??)
62 [ whd in ⊢ (??%?); whd in ⊢ (???%);
64 | @(loop_Some ?????? Hloop10) ]
66 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
70 (* We do not distinuish an input tape *)
72 record TM (sig:FinSet): Type[1] ≝
74 trans : states × (option sig) → states × (option (sig × move));
79 record config (sig:FinSet) (M:TM sig): Type[0] ≝
80 { cstate : states sig M;
84 definition option_hd ≝ λA.λl:list A.
90 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
95 [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
96 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
100 definition step ≝ λsig.λM:TM sig.λc:config sig M.
101 let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
102 let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
103 mk_config ?? news (tape_move sig (ctape ?? c) mv).
105 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
108 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
111 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
112 loop A k1 f p a1 = Some ? a2 →
113 loop A (k2+k1) f p a1 = Some ? a2.
114 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
115 [normalize #a0 #Hfalse destruct
116 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
117 cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
121 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
123 loop A k1 f p a1 = Some ? a2 →
124 f a2 = a3 → q a2 = false →
125 loop A k2 f q a3 = Some ? a4 →
126 loop A (k1+k2) f q a1 = Some ? a4.
127 #Sig #f #p #q #Hpq #k1 elim k1
128 [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
129 |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
130 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
131 [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
132 whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
133 whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
134 |normalize >(Hpq … pa1) normalize
135 #H1 #H2 #H3 @(Hind … H2) //
141 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
143 loop A k1 f p a1 = Some ? a2 →
144 loop A k2 f q a2 = Some ? a3 →
145 loop A (k1+k2) f q a1 = Some ? a3.
146 #Sig #f #p #q #Hpq #k1 elim k1
147 [normalize #k2 #a1 #a2 #a3 #H destruct
148 |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
149 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
150 [#eqa1a2 destruct #H @loop_incr //
151 |normalize >(Hpq … pa1) normalize
152 #H1 #H2 @(Hind … H2) //
158 definition initc ≝ λsig.λM:TM sig.λt.
159 mk_config sig M (start sig M) t.
161 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
163 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
168 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
172 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
174 let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
177 let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
181 definition seq ≝ λsig. λM1,M2 : TM sig.
183 (FinSum (states sig M1) (states sig M2))
184 (seq_trans sig M1 M2)
185 (inl … (start sig M1))
187 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
189 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
190 ∃am.R1 a1 am ∧ R2 am a2.
193 definition injectRl ≝ λsig.λM1.λM2.λR.
195 inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
196 inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
197 ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
198 ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
201 definition injectRr ≝ λsig.λM1.λM2.λR.
203 inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
204 inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
205 ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
206 ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
209 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
210 ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
211 cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
212 cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
214 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
216 definition lift_confL ≝
217 λsig,M1,M2,c.match c with
218 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
219 definition lift_confR ≝
220 λsig,M1,M2,c.match c with
221 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
223 definition halt_liftL ≝
224 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
226 [ inl s1 ⇒ halt sig M1 s1
227 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
229 definition halt_liftR ≝
230 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
233 | inr s2 ⇒ halt sig M2 s2 ].
235 lemma p_halt_liftL : ∀sig,M1,M2,c.
236 halt sig M1 (cstate … c) =
237 halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
238 #sig #M1 #M2 #c cases c #s #t %
241 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
242 halt ? M1 s = false →
243 trans sig M1 〈s,a〉 = 〈news,move〉 →
244 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
245 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
246 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
251 cstate sig M c1 = cstate sig M c2 →
252 ctape sig M c1 = ctape sig M c2 → c1 = c2.
253 #sig #M1 * #s1 #t1 * #s2 #t2 //
256 lemma step_lift_confL : ∀sig,M1,M2,c0.
257 halt ? M1 (cstate ?? c0) = false →
258 step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
259 lift_confL sig M1 M2 (step sig M1 c0).
260 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
262 whd in ⊢ (???(????%));whd in ⊢ (???%);
263 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
264 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
265 #s0 #m0 #Heq whd in ⊢ (???%);
266 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
271 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
272 loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
273 loop ? k (step sig (seq sig M1 M2))
274 (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
275 Some ? (lift_confL … c2).
276 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
278 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
279 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
280 lapply (refl ? (halt ?? (cstate sig M1 c0)))
281 cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
282 [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
283 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
285 | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
286 [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
293 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
294 loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
295 loop ? k (step sig (seq sig M1 M2))
296 (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
297 Some ? (lift_confR … c2).
298 #sig #k #M1 #M2 #c1 #c2
300 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
301 |#k0 #IH whd in ⊢ (??%? → ??%?);
302 lapply (refl ? (halt ?? (cstate sig M2 c1)))
303 cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
304 [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
305 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
307 | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
308 [whd in ⊢ (??%? → ??%?); #Hc2 <IH
309 [@eq_f (* @step_lift_confR // *)
315 ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
316 #A #k #f #p #a #b elim k
317 [normalize #Hfalse destruct
318 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
319 [ normalize #H1 destruct
321 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
323 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
325 #Hhalt whd in ⊢ (??%?); >Hhalt %
328 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
329 ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
330 #sig #M1 #M2 #outc cases outc #s #t %
333 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
334 ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
335 #sig #M1 #M2 #outc cases outc #s #t %
338 theorem sem_seq: ∀sig,M1,M2,R1,R2.
339 Realize sig M1 R1 → Realize sig M2 R2 →
340 Realize sig (seq sig M1 M2) (R1 ∘ R2).
341 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
342 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
343 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
344 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
346 [@(loop_split ??????????? (loop_liftL … Hloop1))
348 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
349 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
350 ||4:cases outc1 #s1 #t1 %
351 |5:@(loop_liftR … Hloop2)
352 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
353 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
354 >(trans_liftL_true sig M1 M2 ??)
355 [ whd in ⊢ (??%?); whd in ⊢ (???%);
357 | @(loop_Some ?????? Hloop10) ]
359 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
364 (* boolean machines: machines with two distinguished halting states *)
369 definition empty_tapes ≝ λsig.λn.
370 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
371 elim n // normalize //
374 definition init ≝ λsig.λM:TM sig.λi:(list sig).
377 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
380 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
381 halt sig M (state sig M c).
383 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
386 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
389 (* Compute ? M f states that f is computed by M *)
390 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
392 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
395 (* for decision problems, we accept a string if on termination
396 output is not empty *)
398 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
400 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
401 (isnilb ? (out ?? c) = false).
403 (* alternative approach.
404 We define the notion of computation. The notion must be constructive,
405 since we want to define functions over it, like lenght and size
407 Perche' serve Type[2] se sposto a e b a destra? *)
409 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
410 mk_move: p a = false → b = f a → cmove A f p a b.
412 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
413 | empty : ∀a. cstar A M a a
414 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
416 definition computation ≝ λsig.λM:TM sig.
417 cstar ? (cmove ? (step sig M) (stop sig M)).
419 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
420 ∀l.∃c.computation sig M (init sig M l) c →
421 (stop sig M c = true) ∧ out ?? c = f l.
423 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
424 ∀l.∃c.computation sig M (init sig M l) c →
425 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).