]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/turing.ma
Added step machine for universal machine.
[helm.git] / matita / matita / lib / turing / turing.ma
1 (*
2
3 Macchina A:
4 postcondizione
5 PA(in,out) ≝ 
6   ∀ls,cs,d,rs.
7     left (tape in) = cs@'#'::ls → 
8     right (tape in) = d::rs → 
9     state in = q0 → 
10   left (tape out) = ls ∧
11   right (tape out) = d::'#'::rev cs@rs ∧
12   state out = qfinal
13   
14 Macchina A0:
15 postcondizione:
16 PA0(in,out) ≝ 
17   ∀ls,c,rs.
18     left (tape in) = c::ls → 
19     right (tape in) = d::rs → 
20     state in = q0 → 
21   left (tape out) = ls ∧
22   right (tape out) = d::c::rs
23   state out = qfinal
24
25 Macchina A1
26 postcondizione true:
27 PA1t(in,out) ≝ 
28   ∀c,rs.
29     right (tape in) = c::rs → 
30     tape in = tape out ∧
31     (c ≠ '#' → state out = qtrue)
32     
33 postcondizione false:
34 PA1f(in,out) ≝ 
35   ∀c,rs.
36     right (tape in) = c::rs → 
37     tape in = tape out ∧
38     (c = '#' → state out = qfalse) ∧
39
40
41 A = do A0 while A1 inv PA0 var |right (tape in)|;
42
43      posso assumere le precondizioni di A
44      H1 : left (tape in) = c::cs@'#'::ls
45      H2 : right (tape in) = d::rs
46
47      in particolare H2 → precondizioni di A1
48      
49      eseguiamo dunque if A1 then (A0; A) else skip
50      
51   
52           
53 by induction on left (tape in)
54      
55      per casi su d =?= '#'
56      
57      Hcase: d ≠ '#' ⇒ 
58      eseguo (A1; A0; A)
59      devo allora provare che PA1°PA0°PA(in,out) → PA(in,out)
60      ∃s1,s2: PA1t(in,s1) ∧ PA0(s1,s2) ∧ PA(s2,out)
61      
62      usando anche Hcase, ottengo che tape in = tape s1
63      soddisfo allora le precondizioni di PA0(s1,s2) ottenendo che
64      left (tape s2) = cs@'#'::ls
65      right (tape s2) = d::c::rs
66      
67      soddisfo allora le precondizioni di PA e per ipotesi induttiva
68      
69        
70      left (tape s) = d::cs@'#'::ls
71      right (tape s) = 
72      
73     
74
75
76
77
78
79
80 ∀inc.
81   (∃ls,cs,d,rs. left inc = ... ∧ right inc = ... ∧ state inc = q0) → 
82 ∃i,outc. loop i step inc = Some ? outc  
83   ∧(∀ls,cs,d,rs.left inc = ... → right inc = ... →
84     ∧ left outc = ls
85     ∧ right outc = d::"#"::rev cs::rs
86     ∧ state outc = qfinal)
87
88 ϕ1 M1 ψ1 → ϕ2 M2 ψ2 → 
89 (ψ1(in1,out1) → ϕ2(out1)) → (ψ2(out1,out2) → ψ3(in1,out2)) →
90 ϕ1 (M1;M2) ψ3
91
92
93
94 -----------------------------------------------------
95 {} (tmp ≝ x; x ≝ y; y ≝ tmp) {x = old(x), y = old(y)}
96   
97
98 ∀inc.
99   ∀ls:list sig.
100   ∀cs:list (sig\#).
101   ∀d.sig.
102   ∀rs:list sig.
103   left inc = cs@"#"::ls → 
104   right inc = d::rs → 
105   state inc = q0 → 
106 ∃i,outc. loop i step inc = Some outc 
107   ∧
108   (∀ls,cs,d,rs.left inc = ... → right inc = ... →
109   ∧ left outc = ls
110   ∧ right outc = d::"#"::rev cs::rs
111   ∧ state outc = qfinal
112
113 *)
114
115
116 (*
117     ||M||  This file is part of HELM, an Hypertextual, Electronic   
118     ||A||  Library of Mathematics, developed at the Computer Science 
119     ||T||  Department of the University of Bologna, Italy.           
120     ||I||                                                            
121     ||T||  
122     ||A||  
123     \   /  This file is distributed under the terms of the       
124      \ /   GNU General Public License Version 2   
125       V_____________________________________________________________*)
126
127 include "basics/vectors.ma".
128
129 record tape (sig:FinSet): Type[0] ≝ 
130 { left : list sig;
131   right: list sig
132 }.
133
134 inductive move : Type[0] ≝
135 | L : move 
136 | R : move
137 | N : move. 
138
139 (* We do not distinuish an input tape *)
140
141 record TM (sig:FinSet): Type[1] ≝ 
142 { states : FinSet;
143   tapes_no: nat; (* additional working tapes *)
144   trans : states × (Vector (option sig) (S tapes_no)) → 
145     states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
146   output: list sig;
147   start: states;
148   halt : states → bool
149 }.
150
151 record config (sig:FinSet) (M:TM sig): Type[0] ≝
152 { state : states sig M;
153   tapes : Vector (tape sig) (S (tapes_no sig M));
154   out : list sig
155 }.
156
157 definition option_hd ≝ λA.λl:list A.
158   match l with
159   [nil ⇒ None ?
160   |cons a _ ⇒ Some ? a
161   ].
162
163 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
164   match \snd m with
165   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
166   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
167   | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
168   ].
169
170 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
171   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
172
173 definition opt_cons ≝ λA.λa:option A.λl:list A.
174   match a with
175   [ None ⇒ l
176   | Some a ⇒ a::l
177   ].
178
179 definition step ≝ λsig.λM:TM sig.λc:config sig M.
180   let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
181   mk_config ?? 
182     news 
183     (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
184     (opt_cons ? outchar (out ?? c)).
185
186 definition empty_tapes ≝ λsig.λn.
187 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
188 elim n // normalize //
189 qed.
190
191 definition init ≝ λsig.λM:TM sig.λi:(list sig).
192   mk_config ??
193     (start sig M)
194     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
195     [ ].
196
197 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
198   halt sig M (state sig M c).
199
200 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
201   match n with 
202   [ O ⇒ None ?
203   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
204   ].
205
206 (* Compute ? M f states that f is computed by M *)
207 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
208 ∀l.∃i.∃c.
209   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
210   out ?? c = f l.
211
212 (* for decision problems, we accept a string if on termination
213 output is not empty *)
214
215 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
216 ∀l.∃i.∃c.
217   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
218   (isnilb ? (out ?? c) = false).
219
220 (* alternative approach.
221 We define the notion of computation. The notion must be constructive,
222 since we want to define functions over it, like lenght and size 
223
224 Perche' serve Type[2] se sposto a e b a destra? *)
225
226 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
227   mk_move: p a = false → b = f a → cmove A f p a b.
228   
229 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
230 | empty : ∀a. cstar A M a a
231 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
232
233 definition computation ≝ λsig.λM:TM sig.
234   cstar ? (cmove ? (step sig M) (stop sig M)).
235
236 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
237   ∀l.∃c.computation sig M (init sig M l) c → 
238    (stop sig M c = true) ∧ out ?? c = f l.
239
240 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
241   ∀l.∃c.computation sig M (init sig M l) c → 
242    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).