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 axiom daemon : ∀X:Prop.X.
46 theorem sem_if: ∀sig,M1,M2,M3,Rtrue,Rfalse,R2,R3,acc.
47 accRealize sig M1 acc Rtrue Rfalse → Realize sig M2 R2 → Realize sig M3 R3 →
48 Realize sig (ifTM sig M1 M2 M3 acc) (λt1,t2. (Rtrue ∘ R2) t1 t2 ∨ (Rfalse ∘ R3) t1 t2).
49 #sig #M1 #M2 #M3 #Rtrue #Rfalse #R2 #R3 #acc #HaccR #HR2 #HR3 #t
50 cases (HaccR t) #k1 * #outc1 * * #Hloop1 #HMtrue #HMfalse
51 cases (true_or_false (cstate ?? outc1 == acc)) #Hacc
52 [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
53 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
55 [@(loop_split ???????????
57 (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
58 (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
59 (λc.halt sig M1 (cstate … c))
60 (λc.halt_liftL ?? (halt sig M1) (cstate … c))
63 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
64 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
65 || #c0 #Hhalt @daemon (* <step_lift_confL // *)
67 |6:cases outc1 #s1 #t1 %
68 |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
70 | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
71 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
72 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
73 >(trans_liftL_true sig M1 M2 ??)
74 [ whd in ⊢ (??%?); whd in ⊢ (???%);
75 @config_eq whd in ⊢ (???%); //
76 | @(loop_Some ?????? Hloop10) ]
77 ||4:cases outc1 #s1 #t1 %
80 @(loop_liftR … Hloop2)
81 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
82 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
83 >(trans_liftL_true sig M1 M2 ??)
84 [ whd in ⊢ (??%?); whd in ⊢ (???%);
86 | @(loop_Some ?????? Hloop10) ]
88 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
92 (* We do not distinuish an input tape *)
94 record TM (sig:FinSet): Type[1] ≝
96 trans : states × (option sig) → states × (option (sig × move));
101 record config (sig:FinSet) (M:TM sig): Type[0] ≝
102 { cstate : states sig M;
106 definition option_hd ≝ λA.λl:list A.
112 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
117 [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
118 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
122 definition step ≝ λsig.λM:TM sig.λc:config sig M.
123 let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
124 let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
125 mk_config ?? news (tape_move sig (ctape ?? c) mv).
127 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
130 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
133 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
134 loop A k1 f p a1 = Some ? a2 →
135 loop A (k2+k1) f p a1 = Some ? a2.
136 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
137 [normalize #a0 #Hfalse destruct
138 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
139 cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
143 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
145 loop A k1 f p a1 = Some ? a2 →
146 f a2 = a3 → q a2 = false →
147 loop A k2 f q a3 = Some ? a4 →
148 loop A (k1+k2) f q a1 = Some ? a4.
149 #Sig #f #p #q #Hpq #k1 elim k1
150 [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
151 |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
152 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
153 [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
154 whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
155 whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
156 |normalize >(Hpq … pa1) normalize
157 #H1 #H2 #H3 @(Hind … H2) //
163 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
165 loop A k1 f p a1 = Some ? a2 →
166 loop A k2 f q a2 = Some ? a3 →
167 loop A (k1+k2) f q a1 = Some ? a3.
168 #Sig #f #p #q #Hpq #k1 elim k1
169 [normalize #k2 #a1 #a2 #a3 #H destruct
170 |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
171 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
172 [#eqa1a2 destruct #H @loop_incr //
173 |normalize >(Hpq … pa1) normalize
174 #H1 #H2 @(Hind … H2) //
180 definition initc ≝ λsig.λM:TM sig.λt.
181 mk_config sig M (start sig M) t.
183 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
185 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
190 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
194 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
196 let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
199 let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
203 definition seq ≝ λsig. λM1,M2 : TM sig.
205 (FinSum (states sig M1) (states sig M2))
206 (seq_trans sig M1 M2)
207 (inl … (start sig M1))
209 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
211 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
212 ∃am.R1 a1 am ∧ R2 am a2.
215 definition injectRl ≝ λsig.λM1.λM2.λR.
217 inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
218 inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
219 ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
220 ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
223 definition injectRr ≝ λsig.λM1.λM2.λR.
225 inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
226 inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
227 ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
228 ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
231 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
232 ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
233 cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
234 cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
236 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
238 definition lift_confL ≝
239 λsig,M1,M2,c.match c with
240 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
241 definition lift_confR ≝
242 λsig,M1,M2,c.match c with
243 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
245 definition halt_liftL ≝
246 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
248 [ inl s1 ⇒ halt sig M1 s1
249 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
251 definition halt_liftR ≝
252 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
255 | inr s2 ⇒ halt sig M2 s2 ].
257 lemma p_halt_liftL : ∀sig,M1,M2,c.
258 halt sig M1 (cstate … c) =
259 halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
260 #sig #M1 #M2 #c cases c #s #t %
263 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
264 halt ? M1 s = false →
265 trans sig M1 〈s,a〉 = 〈news,move〉 →
266 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
267 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
268 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
273 cstate sig M c1 = cstate sig M c2 →
274 ctape sig M c1 = ctape sig M c2 → c1 = c2.
275 #sig #M1 * #s1 #t1 * #s2 #t2 //
278 lemma step_lift_confL : ∀sig,M1,M2,c0.
279 halt ? M1 (cstate ?? c0) = false →
280 step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
281 lift_confL sig M1 M2 (step sig M1 c0).
282 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
284 whd in ⊢ (???(????%));whd in ⊢ (???%);
285 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
286 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
287 #s0 #m0 #Heq whd in ⊢ (???%);
288 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
293 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
294 loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
295 loop ? k (step sig (seq sig M1 M2))
296 (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
297 Some ? (lift_confL … c2).
298 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
300 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
301 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
302 lapply (refl ? (halt ?? (cstate sig M1 c0)))
303 cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
304 [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
305 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
307 | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
308 [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
315 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
316 loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
317 loop ? k (step sig (seq sig M1 M2))
318 (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
319 Some ? (lift_confR … c2).
320 #sig #k #M1 #M2 #c1 #c2
322 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
323 |#k0 #IH whd in ⊢ (??%? → ??%?);
324 lapply (refl ? (halt ?? (cstate sig M2 c1)))
325 cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
326 [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
327 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
329 | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
330 [whd in ⊢ (??%? → ??%?); #Hc2 <IH
331 [@eq_f (* @step_lift_confR // *)
337 ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
338 #A #k #f #p #a #b elim k
339 [normalize #Hfalse destruct
340 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
341 [ normalize #H1 destruct
343 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
345 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
347 #Hhalt whd in ⊢ (??%?); >Hhalt %
350 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
351 ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
352 #sig #M1 #M2 #outc cases outc #s #t %
355 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
356 ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
357 #sig #M1 #M2 #outc cases outc #s #t %
360 theorem sem_seq: ∀sig,M1,M2,R1,R2.
361 Realize sig M1 R1 → Realize sig M2 R2 →
362 Realize sig (seq sig M1 M2) (R1 ∘ R2).
363 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
364 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
365 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
366 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
368 [@(loop_split ??????????? (loop_liftL … Hloop1))
370 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
371 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
372 ||4:cases outc1 #s1 #t1 %
373 |5:@(loop_liftR … Hloop2)
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 ⊢ (???%);
379 | @(loop_Some ?????? Hloop10) ]
381 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
386 (* boolean machines: machines with two distinguished halting states *)
391 definition empty_tapes ≝ λsig.λn.
392 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
393 elim n // normalize //
396 definition init ≝ λsig.λM:TM sig.λi:(list sig).
399 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
402 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
403 halt sig M (state sig M c).
405 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
408 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
411 (* Compute ? M f states that f is computed by M *)
412 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
414 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
417 (* for decision problems, we accept a string if on termination
418 output is not empty *)
420 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
422 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
423 (isnilb ? (out ?? c) = false).
425 (* alternative approach.
426 We define the notion of computation. The notion must be constructive,
427 since we want to define functions over it, like lenght and size
429 Perche' serve Type[2] se sposto a e b a destra? *)
431 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
432 mk_move: p a = false → b = f a → cmove A f p a b.
434 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
435 | empty : ∀a. cstar A M a a
436 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
438 definition computation ≝ λsig.λM:TM sig.
439 cstar ? (cmove ? (step sig M) (stop sig M)).
441 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
442 ∀l.∃c.computation sig M (init sig M l) c →
443 (stop sig M c = true) ∧ out ?? c = f l.
445 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
446 ∀l.∃c.computation sig M (init sig M l) c →
447 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).