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 (*************************** normal Turing Machines ***************************)
  16
  17 (* A normal turing machine is just an ordinary machine where:
  18   1. the tape alphabet is bool
  19   2. the finite state are supposed to be an initial segment of the natural
  20      numbers.
  21   Formally, it is specified by a record with the number n of states, a proof
  22   that n is positive, the transition function and the halting function.
  23 *)
  24
  25 definition trans_source ≝ λn.
  26   FinProd (initN n) (FinOption FinBool).
  27
  28 definition trans_target ≝ λn.
  29   FinProd (FinProd (initN n) (FinOption FinBool)) FinMove.
  30
  31 record normalTM : Type[0] ≝
  32 { no_states : nat;
  33   pos_no_states : (0 < no_states);
  34   ntrans : trans_source no_states → trans_target no_states;
  35   nhalt : initN no_states → bool
  36 }.
  37
  38 lemma decomp_target : ∀n.∀tg: trans_target n.
  39   ∃qout,cout,m. tg = 〈qout,cout,m〉.
  40 #n * * #q #c #m %{q} %{c} %{m} //
  41 qed.
  42
  43 (* A normal machine is just a special case of Turing Machine. *)
  44
  45 definition nstart_state ≝ λM.mk_Sig ?? 0 (pos_no_states M).
  46
  47 definition normalTM_to_TM ≝ λM:normalTM.
  48   mk_TM FinBool (initN (no_states M))
  49    (ntrans M) (nstart_state M) (nhalt M).
  50
  51 coercion normalTM_to_TM.
  52
  53 definition nconfig ≝ λn. config FinBool (initN n).
  54
  55 (* A normal machine has a non empty graph *)
  56
  57 definition sample_input: ∀M.trans_source (no_states M).
  58 #M % [@(nstart_state M) | %]
  59 qed.
  60
  61 lemma nTM_nog: ∀M. graph_enum ?? (ntrans M) ≠ [ ].
  62 #M % #H lapply(graph_enum_complete ?? (ntrans M) (sample_input M) ? (refl ??))
  63 >H normalize #Hd destruct
  64 qed.
  65
  66 (******************************** tuples **************************************)
  67
  68 (* By general results on FinSets we know that every function f between two
  69 finite sets A and B can be described by means of a finite graph of pairs
  70 〈a,f a〉. Hence, the transition function of a normal turing machine can be
  71 described by a finite set of tuples 〈i,c〉,〈j,action〉〉 of the following type:
  72   (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).
  73 Unfortunately this description is not suitable for a Universal Machine, since
  74 such a machine must work with a fixed alphabet, while the size on n is unknown.
  75 Hence, we must pass from natural numbers to a representation for them on a
  76 finitary, e.g. binary, alphabet. In general, we shall associate
  77 to a pair 〈〈i,x〉,〈j,y,m〉〉 a tuple with the following syntactical structure
  78            | w_i x w_j y m
  79 where
  80 1. "|" is a special character used to separate tuples
  81 2. w_i and w_j are list of booleans representing the states $i$ and $j$;
  82 3. x and y are encoding
  83 4. finally, m ...
  84 *)
  85
  86 definition mk_tuple ≝ λqin,cin,qout,cout,mv.
  87   bar::qin@cin::qout@[cout;mv].
  88
  89 definition tuple_TM : nat → list unialpha → Prop ≝
  90  λn,t.∃qin,cin,qout,cout,mv.
  91  only_bits qin ∧ only_bits qout ∧ cin ≠ bar ∧ cout ≠ bar ∧ mv ≠ bar ∧
  92  |qin| = n ∧ |qout| = n ∧
  93  t = mk_tuple qin cin qout cout mv.
  94
  95 (***************************** state encoding *********************************)
  96 (* p < n is represented with a list of bits of lenght n with the p-th bit from
  97 left set to 1. An additional intial bit is set to 1 if the state is final and
  98 to 0 otherwise. *)
  99
 100 let rec to_bitlist n p: list bool ≝
 101   match n with [ O ⇒ [ ] | S q ⇒ (eqb p q)::to_bitlist q p].
 102
 103 let rec from_bitlist l ≝
 104   match l with
 105   [ nil ⇒ 0 (* assert false *)
 106   | cons b tl ⇒ if b then |tl| else from_bitlist tl].
 107
 108 lemma bitlist_length: ∀n,p.|to_bitlist n p| = n.
 109 #n elim n normalize //
 110 qed.
 111
 112 lemma bitlist_inv1: ∀n,p.p<n → from_bitlist (to_bitlist n p) = p.
 113 #n elim n normalize -n
 114   [#p #abs @False_ind /2/
 115   |#n #Hind #p #lepn
 116    cases (le_to_or_lt_eq … (le_S_S_to_le … lepn))
 117     [#ltpn lapply (lt_to_not_eq … ltpn) #Hpn
 118      >(not_eq_to_eqb_false … Hpn) normalize @Hind @ltpn
 119     |#Heq >(eq_to_eqb_true … Heq) normalize <Heq //
 120     ]
 121   ]
 122 qed.
 123
 124 lemma bitlist_lt: ∀l. 0 < |l| → from_bitlist l < |l|.
 125 #l elim l normalize // #b #tl #Hind cases b normalize //
 126 #Htl cases (le_to_or_lt_eq … (le_S_S_to_le … Htl)) -Htl #Htl
 127   [@le_S_S @lt_to_le @Hind //
 128   |cut (tl=[ ]) [/2 by append_l2_injective/] #eqtl >eqtl @le_n
 129   ]
 130 qed.
 131
 132 definition nat_of: ∀n. Nat_to n → nat.
 133 #n normalize * #p #_ @p
 134 qed.
 135
 136 definition bits_of_state ≝ λn.λh:Nat_to n → bool.λs:Nat_to n.
 137    map ? unialpha (λx.bit x) (h s::(to_bitlist n (nat_of n s))).
 138
 139 lemma only_bits_bits_of_state : ∀n,h,p. only_bits (bits_of_state n h p).
 140 #n #h #p #x whd in match (bits_of_state n h p);
 141 #H cases H -H
 142   [#H >H %
 143   |elim (to_bitlist n (nat_of n p))
 144     [@False_ind |#b #l #Hind #H cases H -H #H [>H % |@Hind @H ]]
 145   ]
 146 qed.
 147
 148 (******************************** action encoding *****************************)
 149
 150 definition low_char ≝ λc.
 151   match c with
 152     [ None ⇒ null
 153     | Some b ⇒ bit b
 154     ].
 155
 156 definition low_mv ≝ λm.
 157   match m with
 158   [ R ⇒ bit true
 159   | L ⇒ bit false
 160   | N ⇒ null
 161   ].
 162
 163 lemma injective_low_char: injective … low_char.
 164 #c1 #c2 cases c1 cases c2 normalize //
 165   [#b1 #H destruct
 166   |#b1 #H destruct
 167   |#b1 #b2 #H destruct //
 168   ]
 169 qed.
 170
 171 lemma injective_low_mv: injective … low_mv.
 172 #m1 #m2 cases m1 cases m2 // normalize #H destruct
 173 qed.
 174
 175 (******************************** tuple encoding ******************************)
 176 definition tuple_type ≝ λn.
 177  (Nat_to n × (option FinBool)) × (Nat_to n × (option FinBool) × move).
 178
 179 definition tuple_encoding ≝ λn.λh:Nat_to n→bool.
 180   λp:tuple_type n.
 181   let 〈inp,outp〉 ≝ p in
 182   let 〈q,a〉 ≝ inp in
 183   let 〈qn,an,m〉 ≝ outp in
 184   let qin ≝ bits_of_state n h q in
 185   let qout ≝ bits_of_state n h qn in
 186   let cin ≝ low_char a in
 187   let cout ≝ low_char an in
 188   let mv ≝ low_mv m in
 189   mk_tuple qin cin qout cout mv.
 190
 191 lemma is_tuple: ∀n,h,p. tuple_TM (S n) (tuple_encoding n h p).
 192 #n #h * * #q #a * * #qn #an #m
 193 %{(bits_of_state n h q)} %{(low_char a)}
 194 %{(bits_of_state n h qn)} %{(low_char an)} %{(low_mv m)}
 195 % // %
 196   [%[%[%[%[% /2/ |% cases a normalize [|#b] #H destruct]
 197         |% cases an normalize [|#b] #H destruct]
 198       |% cases m normalize #H destruct]
 199     |>length_map normalize @eq_f //]
 200   |>length_map normalize @eq_f //]
 201 qed.
 202
 203 definition tuple_length ≝ λn.2*n+4.
 204
 205 lemma length_of_tuple: ∀n,t. tuple_TM n t →
 206   |t| = tuple_length n.
 207 #n #t * #qin * #cin * #qout * #cout * #mv *** #_ #Hqin #Hqout #eqt
 208 >eqt normalize >length_append >Hqin -Hqin normalize >length_append
 209 normalize >Hqout //
 210 qed.
 211
 212 definition tuples_list ≝ λn.λh.map … (λp.tuple_encoding n h p).
 213
 214
 215
 216