matita/matita/lib/turing/universal/normalTM.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "turing/universal/alphabet.ma".
  13 include "turing/mono.ma".
  14
  15 (************************* turning DeqMove into a DeqSet **********************)
  16 definition move_eq ≝ λm1,m2:move.
  17   match m1 with
  18   [R ⇒ match m2 with [R ⇒ true | _ ⇒ false]
  19   |L ⇒ match m2 with [L ⇒ true | _ ⇒ false]
  20   |N ⇒ match m2 with [N ⇒ true | _ ⇒ false]].
  21
  22 lemma move_eq_true:∀m1,m2.
  23   move_eq m1 m2 = true ↔ m1 = m2.
  24 *
  25   [* normalize [% #_ % |2,3: % #H destruct ]
  26   |* normalize [1,3: % #H destruct |% #_ % ]
  27   |* normalize [1,2: % #H destruct |% #_ % ]
  28 qed.
  29
  30 definition DeqMove ≝ mk_DeqSet move move_eq move_eq_true.
  31
  32 unification hint 0 ≔ ;
  33     X ≟ DeqMove
  34 (* ---------------------------------------- *) ⊢
  35     move ≡ carr X.
  36
  37 unification hint  0 ≔ m1,m2;
  38     X ≟ DeqMove
  39 (* ---------------------------------------- *) ⊢
  40     move_eq m1 m2 ≡ eqb X m1 m2.
  41
  42
  43 (************************ turning DeqMove into a FinSet ***********************)
  44 definition move_enum ≝ [L;R;N].
  45
  46 lemma move_enum_unique: uniqueb ? [L;R;N] = true.
  47 // qed.
  48
  49 lemma move_enum_complete: ∀x:move. memb ? x [L;R;N] = true.
  50 * // qed.
  51
  52 definition FinMove ≝
  53   mk_FinSet DeqMove [L;R;N] move_enum_unique move_enum_complete.
  54
  55 unification hint  0 ≔ ;
  56     X ≟ FinMove
  57 (* ---------------------------------------- *) ⊢
  58     move ≡ FinSetcarr X.
  59
  60 (*************************** normal Turing Machines ***************************)
  61
  62 (* A normal turing machine is just an ordinary machine where:
  63   1. the tape alphabet is bool
  64   2. the finite state are supposed to be an initial segment of the natural
  65      numbers.
  66   Formally, it is specified by a record with the number n of states, a proof
  67   that n is positive, the transition function and the halting function.
  68 *)
  69
  70 definition trans_source ≝ λn.FinProd (initN n) (FinOption FinBool).
  71 definition trans_target ≝ λn.FinProd (initN n) (FinOption (FinProd FinBool FinMove)).
  72
  73 record normalTM : Type[0] ≝
  74 { no_states : nat;
  75   pos_no_states : (0 < no_states);
  76   ntrans : trans_source no_states → trans_target no_states;
  77   nhalt : initN no_states → bool
  78 }.
  79
  80 (* A normal machine is just a special case of Turing Machine. *)
  81
  82 definition normalTM_to_TM ≝ λM:normalTM.
  83   mk_TM FinBool (initN (no_states M))
  84    (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
  85
  86 coercion normalTM_to_TM.
  87
  88 definition nconfig ≝ λn. config FinBool (initN n).
  89
  90 (******************************** tuples **************************************)
  91
  92 (* By general results on FinSets we know that every function f between two
  93 finite sets A and B can be described by means of a finite graph of pairs
  94 〈a,f a〉. Hence, the transition function of a normal turing machine can be
  95 described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type:
  96   (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
  97 Unfortunately this description is not suitable for a Universal Machine, since
  98 such a machine must work with a fixed alphabet, while the size on n is unknown.
  99 Hence, we must pass from natural numbers to a representation for them on a
 100 finitary, e.g. binary, alphabet. In general, we shall associate
 101 to a pair 〈〈i,c〉,〈j,action〉〉 a tuple with the following syntactical structure
 102            |w_ix,w_jy,z
 103 where
 104 1. "|" and "," are special characters used as delimiters;
 105 2. w_i and w_j are list of booleans representing the states $i$ and $j$;
 106 3. x is special symbol null if c=None and is a if c=Some a
 107 4. y and z are both null if action = None, and are equal to b,m' if
 108    action = Some b,m;
 109 5. finally, m' = 0 if m = L, m' = 1 if m=R and m' = null if m = N
 110
 111 As a minor, additional complication, we shall suppose that every characters is
 112 decorated by an additonal bit, normally set to false, to be used as a marker.
 113 *)
 114
 115 definition mk_tuple ≝ λqin,cin,qout,cout,mv.
 116   〈bar,false〉::qin@cin::〈comma,false〉::qout@cout::〈comma,false〉::[mv].
 117
 118 (* by definition, a tuple is not marked *)
 119 definition tuple_TM : nat → list STape → Prop ≝
 120  λn,t.∃qin,cin,qout,cout,mv.
 121  no_marks qin ∧ no_marks qout ∧
 122  only_bits qin ∧ only_bits qout ∧
 123  bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧
 124  (cout = null → mv = null) ∧
 125  |qin| = n ∧ |qout| = n ∧
 126  t = mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
 127
 128 (***************************** state encoding *********************************)
 129 (* p < n is represented with a list of bits of lenght n with the p-th bit from
 130 left set to 1. An additional intial bit is set to 1 if the state is final and
 131 to 0 otherwise. *)
 132
 133 let rec to_bitlist n p: list bool ≝
 134   match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p].
 135
 136 let rec from_bitlist l ≝
 137   match l with
 138   [ nil ⇒ 0 (* assert false *)
 139   | cons b tl ⇒ if b then |tl| else from_bitlist tl].
 140
 141 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
 142 #n elim n normalize //
 143 qed.
 144
 145 lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
 146 #n elim n normalize -n
 147   [#p #abs @False_ind /2/
 148   |#n #Hind #p #lepn
 149    cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
 150     [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
 151      >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
 152     |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
 153     ]
 154   ]
 155 qed.
 156
 157 lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
 158 #l elim l normalize // #b #tl #Hind cases b normalize //
 159 #Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
 160   [@le_S_S @lt_to_le @Hind //
 161   |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
 162   ]
 163 qed.
 164
 165 definition nat_of: ∀n. Nat_to n → nat.
 166 #n normalize * #p #_ @p
 167 qed.
 168
 169 definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
 170   h s::(to_bitlist n (nat_of n s)).
 171
 172 definition m_bits_of_state ≝ λn.λh.λp.
 173   map ? (unialpha×bool) (λx.〈bit x,false〉) (bits_of_state n h p).
 174
 175 lemma no_marks_bits_of_state : ∀n,h,p. no_marks (m_bits_of_state n h p).
 176 #n #h #p #x whd in match (m_bits_of_state n h p);
 177 #H cases (orb_true_l … H) -H
 178   [#H >(\P H) %
 179   |elim (to_bitlist n (nat_of n p))
 180     [whd in ⊢ ((??%?)→?); #H destruct
 181     |#b #l #Hind #H cases (orb_true_l … H) -H #H
 182       [>(\P H) % |@Hind @H]
 183     ]
 184   ]
 185 qed.
 186
 187 lemma only_bits_bits_of_state : ∀n,h,p. only_bits (m_bits_of_state n h p).
 188 #n #h #p #x whd in match (m_bits_of_state n h p);
 189 #H cases (orb_true_l … H) -H
 190   [#H >(\P H) %
 191   |elim (to_bitlist n (nat_of n p))
 192     [whd in ⊢ ((??%?)→?); #H destruct
 193     |#b #l #Hind #H cases (orb_true_l … H) -H #H
 194       [>(\P H) % |@Hind @H ]
 195     ]
 196   ]
 197 qed.
 198
 199 (******************************** action encoding *****************************)
 200 definition low_action ≝ λaction.
 201   match action with
 202     [ None ⇒ 〈null,null〉
 203     | Some act ⇒ let 〈na,m〉 ≝ act in
 204       match m with
 205       [ R ⇒ 〈bit na,bit true〉
 206       | L ⇒ 〈bit na,bit false〉
 207       | N ⇒ 〈bit na,null〉]
 208     ].
 209
 210 (******************************** tuple encoding ******************************)
 211 definition tuple_type ≝ λn.
 212  (Nat_to n × (option FinBool)) × (Nat_to n × (option (FinBool × move))).
 213
 214 definition tuple_encoding ≝ λn.λh:Nat_to n→bool.
 215   λp:tuple_type n.
 216   let 〈inp,outp〉 ≝ p in
 217   let 〈q,a〉 ≝ inp in
 218   let cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ] in
 219   let 〈qn,action〉 ≝ outp in
 220   let 〈cout,mv〉 ≝ low_action action in
 221   let qin ≝ m_bits_of_state n h q in
 222   let qout ≝ m_bits_of_state n h qn in
 223   mk_tuple qin 〈cin,false〉 qout 〈cout,false〉 〈mv,false〉.
 224
 225 (*
 226 definition WFTuple_conditions ≝
 227  λn,qin,cin,qout,cout,mv.
 228  no_marks qin ∧ no_marks qout ∧ (* queste fuori ? *)
 229  only_bits qin ∧ only_bits qout ∧
 230  bit_or_null cin = true ∧ bit_or_null cout = true ∧ bit_or_null mv = true ∧
 231  (cout = null → mv = null) ∧
 232  |qin| = n ∧ |qout| = n. *)
 233
 234 lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p).
 235 #n #h * * #q #a * #qn #action
 236 @(ex_intro … (m_bits_of_state n h q))
 237 letin cin ≝ match a with [ None ⇒ null | Some b ⇒ bit b ]
 238 @(ex_intro … cin)
 239 @(ex_intro … (m_bits_of_state n h qn))
 240 letin cout ≝
 241   match action with
 242   [ None ⇒ null | Some act ⇒ bit (\fst act)]
 243 @(ex_intro … cout)
 244 letin mv ≝ match action with
 245   [ None ⇒ null
 246   | Some act ⇒
 247       match \snd act with
 248       [ R ⇒ bit true | L ⇒ bit false | N ⇒ null]
 249   ]
 250 @(ex_intro … mv)
 251 %[%[%[%[%[%[%[% /3/
 252              |whd in match cin ; cases a //]
 253            |whd in match cout; cases action //]
 254          |whd in match mv; cases action // * #b #m cases m //]
 255        |whd in match cout; whd in match mv; cases action
 256          [// | #act whd in ⊢ ((??%?)→?); #Hfalse destruct ]]
 257      |>length_map normalize @eq_f //]
 258    |>length_map normalize @eq_f //]
 259  |normalize cases a cases action normalize //
 260    [* #c #m cases m % |* #c #m #c1 cases m %]
 261  ]
 262 qed.
 263
 264 definition tuple_length ≝ λn.2*n+6.
 265
 266 lemma length_of_tuple: ∀n,t. tuple_TM n t →
 267   |t| = tuple_length n.
 268 #n #t * #qin * #cin * #qout * #cout * #mv *** #_ #Hqin #Hqout #eqt >eqt
 269 whd in match (mk_tuple ?????); normalize >length_append >Hqin -Hqin normalize
 270 >length_append normalize >Hqout -Hqout //
 271 qed.
 272
 273 definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p).
 274
 275 (******************* general properties of encoding of tuples *****************)
 276
 277 lemma no_grids_in_tuple : ∀n,l.tuple_TM n l → no_grids l.
 278 #n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
 279 #_ #_ #Hqin #Hqout #Hcin #Hcout #Hmv #_ #_ #_ #Hl >Hl
 280 #c #Hc cases (orb_true_l … Hc) -Hc #Hc
 281 [ >(\P Hc) %
 282 | cases (memb_append … Hc) -Hc #Hc
 283 [ @bit_not_grid @(Hqin … Hc)
 284 | cases (orb_true_l … Hc) -Hc #Hc
 285 [ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
 286 | cases (orb_true_l … Hc) -Hc #Hc
 287 [ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
 288 | cases (memb_append …Hc) -Hc #Hc
 289 [ @bit_not_grid @(Hqout … Hc)
 290 | cases (orb_true_l … Hc) -Hc #Hc
 291 [ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) @bit_or_null_not_grid //
 292 | cases (orb_true_l … Hc) -Hc #Hc
 293 [ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
 294 | >(memb_single … Hc) @bit_or_null_not_grid @Hmv
 295 ]]]]]]
 296 qed.
 297
 298 lemma no_marks_in_tuple : ∀n,l.tuple_TM n l → no_marks l.
 299 #n #l * #qin * #cin * #qout * #cout * #mv * * * * * * * * * *
 300 #Hqin #Hqout #_ #_ #_ #_ #_ #_ #_ #_ #Hl >Hl
 301 #c #Hc cases (orb_true_l … Hc) -Hc #Hc
 302 [ >(\P Hc) %
 303 | cases (memb_append … Hc) -Hc #Hc
 304 [ @(Hqin … Hc)
 305 | cases (orb_true_l … Hc) -Hc #Hc
 306 [ change with (c == 〈cin,false〉 = true) in Hc; >(\P Hc) %
 307 | cases (orb_true_l … Hc) -Hc #Hc
 308 [ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
 309 | cases (memb_append … Hc) -Hc #Hc
 310 [ @(Hqout … Hc)
 311 | cases (orb_true_l … Hc) -Hc #Hc
 312 [ change with (c == 〈cout,false〉 = true) in Hc; >(\P Hc) %
 313 | cases (orb_true_l … Hc) -Hc #Hc
 314 [ change with (c == 〈comma,false〉 = true) in Hc; >(\P Hc) %
 315 | >(memb_single … Hc) %
 316 ]]]]]]
 317 qed.
 318
 319