1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "turing/mono.ma".
19 - return its nth element
20 - return the index of a given element
22 axiom FS_crd : FinSet → nat.
23 axiom FS_nth : ∀F:FinSet.nat → option F.
24 axiom index_of_FS : ∀F:FinSet.F → nat.
26 (* unary bit representation (with a given length) of a certain number *)
27 axiom unary_of_nat : nat → nat → nat.
29 axiom FinVector : Type[0] → nat → FinSet.
31 definition binary_base_states ≝ initN 7.
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 …)).
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)))).
45 axiom daemon : ∀T:Type[0].T.
46 definition initN_pred ≝ λn.λm:initN n.(pred (pi1 … m) : initN n).
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.
55 let 〈s0,phase,ch,count〉 ≝ s in
56 match pi1 … phase with
57 [ O ⇒ (*** PHASE 0: read ***)
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 ***)
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
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'〉
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〉 ]
84 | S phase ⇒ match phase with
85 [ O ⇒ (*** PHASE 3: move head left ***)
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 ***)
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
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〉 ]
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〉 ]]]]]].
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
115 definition mk_binaryTM ≝
116 λsig.λM:TM sig.mk_TM FinBool (FinProd (states … M) (FinProd (initN 3) (initN
118 pos_no_states : (0 < no_states);
119 ntrans : trans_source no_states → trans_target no_states;
120 nhalt : initN no_states → bool