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
 126
 127
 128
 129
 130
 131
 132
 133 (*
 134 ==============================
 135 MACCHINA PER COPIA NUOVO STATO IN CURRENT
 136 ==============================
 137
 138 Input:
 139
 140   ls # current # ... | in_state , out_state , D | ... # rs
 141                                   ^
 142                                   0
 143
 144 Output:
 145   ls # out_state # ... | in_state , out_state , D | ... # rs
 146                                               ^
 147                                               9
 148
 149 STATO 0:
 150   \forall x. x/*x/L --> 1
 151
 152 STATO 1:
 153   [01,|]/L --> 1
 154   #/L --> 2
 155
 156 STATO 2:
 157   [01]/L --> 2
 158   #/R -> 3
 159
 160 STATO 3:
 161   \forall x. x/*x/R --> 4
 162   #/R --> 8
 163
 164 STATO 4:
 165   [01,|#]/R --> 4
 166   \forall x. *x/x/R --> 5(x)
 167
 168 STATO 5(x):
 169   #/R --> 6(x)
 170   \forall y. y/*y/L --> 7(x)
 171
 172 STATO 6(x):
 173   \forall D. D/*D/L --> 7(x)
 174
 175 STATO 7(x):
 176   [01,|#]/l --> 7(x)
 177   \forall y. *y/x/R --> 3
 178
 179 STATO 8:
 180   [01,|#]/R --> 8
 181   \forall D. *D/D/L --> 9
 182
 183 STATO 9:
 184   stato finale
 185
 186
 187 ==================================
 188 MACCHINE PER SPOSTARE LA "TESTINA"
 189 ================================
 190
 191 Lo spostamento a sx si ottiene mediante
 192
 193 ls x # current y # macchina # rs
 194 ----C--->
 195 ls x # current # y macchina # rs
 196 ----B--->
 197 ls x # current # macchina # y rs
 198 ----B--->
 199 ls # x current # macchina # y rs
 200 ----C--->
 201 ls # current x # macchina # y rs
 202
 203
 204 Lo spostamento a dx si ottiene mediante
 205
 206 ls # current x # macchina # y rs
 207 ----A--->
 208 ls x # current # macchina # y rs
 209 ----A--->
 210 ls x # current # macchina y # rs
 211 ----A--->
 212 ls x # current y # macchina # rs
 213
 214
 215 MACCHINA A
 216 ----------
 217 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
 218
 219 Input:
 220
 221   ls # cs x rs
 222           ^
 223           0
 224
 225 Output:
 226   ls x # cs rs
 227      ^
 228      4
 229
 230 STATO 0:
 231   \forall x.x/L --> 1(x)
 232
 233 STATO 1(x):
 234   \forall c != #. c/x/R --> 2(c)
 235   #/x/R --> 3
 236
 237 STATO 2(c):
 238   \forall d. d/c/L --> 0
 239
 240 STATO 3:
 241   \forall c. c/#/L --> 4
 242
 243 STATO 4:
 244   stato finale
 245
 246
 247 MACCHINA B
 248 ----------
 249 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
 250
 251 Input:
 252
 253   ls x cs # rs
 254      ^
 255      0
 256
 257 Output:
 258   ls cs # x rs
 259           ^
 260           4
 261
 262 STATO 0:
 263   \forall x.x/R --> 1(x)
 264
 265 STATO 1(x):
 266   \forall c != #. c/x/L --> 2(c)
 267   #/x/L --> 3
 268
 269 STATO 2(c):
 270   \forall d. d/c/R --> 0
 271
 272 STATO 3:
 273   \forall c. c/#/L --> 4
 274
 275 STATO 4:
 276   stato finale
 277
 278
 279 MACCHINA C
 280 ----------
 281 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
 282
 283 Input:
 284   ls x cs # rs
 285      ^
 286      0
 287
 288 Output:
 289   ls cs x # rs
 290         ^
 291         3
 292
 293 STATO 0:
 294   \forall x. x/R --> 1(x)
 295
 296 STATO 1(x):
 297   \forall c != #. c/x/L --> 2(c)
 298   #/#/L --> 3
 299
 300 STATO 2(c):
 301   \forall d. d/c/R --> 0
 302
 303 STATO 3:
 304   stato finale
 305
 306 *)