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 "basics/vectors.ma".
13 (* include "basics/relations.ma". *)
15 record tape (sig:FinSet): Type[0] ≝
20 inductive move : Type[0] ≝
25 (* We do not distinuish an input tape *)
27 record TM (sig:FinSet): Type[1] ≝
29 trans : states × (option sig) → states × (option (sig × move));
34 record config (sig:FinSet) (M:TM sig): Type[0] ≝
35 { cstate : states sig M;
39 definition option_hd ≝ λA.λl:list A.
45 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
50 [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
51 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
55 definition step ≝ λsig.λM:TM sig.λc:config sig M.
56 let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
57 let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
58 mk_config ?? news (tape_move sig (ctape ?? c) mv).
60 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
63 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
66 axiom loop_incr : ∀A,f,p,k1,k2,a1,a2.
67 loop A k1 f p a1 = Some ? a2 →
68 loop A (k2+k1) f p a1 = Some ? a2.
70 axiom loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
72 loop A k1 f p a1 = Some ? a2 → f a2 = a3 →
73 loop A k2 f q a3 = Some ? a4 →
74 loop A (k1+k2) f q a1 = Some ? a4.
77 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
79 loop A k1 f p a1 = Some ? a2 →
80 loop A k2 f q a2 = Some ? a3 →
81 loop A (k1+k2) f q a1 = Some ? a3.
82 #Sig #f #p #q #Hpq #k1 elim k1
83 [normalize #k2 #a1 #a2 #a3 #H destruct
84 |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
85 cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
86 [#eqa1a2 destruct #H @loop_incr //
87 |normalize >(Hpq … pa1) normalize
88 #H1 #H2 @(Hind … H2) //
94 definition initc ≝ λsig.λM:TM sig.λt.
95 mk_config sig M (start sig M) t.
97 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
99 loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
104 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
108 if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
110 let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
113 let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
117 definition seq ≝ λsig. λM1,M2 : TM sig.
119 (FinSum (states sig M1) (states sig M2))
120 (seq_trans sig M1 M2)
121 (inl … (start sig M1))
123 [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
125 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
126 ∃am.R1 a1 am ∧ R2 am a2.
129 definition injectRl ≝ λsig.λM1.λM2.λR.
131 inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
132 inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
133 ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
134 ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
137 definition injectRr ≝ λsig.λM1.λM2.λR.
139 inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
140 inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
141 ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
142 ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
145 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
146 ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
147 cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
148 cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
150 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
152 definition lift_confL ≝
153 λsig,M1,M2,c.match c with
154 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
155 definition lift_confR ≝
156 λsig,M1,M2,c.match c with
157 [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
159 definition halt_liftL ≝
160 λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
162 [ inl s1 ⇒ halt sig M1 s1
163 | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
165 axiom loop_dec : ∀A,k1,k2,f,p,q,a1,a2,a3.
166 loop A k1 f p a1 = Some ? a2 →
167 loop A k2 f q a2 = Some ? a3 →
168 loop A (k1+k2) f q a1 = Some ? a3.
170 lemma p_halt_liftL : ∀sig,M1,M2,c.
171 halt sig M1 (cstate … c) =
172 halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
173 #sig #M1 #M2 #c cases c #s #t %
176 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
177 halt ? M1 s = false →
178 trans sig M1 〈s,a〉 = 〈news,move〉 →
179 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
180 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
181 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
186 cstate sig M c1 = cstate sig M c2 →
187 ctape sig M c1 = ctape sig M c2 → c1 = c2.
188 #sig #M1 * #s1 #t1 * #s2 #t2 //
191 lemma step_lift_confL : ∀sig,M1,M2,c0.
192 halt ? M1 (cstate ?? c0) = false →
193 step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
194 lift_confL sig M1 M2 (step sig M1 c0).
195 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
197 whd in ⊢ (???(????%));whd in ⊢ (???%);
198 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
199 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
200 #s0 #m0 #Heq whd in ⊢ (???%);
201 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
206 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
207 loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
208 loop ? k (step sig (seq sig M1 M2))
209 (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
210 Some ? (lift_confL … c2).
211 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
213 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
214 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
215 lapply (refl ? (halt ?? (cstate sig M1 c0)))
216 cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
217 [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
218 [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
220 | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
221 [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
226 axiom loop_liftR : ∀sig,k,M1,M2,c1,c2.
227 loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
228 loop ? k (step sig (seq sig M1 M2))
229 (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
230 Some ? (lift_confR … c2).
233 ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
235 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
237 trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
239 #Hhalt whd in ⊢ (??%?); >Hhalt %
242 theorem sem_seq: ∀sig,M1,M2,R1,R2.
243 Realize sig M1 R1 → Realize sig M2 R2 →
244 Realize sig (seq sig M1 M2) (R1 ∘ R2).
245 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
246 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
247 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
248 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
250 [@(loop_split ??????????? (loop_liftL … Hloop1))
252 [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
253 | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
255 |4:@(loop_liftR … Hloop2)
256 |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
257 generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
258 >(trans_liftL_true sig M1 M2 ??)
259 [ whd in ⊢ (??%?); whd in ⊢ (???%);
261 | @(loop_Some ?????? Hloop10) ]
266 definition empty_tapes ≝ λsig.λn.
267 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
268 elim n // normalize //
271 definition init ≝ λsig.λM:TM sig.λi:(list sig).
274 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
277 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
278 halt sig M (state sig M c).
280 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
283 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
286 (* Compute ? M f states that f is computed by M *)
287 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
289 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
292 (* for decision problems, we accept a string if on termination
293 output is not empty *)
295 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
297 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
298 (isnilb ? (out ?? c) = false).
300 (* alternative approach.
301 We define the notion of computation. The notion must be constructive,
302 since we want to define functions over it, like lenght and size
304 Perche' serve Type[2] se sposto a e b a destra? *)
306 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
307 mk_move: p a = false → b = f a → cmove A f p a b.
309 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
310 | empty : ∀a. cstar A M a a
311 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
313 definition computation ≝ λsig.λM:TM sig.
314 cstar ? (cmove ? (step sig M) (stop sig M)).
316 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
317 ∀l.∃c.computation sig M (init sig M l) c →
318 (stop sig M c = true) ∧ out ?? c = f l.
320 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
321 ∀l.∃c.computation sig M (init sig M l) c →
322 (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).