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 (* TODO
 188 match s with
 189  [ q0 ⇒ match c with
 190    [ bit x ⇒ 〈q1,〈mark x,L〉〉
 191    | _ ⇒ 〈qsink,〈c,N〉〉 ]
 192  | q1 ⇒ match c with
 193    [ bit x ⇒ 〈q1,〈c,L〉〉
 194    | comma ⇒ 〈q1,〈c,L〉〉
 195    | bar ⇒ 〈q1,〈c,L〉〉
 196    | grid ⇒ 〈q2,〈c,R〉〉
 197    | _ ⇒ 〈qsink,〈c,N〉〉 ]
 198  | q2 ⇒ match c with
 199    [ bit x ⇒ 〈q2,〈c,L〉〉
 200    | grid ⇒ 〈q3,〈c,R〉〉
 201    | _ ⇒ 〈qsink,〈c,N〉〉 ]
 202  | q3 ⇒ match c with
 203    [ bit x ⇒ 〈q4,〈mark x,R〉〉
 204    | grid ⇒ 〈q8,〈c,R〉〉
 205    | _ ⇒ 〈qsink,〈c,N〉〉 ]
 206  | q4 ⇒ match c with
 207    [ bit x ⇒ 〈q4,〈c,R〉〉
 208    | comma ⇒ 〈q4,〈c,R〉〉
 209    | bar ⇒ 〈q4,〈c,R〉〉
 210    | grid ⇒ 〈q4,〈c,R〉〉
 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〉〉
 222    | bar ⇒ 〈q7 x,〈c,L〉〉
 223    | grid ⇒ 〈q7 x,〈c,L〉〉
 224    | mark y ⇒ 〈q3,〈bit x,R〉〉 ]
 225  | q8 ⇒ match c with
 226    [ bit y ⇒ 〈q8,〈c,R〉〉
 227    | comma ⇒ 〈q8,〈c,R〉〉
 228    | bar ⇒ 〈q8,〈c,R〉〉
 229    | grid ⇒ 〈q8,〈c,R〉〉
 230    | mark D ⇒ 〈q9,〈bit D,L〉〉 ]
 231  | q9 ⇒ ? (* successo *)
 232  ].
 233 *)
 234 (*
 235 ==================================
 236 MACCHINE PER SPOSTARE LA "TESTINA"
 237 ================================
 238
 239 Lo spostamento a sx si ottiene mediante
 240
 241 ls x # current y # macchina # rs
 242 ----C--->
 243 ls x # current # y macchina # rs
 244 ----B--->
 245 ls x # current # macchina # y rs
 246 ----B--->
 247 ls # x current # macchina # y rs
 248 ----C--->
 249 ls # current x # macchina # y rs
 250
 251
 252 Lo spostamento a dx si ottiene mediante
 253
 254 ls # current x # macchina # y rs
 255 ----A--->
 256 ls x # current # macchina # y rs
 257 ----A--->
 258 ls x # current # macchina y # rs
 259 ----A--->
 260 ls x # current y # macchina # rs
 261
 262
 263 MACCHINA A
 264 ----------
 265 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
 266
 267 Input:
 268
 269   ls # cs x rs
 270           ^
 271           0
 272
 273 Output:
 274   ls x # cs rs
 275      ^
 276      4
 277
 278 STATO 0:
 279   \forall x.x/L --> 1(x)
 280
 281 STATO 1(x):
 282   \forall c != #. c/x/R --> 2(c)
 283   #/x/R --> 3
 284
 285 STATO 2(c):
 286   \forall d. d/c/L --> 0
 287
 288 STATO 3:
 289   \forall c. c/#/L --> 4
 290
 291 STATO 4:
 292   stato finale
 293 *)
 294 (* TODO
 295 match s with
 296  [ q0 ⇒ match c with
 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〉〉 ]
 302  | q2 d ⇒ 〈q0,〈d,L〉〉
 303  | q3 ⇒ 〈q4,〈grid,L〉〉
 304  | q4 ⇒ (* finale *) ].
 305 *)
 306 (*
 307 MACCHINA B
 308 ----------
 309 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
 310
 311 Input:
 312
 313   ls x cs # rs
 314      ^
 315      0
 316
 317 Output:
 318   ls cs # x rs
 319           ^
 320           4
 321
 322 STATO 0:
 323   \forall x.x/R --> 1(x)
 324
 325 STATO 1(x):
 326   \forall c != #. c/x/L --> 2(c)
 327   #/x/L --> 3
 328
 329 STATO 2(c):
 330   \forall d. d/c/R --> 0
 331
 332 STATO 3:
 333   \forall c. c/#/L --> 4
 334
 335 STATO 4:
 336   stato finale
 337 *)
 338 (* TODO
 339 match s with
 340 [ q0 ⇒ match c with
 341   [ bit x ⇒ 〈q1 x,〈c,R〉〉
 342   | _ ⇒ 〈qsink,〈c,N〉〉]
 343 | q1 x ⇒ match c with
 344   [ grid ⇒ 〈q3,〈bit x,L〉〉
 345   | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
 346 | q2 d ⇒ 〈q0,〈d,R〉〉
 347 | q3 ⇒ 〈q4,〈grid,L〉〉
 348 | q4 ⇒ (* finale *) ].
 349 *)
 350 (*
 351 MACCHINA C
 352 ----------
 353 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
 354
 355 Input:
 356   ls x cs # rs
 357      ^
 358      0
 359
 360 Output:
 361   ls cs x # rs
 362         ^
 363         3
 364
 365 STATO 0:
 366   \forall x. x/R --> 1(x)
 367
 368 STATO 1(x):
 369   \forall c != #. c/x/L --> 2(c)
 370   #/#/L --> 3
 371
 372 STATO 2(c):
 373   \forall d. d/c/R --> 0
 374
 375 STATO 3:
 376   stato finale
 377
 378 *)
 379 (* TODO
 380 match s with
 381 [ q0 ⇒ match c with
 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〉〉
 387 | q2 d ⇒ 〈q0,〈c,R〉〉
 388 | q3 ⇒ (* finale *) ].
 389 *)