1 include "turing/turing.ma".
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 ","
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)
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
19 MACCHINA per confronto tuple:
20 =============================
23 ls # current # ... | input , output , D | ... # rs
29 ls # current # ... | input , output , D | ... # rs (rimuove le marcature e si sposta sull'output)
34 ls # current # ... | input , output , D | ... # rs (sposta la marcatura alla tupla successiva)
42 \forall c != *z. c/L --> 1
43 \forall x. *x/x/R --> 2(x)
46 \forall y. y/*y/R --> 3(x)
50 \forall y.\forall c != *y. c/R --> 3(x)
55 \forall x. x/*x/L --> 1
59 \forall c != |. c/R --> 5
63 \forall x. x/*x/L --> 7
66 \forall c != #. c/L --> 7
70 \forall c != #. c/L --> 8
71 \forall x. *x/x/L --> 8
75 \forall x. x/*x/L --> FAILURE
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.
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.
90 definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
92 definition tmatch ≝ λs,c.
95 [ grid ⇒ 〈qm1,〈grid,R〉〉
96 | _ ⇒ 〈qmsink,〈c,N〉〉 ]
98 [ mark x ⇒ 〈qm2 x,〈bit x,R〉〉
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〉〉 ]
110 [ comma ⇒ 〈qmsuccess,〈comma,R〉〉
111 | bit x ⇒ 〈qm1,〈mark x,L〉〉
112 | _ ⇒ 〈qmsink,〈c,N〉〉 ]
114 [ bar ⇒ 〈qm6,〈bar,R〉〉
117 [ bit x ⇒ 〈qm7,〈mark x,L〉〉
118 | _ ⇒ 〈qmsink,〈c,N〉〉 ]
120 [ grid ⇒ 〈qm8,〈grid,L〉〉
123 [ grid ⇒ 〈qm9,〈grid,R〉〉
124 | mark x ⇒ 〈qm8,〈bit x,L〉〉
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〉〉].
135 ==============================
136 MACCHINA PER COPIA NUOVO STATO IN CURRENT
137 ==============================
141 ls # current # ... | in_state , out_state , D | ... # rs
146 ls # out_state # ... | in_state , out_state , D | ... # rs
151 \forall x. x/*x/L --> 1
162 \forall x. x/*x/R --> 4
167 \forall x. *x/x/R --> 5(x)
171 \forall y. y/*y/L --> 7(x)
174 \forall D. D/*D/L --> 7(x)
178 \forall y. *y/x/R --> 3
182 \forall D. *D/D/L --> 9
190 [ bit x ⇒ 〈q1,〈mark x,L〉〉
191 | _ ⇒ 〈qsink,〈c,N〉〉 ]
197 | _ ⇒ 〈qsink,〈c,N〉〉 ]
201 | _ ⇒ 〈qsink,〈c,N〉〉 ]
203 [ bit x ⇒ 〈q4,〈mark x,R〉〉
205 | _ ⇒ 〈qsink,〈c,N〉〉 ]
211 | mark x ⇒ 〈q5 x,〈bit x,R〉〉 ]
212 | q5 x ⇒ match c with
213 [ grid ⇒ 〈q6 x,〈c,R〉〉
214 | bit y ⇒ 〈q7 x,〈mark y,L〉〉
215 | _ ⇒ 〈qsink,〈c,N〉〉 ]
216 | q6 x ⇒ match c with
217 [ bit D ⇒ 〈q7 x,〈mark D,L〉〉
218 | _ ⇒ 〈qsink,〈c,N〉〉 ]
219 | q7 x ⇒ match c with
220 [ bit y ⇒ 〈q7 x,〈c,L〉〉
221 | comma ⇒ 〈q7 x,〈c,L〉〉
223 | grid ⇒ 〈q7 x,〈c,L〉〉
224 | mark y ⇒ 〈q3,〈bit x,R〉〉 ]
230 | mark D ⇒ 〈q9,〈bit D,L〉〉 ]
231 | q9 ⇒ ? (* successo *)
235 ==================================
236 MACCHINE PER SPOSTARE LA "TESTINA"
237 ================================
239 Lo spostamento a sx si ottiene mediante
241 ls x # current y # macchina # rs
243 ls x # current # y macchina # rs
245 ls x # current # macchina # y rs
247 ls # x current # macchina # y rs
249 ls # current x # macchina # y rs
252 Lo spostamento a dx si ottiene mediante
254 ls # current x # macchina # y rs
256 ls x # current # macchina # y rs
258 ls x # current # macchina y # rs
260 ls x # current y # macchina # rs
265 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
279 \forall x.x/L --> 1(x)
282 \forall c != #. c/x/R --> 2(c)
286 \forall d. d/c/L --> 0
289 \forall c. c/#/L --> 4
297 [ bit x ⇒ 〈q1 x,〈c,L〉〉
298 | _ ⇒ 〈qsink,〈c,N〉〉 ]
299 | q1 x ⇒ match c with
300 [ grid ⇒ 〈q3,〈bit x,R〉〉
301 | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
304 | q4 ⇒ (* finale *) ].
309 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
323 \forall x.x/R --> 1(x)
326 \forall c != #. c/x/L --> 2(c)
330 \forall d. d/c/R --> 0
333 \forall c. c/#/L --> 4
341 [ bit x ⇒ 〈q1 x,〈c,R〉〉
343 | q1 x ⇒ match c with
344 [ grid ⇒ 〈q3,〈bit x,L〉〉
345 | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
348 | q4 ⇒ (* finale *) ].
353 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
366 \forall x. x/R --> 1(x)
369 \forall c != #. c/x/L --> 2(c)
373 \forall d. d/c/R --> 0
382 [ bit x ⇒ 〈q1 x,〈c,R〉〉
383 | _ ⇒ 〈qsink,〈c,N〉〉 ]
384 | q1 x ⇒ match c with
385 [ grid ⇒ 〈q3,〈grid,L〉〉
386 | _ ⇒ 〈q2 c,〈bit x,L〉〉
388 | q3 ⇒ (* finale *) ].