matita/matita/lib/turing/universal.ma

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