matita/matita/lib/turing/multi_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/multi_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.
  71   FinProd (initN n) (FinOption FinBool).
  72
  73 definition trans_target ≝ λn.
  74   FinProd (FinProd (initN n) (FinOption FinBool)) FinMove.
  75
  76 record normalTM : Type[0] ≝
  77 { no_states : nat;
  78   pos_no_states : (0 < no_states);
  79   ntrans : trans_source no_states → trans_target no_states;
  80   nhalt : initN no_states → bool
  81 }.
  82
  83 (* A normal machine is just a special case of Turing Machine. *)
  84
  85 definition normalTM_to_TM ≝ λM:normalTM.
  86   mk_TM FinBool (initN (no_states M))
  87    (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
  88
  89 coercion normalTM_to_TM.
  90
  91 definition nconfig ≝ λn. config FinBool (initN n).
  92
  93 (******************************** tuples **************************************)
  94
  95 (* By general results on FinSets we know that every function f between two
  96 finite sets A and B can be described by means of a finite graph of pairs
  97 〈a,f a〉. Hence, the transition function of a normal turing machine can be
  98 described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type:
  99   (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).
 100 Unfortunately this description is not suitable for a Universal Machine, since
 101 such a machine must work with a fixed alphabet, while the size on n is unknown.
 102 Hence, we must pass from natural numbers to a representation for them on a
 103 finitary, e.g. binary, alphabet. In general, we shall associate
 104 to a pair 〈〈i,x〉,〈j,y,m〉〉 a tuple with the following syntactical structure
 105            | w_i x w_j y m
 106 where
 107 1. "|" is a special character used to separate tuples
 108 2. w_i and w_j are list of booleans representing the states $i$ and $j$;
 109 3. x and y are encoding
 110 4. finally, m ...
 111 *)
 112
 113 definition mk_tuple ≝ λqin,cin,qout,cout,mv.
 114   bar::qin@cin::qout@[cout;mv].
 115
 116 definition tuple_TM : nat → list unialpha → Prop ≝
 117  λn,t.∃qin,cin,qout,cout,mv.
 118  only_bits qin ∧ only_bits qout ∧ cin ≠ bar ∧ cout ≠ bar ∧ mv ≠ bar ∧
 119  |qin| = n ∧ |qout| = n ∧
 120  t = mk_tuple qin cin qout cout mv.
 121
 122 (***************************** state encoding *********************************)
 123 (* p < n is represented with a list of bits of lenght n with the p-th bit from
 124 left set to 1. An additional intial bit is set to 1 if the state is final and
 125 to 0 otherwise. *)
 126
 127 let rec to_bitlist n p: list bool ≝
 128   match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p].
 129
 130 let rec from_bitlist l ≝
 131   match l with
 132   [ nil ⇒ 0 (* assert false *)
 133   | cons b tl ⇒ if b then |tl| else from_bitlist tl].
 134
 135 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
 136 #n elim n normalize //
 137 qed.
 138
 139 lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
 140 #n elim n normalize -n
 141   [#p #abs @False_ind /2/
 142   |#n #Hind #p #lepn
 143    cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
 144     [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
 145      >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
 146     |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
 147     ]
 148   ]
 149 qed.
 150
 151 lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
 152 #l elim l normalize // #b #tl #Hind cases b normalize //
 153 #Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
 154   [@le_S_S @lt_to_le @Hind //
 155   |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
 156   ]
 157 qed.
 158
 159 definition nat_of: ∀n. Nat_to n → nat.
 160 #n normalize * #p #_ @p
 161 qed.
 162
 163 definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
 164    map ? unialpha (λx.bit x) (h s::(to_bitlist n (nat_of n s))).
 165
 166 lemma only_bits_bits_of_state : ∀n,h,p. only_bits (bits_of_state n h p).
 167 #n #h #p #x whd in match (bits_of_state n h p);
 168 #H cases H -H
 169   [#H >H %
 170   |elim (to_bitlist n (nat_of n p))
 171     [@False_ind |#b #l #Hind #H cases H -H #H [>H % |@Hind @H ]]
 172   ]
 173 qed.
 174
 175 (******************************** action encoding *****************************)
 176
 177 definition low_char ≝ λc.
 178   match c with
 179     [ None ⇒ null
 180     | Some b ⇒ bit b
 181     ].
 182
 183 definition low_mv ≝ λm.
 184   match m with
 185   [ R ⇒ bit true
 186   | L ⇒ bit false
 187   | N ⇒ null
 188   ].
 189
 190 (******************************** tuple encoding ******************************)
 191 definition tuple_type ≝ λn.
 192  (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).
 193
 194 definition tuple_encoding ≝ λn.λh:Nat_to n→bool.
 195   λp:tuple_type n.
 196   let 〈inp,outp〉 ≝ p in
 197   let 〈q,a〉 ≝ inp in
 198   let 〈qn,an,m〉 ≝ outp in
 199   let qin ≝ bits_of_state n h q in
 200   let qout ≝ bits_of_state n h qn in
 201   let cin ≝ low_char a in
 202   let cout ≝ low_char an in
 203   let mv ≝ low_mv m in
 204   mk_tuple qin cin qout cout mv.
 205
 206 lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p).
 207 #n #h * * #q #a * * #qn #an #m
 208 %{(bits_of_state n h q)} %{(low_char a)}
 209 %{(bits_of_state n h qn)} %{(low_char an)} %{(low_mv m)}
 210 % // %
 211   [%[%[%[%[% /2/ |% cases a normalize [|#b] #H destruct]
 212         |% cases an normalize [|#b] #H destruct]
 213       |% cases m normalize #H destruct]
 214     |>length_map normalize @eq_f //]
 215   |>length_map normalize @eq_f //]
 216 qed.
 217
 218 definition tuple_length ≝ λn.2*n+4.
 219
 220 lemma length_of_tuple: ∀n,t. tuple_TM n t →
 221   |t| = tuple_length n.
 222 #n #t * #qin * #cin * #qout * #cout * #mv *** #_ #Hqin #Hqout #eqt
 223 >eqt normalize >length_append >Hqin -Hqin normalize >length_append
 224 normalize >Hqout //
 225 qed.
 226
 227 definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p).
 228
 229
 230
 231