]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/universal.ma
Progress in semantics of the copy machine.
[helm.git] / matita / matita / lib / turing / universal.ma
1 include "turing/turing.ma".
2
3 (* 
4 Simboli:
5 0 1 *0 *1 # | ,
6
7 [lista di simboli] fa match su un simbolo qualunque nella lista
8 ad esempio [#|,] fa match con la gratella "#", la barra verticale "|" e la virgola ","
9
10 Convenzione variabili:
11 - x,y,z,D     = bit (non marcati)
12 - *x,*y,*z,*D = bit marcati
13 - c,d,e = caratteri (bit marcati e non marcati e separatori)
14
15 Convenzioni mosse:
16 c/D --> Q : leggo c, scrivo c, mi sposto a D e passo allo stato Q
17 c/d/D --> Q : leggo c, scrivo d, mi sposto a D e passo allo stato Q
18
19 MACCHINA per confronto tuple:
20 =============================
21 Input:
22       *               *
23  ls # current # ... | input , output , D | ... # rs
24     ^
25     0
26
27 Output:
28
29  ls # current # ... | input , output , D | ... # rs  (rimuove le marcature e si sposta sull'output)
30                               ^
31                            SUCCESS
32
33       *                                    *
34  ls # current # ... | input , output , D | ... # rs (sposta la marcatura alla tupla successiva)
35     ^
36  FAILURE
37
38 STATO 0:
39   #/R --> 1
40   
41 STATO 1:
42   \forall c != *z. c/L --> 1
43   \forall x. *x/x/R --> 2(x)
44
45 STATO 2(x):
46   \forall y. y/*y/R --> 3(x)
47   #/R --> 3(x)
48
49 STATO 3(x):
50   \forall y.\forall c != *y. c/R --> 3(x)
51   *x/x/R --> 4
52   *~x/~x/R --> 5
53
54 STATO 4:
55   \forall x. x/*x/L --> 1
56   ,/R --> SUCCESS
57   
58 STATO 5:
59   \forall c != |. c/R --> 5
60   |/R --> 6
61
62 STATO 6:
63   \forall x. x/*x/L --> 7
64
65 STATO 7:
66   \forall c != #. c/L --> 7
67   #/L -→ 8
68
69 STATO 8:
70   \forall c != #. c/L --> 8
71   \forall x. *x/x/L --> 8
72   #/R --> 9
73
74 STATO 9:
75   \forall x. x/*x/L --> FAILURE
76
77 *)
78
79 inductive alpha_uni : Type[0] ≝ 
80 | bit : bool → alpha_uni
81 | mark : bool → alpha_uni
82 | grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
83
84 inductive Qmatch : Type[0] ≝
85 | qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
86 | qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch 
87 | qm8 : Qmatch | qm9 : Qmatch 
88 | qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
89
90 definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
91
92 definition tmatch ≝ λs,c.
93 match s with
94 [ qm0 ⇒ match c with
95   [ grid ⇒ 〈qm1,〈grid,R〉〉
96   | _ ⇒ 〈qmsink,〈c,N〉〉 ]
97 | qm1 ⇒ match c with
98   [ mark x ⇒ 〈qm2 x,〈bit x,R〉〉
99   | _ ⇒ 〈qm1,〈c,L〉〉 ]
100 | qm2 x ⇒ match c with
101   [ bit y ⇒ 〈qm3 x,〈mark y,R〉〉
102   | grid ⇒ 〈qm3 x,〈grid,R〉〉
103   | _ ⇒ 〈qmsink,〈c,N〉〉 ]
104 | qm3 x ⇒ match c with
105   [ mark y ⇒ match bool_eqb x y with
106     [ true ⇒ 〈qm4,〈bit y,R〉〉
107     | false ⇒ 〈qm5,〈bit y,R〉〉 ]
108   | _ ⇒ 〈qm3 x,〈c,R〉〉 ]
109 | qm4 ⇒ match c with
110   [ comma ⇒ 〈qmsuccess,〈comma,R〉〉
111   | bit x ⇒ 〈qm1,〈mark x,L〉〉
112   | _ ⇒ 〈qmsink,〈c,N〉〉 ]
113 | qm5 ⇒ match c with
114   [ bar ⇒ 〈qm6,〈bar,R〉〉
115   | _ ⇒ 〈qm5,〈c,R〉〉 ]
116 | qm6 ⇒ match c with 
117   [ bit x ⇒ 〈qm7,〈mark x,L〉〉
118   | _ ⇒ 〈qmsink,〈c,N〉〉 ]
119 | qm7 ⇒ match c with
120   [ grid ⇒ 〈qm8,〈grid,L〉〉
121   | _ ⇒ 〈qm7,〈c,L〉〉 ]
122 | qm8 ⇒ match c with
123   [ grid ⇒ 〈qm9,〈grid,R〉〉 
124   | mark x ⇒ 〈qm8,〈bit x,L〉〉 
125   | _ ⇒ 〈qm8,〈c,L〉〉 ]
126 | qm9 ⇒ match c with
127   [ bit x ⇒ 〈qmfailure,〈mark x,L〉〉 
128   | _ ⇒ 〈qmsink,〈c,N〉〉 ]
129 | qmsink ⇒ 〈qmsink,〈c,N〉〉 
130 | qmsuccess ⇒ 〈qmsuccess,〈c,N〉〉
131 | qmfailure ⇒ 〈qmfailure,〈c,N〉〉].
132
133   
134 (*
135 ==============================
136 MACCHINA PER COPIA NUOVO STATO IN CURRENT
137 ==============================
138
139 Input:
140   
141   ls # current # ... | in_state , out_state , D | ... # rs
142                                   ^
143                                   0
144
145 Output:
146   ls # out_state # ... | in_state , out_state , D | ... # rs
147                                               ^
148                                               9
149
150 STATO 0:
151   \forall x. x/*x/L --> 1
152   
153 STATO 1:
154   [01,|]/L --> 1
155   #/L --> 2
156
157 STATO 2:
158   [01]/L --> 2
159   #/R -> 3
160
161 STATO 3:
162   \forall x. x/*x/R --> 4
163   #/R --> 8
164
165 STATO 4:
166   [01,|#]/R --> 4
167   \forall x. *x/x/R --> 5(x)
168
169 STATO 5(x):
170   #/R --> 6(x)
171   \forall y. y/*y/L --> 7(x)
172
173 STATO 6(x):
174   \forall D. D/*D/L --> 7(x)
175
176 STATO 7(x):
177   [01,|#]/l --> 7(x)
178   \forall y. *y/x/R --> 3
179
180 STATO 8:
181   [01,|#]/R --> 8
182   \forall D. *D/D/L --> 9
183
184 STATO 9:
185   stato finale
186 *)
187 match s with
188  [ q0 ⇒ match c with
189    [ bit x ⇒ 〈q1,〈mark x,L〉〉
190    | _ ⇒ 〈qsink,〈c,N〉〉 ]
191  | q1 ⇒ match c with
192    [ bit x ⇒ 〈q1,〈c,L〉〉
193    | comma ⇒ 〈q1,〈c,L〉〉
194    | bar ⇒ 〈q1,〈c,L〉〉
195    | grid ⇒ 〈q2,〈c,R〉〉
196    | _ ⇒ 〈qsink,〈c,N〉〉 ]
197  | q2 ⇒ match c with
198    [ bit x ⇒ 〈q2,〈c,L〉〉
199    | grid ⇒ 〈q3,〈c,R〉〉 
200    | _ ⇒ 〈qsink,〈c,N〉〉 ]
201  | q3 ⇒ match c with
202    [ bit x ⇒ 〈q4,〈mark x,R〉〉
203    | grid ⇒ 〈q8,〈c,R〉〉
204    | _ ⇒ 〈qsink,〈c,N〉〉 ]
205  | q4 ⇒ match c with
206    [ bit x ⇒ 〈q4,〈c,R〉〉
207    | comma ⇒ 〈q4,〈c,R〉〉
208    | bar ⇒ 〈q4,〈c,R〉〉
209    | grid ⇒ 〈q4,〈c,R〉〉
210    | mark x ⇒ 〈q5 x,〈bit x,R〉〉 ]
211  | q5 x ⇒ match c with
212    [ grid ⇒ 〈q6 x,〈c,R〉〉
213    | bit y ⇒ 〈q7 x,〈mark y,L〉〉
214    | _ ⇒ 〈qsink,〈c,N〉〉 ]
215  | q6 x ⇒ match c with
216    [ bit D ⇒ 〈q7 x,〈mark D,L〉〉
217    | _ ⇒ 〈qsink,〈c,N〉〉 ]
218  | q7 x ⇒ match c with
219    [ bit y ⇒ 〈q7 x,〈c,L〉〉
220    | comma ⇒ 〈q7 x,〈c,L〉〉
221    | bar ⇒ 〈q7 x,〈c,L〉〉
222    | grid ⇒ 〈q7 x,〈c,L〉〉
223    | mark y ⇒ 〈q3,〈bit x,R〉〉 ]
224  | q8 ⇒ match c with
225    [ bit y ⇒ 〈q8,〈c,R〉〉
226    | comma ⇒ 〈q8,〈c,R〉〉
227    | bar ⇒ 〈q8,〈c,R〉〉
228    | grid ⇒ 〈q8,〈c,R〉〉
229    | mark D ⇒ 〈q9,〈bit D,L〉〉 ]
230  | q9 ⇒ ? (* successo *)
231  ].
232
233 (*
234 ==================================
235 MACCHINE PER SPOSTARE LA "TESTINA"
236 ================================
237
238 Lo spostamento a sx si ottiene mediante
239
240 ls x # current y # macchina # rs
241 ----C--->
242 ls x # current # y macchina # rs
243 ----B--->
244 ls x # current # macchina # y rs
245 ----B--->
246 ls # x current # macchina # y rs
247 ----C--->
248 ls # current x # macchina # y rs
249
250
251 Lo spostamento a dx si ottiene mediante
252
253 ls # current x # macchina # y rs
254 ----A--->
255 ls x # current # macchina # y rs
256 ----A--->
257 ls x # current # macchina y # rs
258 ----A--->
259 ls x # current y # macchina # rs
260
261
262 MACCHINA A
263 ----------
264 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
265
266 Input:
267   
268   ls # cs x rs
269           ^
270           0
271
272 Output:
273   ls x # cs rs
274      ^
275      4
276
277 STATO 0:
278   \forall x.x/L --> 1(x)
279
280 STATO 1(x):
281   \forall c != #. c/x/R --> 2(c)
282   #/x/R --> 3
283
284 STATO 2(c):
285   \forall d. d/c/L --> 0
286
287 STATO 3:
288   \forall c. c/#/L --> 4
289
290 STATO 4:
291   stato finale
292 *)
293
294 match s with
295  [ q0 ⇒ match c with
296    [ bit x ⇒ 〈q1 x,〈c,L〉〉
297    | _ ⇒ 〈qsink,〈c,N〉〉 ]
298  | q1 x ⇒ match c with
299    [ grid ⇒ 〈q3,〈bit x,R〉〉
300    | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
301  | q2 d ⇒ 〈q0,〈d,L〉〉
302  | q3 ⇒ 〈q4,〈grid,L〉〉
303  | q4 ⇒ (* finale *) ].
304
305 (*
306 MACCHINA B
307 ----------
308 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
309
310 Input:
311
312   ls x cs # rs
313      ^
314      0
315
316 Output:
317   ls cs # x rs
318           ^
319           4
320
321 STATO 0:
322   \forall x.x/R --> 1(x)
323
324 STATO 1(x):
325   \forall c != #. c/x/L --> 2(c)
326   #/x/L --> 3
327
328 STATO 2(c):
329   \forall d. d/c/R --> 0
330
331 STATO 3:
332   \forall c. c/#/L --> 4
333
334 STATO 4:
335   stato finale
336 *)
337
338 match s with
339 [ q0 ⇒ match c with
340   [ bit x ⇒ 〈q1 x,〈c,R〉〉
341   | _ ⇒ 〈qsink,〈c,N〉〉]
342 | q1 x ⇒ match c with
343   [ grid ⇒ 〈q3,〈bit x,L〉〉
344   | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
345 | q2 d ⇒ 〈q0,〈d,R〉〉
346 | q3 ⇒ 〈q4,〈grid,L〉〉 
347 | q4 ⇒ (* finale *) ].
348
349 (*
350 MACCHINA C
351 ----------
352 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
353
354 Input:
355   ls x cs # rs
356      ^
357      0
358
359 Output:
360   ls cs x # rs
361         ^
362         3
363
364 STATO 0:
365   \forall x. x/R --> 1(x)
366
367 STATO 1(x):
368   \forall c != #. c/x/L --> 2(c)
369   #/#/L --> 3
370
371 STATO 2(c):
372   \forall d. d/c/R --> 0
373
374 STATO 3:
375   stato finale
376
377 *)
378
379 match s with 
380 [ q0 ⇒ match c with
381   [ bit x ⇒ 〈q1 x,〈c,R〉〉
382   | _ ⇒ 〈qsink,〈c,N〉〉 ]
383 | q1 x ⇒ match c with
384   [ grid ⇒ 〈q3,〈grid,L〉〉
385   | _ ⇒ 〈q2 c,〈bit x,L〉〉
386 | q2 d ⇒ 〈q0,〈c,R〉〉
387 | q3 ⇒ (* finale *) ].