matita/matita/lib/turing/multi_universal/binaryTM.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "turing/mono.ma".
  16
  17 (* given a FinSet F:
  18    - get its cardinality
  19    - return its nth element
  20    - return the index of a given element
  21  *)
  22 axiom FS_crd : FinSet → nat.
  23 axiom FS_nth : ∀F:FinSet.nat → option F.
  24 axiom index_of_FS : ∀F:FinSet.F → nat.
  25
  26 (* unary bit representation (with a given length) of a certain number *)
  27 axiom unary_of_nat : nat → nat → nat.
  28
  29 axiom FinVector : Type[0] → nat → FinSet.
  30
  31 definition binary_base_states ≝ initN 7.
  32
  33 definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 7 (refl …)).
  34 definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 7 (refl …)).
  35 definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 7 (refl …)).
  36 definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 7 (refl …)).
  37 definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 7 (refl …)).
  38 definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 7 (refl …)).
  39 definition bin6 : binary_base_states ≝ mk_Sig ?? 6 (leb_true_to_le 7 7 (refl …)).
  40
  41 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
  42  FinProd (FinProd states binary_base_states)
  43          (FinProd (FinOption sig) (initN (2 * (FS_crd sig)))).
  44
  45 axiom daemon : ∀T:Type[0].T.
  46 definition initN_pred ≝ λn.λm:initN n.(pred (pi1 … m) : initN n).
  47
  48 (* controllare i contatori, molti andranno incrementati di uno *)
  49 definition trans_binaryTM : ∀sig,states:FinSet.
  50   (states × (option sig) → states × (option sig) × move) →
  51   ((states_binaryTM sig states) × (option bool) →
  52    (states_binaryTM sig states) × (option bool) × move)
  53 ≝ λsig,states,trans,p.
  54   let 〈s,a〉 ≝ p in
  55   let 〈s0,phase,ch,count〉 ≝ s in
  56   match pi1 … phase with
  57   [ O ⇒ (*** PHASE 0: read ***)
  58       match a with
  59       [ Some a0 ⇒
  60         match count with
  61         [ O ⇒ 〈〈s0,1,ch,FS_crd sig〉,None ?,N〉
  62         | S k ⇒ if (a0 == true)
  63                 then 〈〈s0,0,FS_nth sig k,k〉, None ?,R〉
  64                 else 〈〈s0,0,ch,k〉,None ?,R〉 ]
  65       | None ⇒ (* Overflow position! *)
  66           〈〈s0,4,None ?,0〉,None ?,R〉 ]
  67   | S phase ⇒ match phase with
  68   [ O ⇒ (*** PHASE 1: restart ***)
  69       match count with
  70       [ O ⇒ 〈〈s0,2,ch,FS_crd sig〉,None ?,N〉
  71       | S k ⇒ 〈〈s0,1,ch,k〉,None ?,L〉 ]
  72   | S phase ⇒ match phase with
  73   [ O ⇒ (*** PHASE 2: write ***)
  74       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
  75       match count with
  76       [ O ⇒ let mv' ≝ match mv with [ R ⇒ N | _ ⇒ L ] in
  77             let count' ≝ match mv with [ R ⇒ 0 | N ⇒ FS_crd sig | L ⇒ 2*(FS_crd sig) ] in
  78              〈〈s',3,ch,count'〉,None ?,mv'〉
  79       | S k ⇒ match a' with
  80          [ None ⇒ 〈〈s0,2,ch,k〉,None ?,R〉
  81          | Some a0' ⇒ let out ≝ (FS_nth k == a') in
  82                       〈〈s0,2,ch,k〉,Some ? out,R〉 ]
  83       ]
  84   | S phase ⇒ match phase with
  85   [ O ⇒ (*** PHASE 3: move head left ***)
  86       match count with
  87       [ O ⇒ 〈〈s0,6,ch,O〉, None ?,N〉
  88       | S k ⇒ 〈〈s0,3,ch,k〉, None ?,L〉 ]
  89   | S phase ⇒ match phase with
  90   [ O ⇒ (*** PHASE 4: check position ***)
  91       match a with
  92       [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,2,ch,FS_crd sig〉,None ?,N〉
  93       | Some _ ⇒ (* leftof *)
  94         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
  95         match a' with
  96         [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,2,ch,0〉,None ?,N〉
  97         | Some _ ⇒ (* extend tape *) 〈〈s0,5,ch,FS_crd sig〉,None ?,L〉 ]
  98       ]
  99   | S phase ⇒ match phase with
 100   [ O ⇒ (*** PHASE 5: left extension ***)
 101       match pi1 … count with
 102       [ O ⇒ 〈〈s0,bin2,ch,FS_crd sig〉,None ?,N〉
 103       | S k ⇒ 〈〈s0,bin5,ch,k〉,Some ? false,L〉 ]
 104   | S _ ⇒ (*** PHASE 6: stop ***) 〈s,None ?,N〉 ]]]]]].
 105
 106 (*
 107  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
 108  * - ha per alfabeto FinBool
 109  * - ha stati di tipo (states … M) × (initN 3) × (initN (dimensione dell'alfabeto di M))
 110  *   dove il primo elemento corrisponde allo stato della macchina input,
 111  *   il secondo identifica la fase (lettura, scrittura, spostamento)
 112  *   il terzo è un contatore
 113  * - (la funzione di transizione è complessa al punto di rendere discutibile
 114  *)
 115 definition mk_binaryTM ≝
 116   λsig.λM:TM sig.mk_TM FinBool (FinProd (states … M) (FinProd (initN 3) (initN
 117 { no_states : nat;
 118   pos_no_states : (0 < no_states);
 119   ntrans : trans_source no_states → trans_target no_states;
 120   nhalt : initN no_states → bool
 121 }.