matita/matita/lib/turing/char_move.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 *)
  20
  21 inductive alpha_uni : Type[0] ≝
  22 | bit : bool → alpha_uni
  23 | mark : bool → alpha_uni
  24 | grid : alpha_uni | bar : alpha_uni | comma : alpha_uni.
  25
  26 inductive Qmatch : Type[0] ≝
  27 | qm0 : Qmatch | qm1 : Qmatch | qm2 : bool → Qmatch | qm3 : bool → Qmatch
  28 | qm4 : Qmatch | qm5 : Qmatch | qm6 : Qmatch | qm7 : Qmatch
  29 | qm8 : Qmatch | qm9 : Qmatch
  30 | qmsuccess : Qmatch | qmfailure : Qmatch | qmsink : Qmatch.
  31
  32 definition bool_eqb ≝ λb1,b2:bool.¬ (xorb b1 b2).
  33
  34 (*
  35 ==================================
  36 MACCHINE PER SPOSTARE LA "TESTINA"
  37 ================================
  38
  39 Lo spostamento a sx si ottiene mediante
  40
  41 ls x # current y # macchina # rs
  42 ----C--->
  43 ls x # current # y macchina # rs
  44 ----B--->
  45 ls x # current # macchina # y rs
  46 ----B--->
  47 ls # x current # macchina # y rs
  48 ----C--->
  49 ls # current x # macchina # y rs
  50
  51
  52 Lo spostamento a dx si ottiene mediante
  53
  54 ls # current x # macchina # y rs
  55 ----A--->
  56 ls x # current # macchina # y rs
  57 ----A--->
  58 ls x # current # macchina y # rs
  59 ----A--->
  60 ls x # current y # macchina # rs
  61
  62
  63 MACCHINA A
  64 ----------
  65 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua sinistra.
  66
  67 Input:
  68
  69   ls # cs x rs
  70           ^
  71           0
  72
  73 Output:
  74   ls x # cs rs
  75      ^
  76      4
  77
  78 STATO 0:
  79   \forall x.x/L --> 1(x)
  80
  81 STATO 1(x):
  82   \forall c != #. c/x/R --> 2(c)
  83   #/x/R --> 3
  84
  85 STATO 2(c):
  86   \forall d. d/c/L --> 0
  87
  88 STATO 3:
  89   \forall c. c/#/L --> 4
  90
  91 STATO 4:
  92   stato finale
  93 *)
  94
  95 (* struttura generica della semantica *)
  96 lemma move_char_sem: ∀inc. prec inc → ∃i. ∃outc. loop i step inc = Some outc
  97 ∧ postc outc inc.
  98
  99 lemma sequential : ∀M1,M2.
 100
 101 definition pre c ≝
 102   let s ≝ state c in
 103   let tp ≝ tape c in
 104   let left ≝
 105
 106 definition post c1 c2 ≝
 107   let s1 ≝ state c1 in
 108   let tp1 ≝ tape c1 in
 109   let leftt ≝ left tp1 in
 110   let rightt ≝ right tp1 in
 111   c2 = mk_config finals
 112
 113
 114
 115 match s with
 116  [ q0 ⇒ match c with
 117    [ bit x ⇒ 〈q1 x,〈c,L〉〉
 118    | _ ⇒ 〈qsink,〈c,N〉〉 ]
 119  | q1 x ⇒ match c with
 120    [ grid ⇒ 〈q3,〈bit x,R〉〉
 121    | _ ⇒ 〈q2 c,〈bit x,R〉〉 ]
 122  | q2 d ⇒ 〈q0,〈d,L〉〉
 123  | q3 ⇒ 〈q4,〈grid,L〉〉
 124  | q4 ⇒ (* finale *) ].
 125
 126 (*
 127 MACCHINA B
 128 ----------
 129 Sposta il carattere binario su cui si trova la testina oltre il primo # alla sua destra.
 130
 131 Input:
 132
 133   ls x cs # rs
 134      ^
 135      0
 136
 137 Output:
 138   ls cs # x rs
 139           ^
 140           4
 141
 142 STATO 0:
 143   \forall x.x/R --> 1(x)
 144
 145 STATO 1(x):
 146   \forall c != #. c/x/L --> 2(c)
 147   #/x/L --> 3
 148
 149 STATO 2(c):
 150   \forall d. d/c/R --> 0
 151
 152 STATO 3:
 153   \forall c. c/#/L --> 4
 154
 155 STATO 4:
 156   stato finale
 157 *)
 158
 159 match s with
 160 [ q0 ⇒ match c with
 161   [ bit x ⇒ 〈q1 x,〈c,R〉〉
 162   | _ ⇒ 〈qsink,〈c,N〉〉]
 163 | q1 x ⇒ match c with
 164   [ grid ⇒ 〈q3,〈bit x,L〉〉
 165   | _ ⇒ 〈q2 c,〈bit x,L〉〉 ]
 166 | q2 d ⇒ 〈q0,〈d,R〉〉
 167 | q3 ⇒ 〈q4,〈grid,L〉〉
 168 | q4 ⇒ (* finale *) ].
 169
 170 (*
 171 MACCHINA C
 172 ----------
 173 Sposta il carattere binario su cui si trova la testina appena prima del primo # alla sua destra.
 174
 175 Input:
 176   ls x cs # rs
 177      ^
 178      0
 179
 180 Output:
 181   ls cs x # rs
 182         ^
 183         3
 184
 185 STATO 0:
 186   \forall x. x/R --> 1(x)
 187
 188 STATO 1(x):
 189   \forall c != #. c/x/L --> 2(c)
 190   #/#/L --> 3
 191
 192 STATO 2(c):
 193   \forall d. d/c/R --> 0
 194
 195 STATO 3:
 196   stato finale
 197
 198 *)
 199
 200 match s with
 201 [ q0 ⇒ match c with
 202   [ bit x ⇒ 〈q1 x,〈c,R〉〉
 203   | _ ⇒ 〈qsink,〈c,N〉〉 ]
 204 | q1 x ⇒ match c with
 205   [ grid ⇒ 〈q3,〈grid,L〉〉
 206   | _ ⇒ 〈q2 c,〈bit x,L〉〉
 207 | q2 d ⇒ 〈q0,〈c,R〉〉
 208 | q3 ⇒ (* finale *) ].