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 *) ].