]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/multi_universal/binaryTM.ma
Starting proof about semantics of binary machines.
[helm.git] / 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 → (list bool).
28
29 axiom FinVector : Type[0] → nat → FinSet.
30
31 definition binary_base_states ≝ initN 6.
32
33 definition bin0 : binary_base_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 6 (refl …)).
34 definition bin1 : binary_base_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 6 (refl …)).
35 definition bin2 : binary_base_states ≝ mk_Sig ?? 2 (leb_true_to_le 3 6 (refl …)).
36 definition bin3 : binary_base_states ≝ mk_Sig ?? 3 (leb_true_to_le 4 6 (refl …)).
37 definition bin4 : binary_base_states ≝ mk_Sig ?? 4 (leb_true_to_le 5 6 (refl …)).
38 definition bin5 : binary_base_states ≝ mk_Sig ?? 5 (leb_true_to_le 6 6 (refl …)).
39
40 definition states_binaryTM : FinSet → FinSet → FinSet ≝ λsig,states.
41  FinProd (FinProd states binary_base_states) 
42          (FinProd (FinOption sig) (initN (S (2 * (FS_crd sig))))).
43
44 axiom daemon : ∀T:Type[0].T.
45
46 definition to_initN : ∀n,m.n < m → initN m ≝ λn,m,Hn.mk_Sig … n ….// qed.
47
48 definition initN_pred : ∀n.∀m:initN n.initN n ≝ λn,m.mk_Sig … (pred (pi1 … m)) …. 
49 cases m #m0 /2 by le_to_lt_to_lt/ qed.
50
51 (* controllare i contatori, molti andranno incrementati di uno *)
52 definition trans_binaryTM : ∀sig,states:FinSet.
53   (states × (option sig) → states × (option sig) × move) → 
54   ((states_binaryTM sig states) × (option bool) → 
55    (states_binaryTM sig states) × (option bool) × move) 
56 ≝ λsig,states,trans,p.
57   let 〈s,a〉 ≝ p in
58   let 〈s0,phase,ch,count〉 ≝ s in
59   let (H1 : O < S (2*FS_crd sig)) ≝ ? in
60   let (H2 : FS_crd sig < S (2*FS_crd sig)) ≝ ? in
61   match pi1 … phase with
62   [ O ⇒ (*** PHASE 0: read ***)
63       match a with
64       [ Some a0 ⇒ 
65         match pi1 … count with
66         [ O ⇒ 〈〈s0,bin1,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
67         | S k ⇒ if (a0 == true) 
68                 then 〈〈s0,bin0,FS_nth sig k,initN_pred … count〉, None ?,R〉
69                 else 〈〈s0,bin0,ch,initN_pred … count〉,None ?,R〉 ]
70       | None ⇒ (* Overflow position! *)
71           〈〈s0,bin4,None ?,to_initN 0 ? H1〉,None ?,R〉 ]
72   | S phase ⇒ match phase with
73   [ O ⇒ (*** PHASE 1: restart ***)
74       match pi1 … count with
75       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
76       | S k ⇒ 〈〈s0,bin1,ch,initN_pred … count〉,None ?,L〉 ]
77   | S phase ⇒ match phase with
78   [ O ⇒ (*** PHASE 2: write ***)
79       let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
80       match pi1 … count with
81       [ O ⇒ let mv' ≝ match mv with [ R ⇒ N | _ ⇒ L ] in
82             let count' ≝ match mv with [ R ⇒ 0 | N ⇒ FS_crd sig | L ⇒ 2*(FS_crd sig) ] in
83              〈〈s',bin3,ch,to_initN count' ??〉,None ?,mv'〉
84       | S k ⇒ match a' with
85          [ None ⇒ 〈〈s0,bin2,ch,initN_pred … count〉,None ?,R〉
86          | Some a0' ⇒ let out ≝ (FS_nth ? k == a') in
87                       〈〈s0,bin2,ch,initN_pred … count〉,Some ? out,R〉 ]
88       ]
89   | S phase ⇒ match phase with
90   [ O ⇒ (*** PHASE 3: move head left ***)
91       match pi1 … count with
92       [ O ⇒ 〈〈s0,bin0,None ?,to_initN (FS_crd sig) ? H2〉, None ?,N〉 (* the end: restart *)
93       | S k ⇒ 〈〈s0,bin3,ch,initN_pred … count〉, None ?,L〉 ]
94   | S phase ⇒ match phase with
95   [ O ⇒ (*** PHASE 4: check position ***)
96       match a with
97       [ None ⇒ (* niltape/rightof: we can write *) 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
98       | Some _ ⇒ (* leftof *)
99         let 〈s',a',mv〉 ≝ trans 〈s0,ch〉 in
100         match a' with
101         [ None ⇒ (* we don't write anything: go to end of 2 *) 〈〈s0,bin2,ch,to_initN 0 ? H1〉,None ?,N〉
102         | Some _ ⇒ (* extend tape *) 〈〈s0,bin5,ch,to_initN (FS_crd sig) ? H2〉,None ?,L〉 ]
103       ]
104   | S _ ⇒ (*** PHASE 5: left extension ***)
105       match pi1 … count with
106       [ O ⇒ 〈〈s0,bin2,ch,to_initN (FS_crd sig) ? H2〉,None ?,N〉
107       | S k ⇒ 〈〈s0,bin5,ch,initN_pred … count〉,Some ? false,L〉 ]]]]]].
108 [2,3: //]
109 whd in match count'; cases mv whd in ⊢ (?%?); //
110 qed.
111
112 definition halt_binaryTM : ∀sig,M.states_binaryTM sig (states sig M) → bool ≝ 
113   λsig,M,s.let 〈s0,phase,ch,count〉 ≝ s in
114   pi1 … phase == O ∧ halt sig M s0.
115
116 (*
117  * Una mk_binaryTM prende in input una macchina M e produce una macchina che:
118  * - ha per alfabeto FinBool
119  * - ha stati di tipo ((states … M) × (initN 7)) × 
120        ((option sig) × (initN (2*dimensione dell'alfabeto di M + 1))
121  *   dove il primo elemento corrisponde allo stato della macchina input,
122  *   il secondo identifica la fase (lettura, scrittura, spostamento)
123  *   il terzo identifica il carattere oggetto letto
124  *   il quarto è un contatore
125  * - la funzione di transizione viene prodotta da trans_binaryTM
126  * - la funzione di arresto viene prodotta da halt_binaryTM
127  *)
128 definition mk_binaryTM ≝ 
129   λsig.λM:TM sig.
130   mk_TM FinBool (states_binaryTM sig (states sig M)) 
131     (trans_binaryTM sig (states sig M) (trans sig M)) 
132     (〈start sig M,bin0,None ?,FS_crd sig〉) (halt_binaryTM sig M).// qed.
133
134 definition bin_current ≝ λsig,t.match current ? t with
135 [ None ⇒ [ ] | Some c ⇒ unary_of_nat (FS_crd sig) (index_of_FS sig c) ].
136
137 definition tape_bin_lift ≝ λsig,t.
138 let ls' ≝ flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (left ? t)) in
139 let c' ≝ option_hd ? (bin_current sig t) in
140 let rs' ≝ tail ? (bin_current sig t)@flatten ? (map ?? (unary_of_nat (FS_crd sig) ∘ (index_of_FS sig)) (right ? t)) in
141  mk_tape ? ls' c' rs'.
142
143 definition R_bin_lift ≝ λsig,R,t1,t2.
144   ∃u1.t1 = tape_bin_lift sig u1 → 
145   ∃u2.t2 = tape_bin_lift sig u2 ∧ R u1 u2.
146   
147 definition state_bin_lift :
148   ∀sig.∀M:TM sig.states sig M → states ? (mk_binaryTM ? M)
149  ≝ λsig,M,q.〈q,bin0,None ?,FS_crd sig〉.// qed.
150
151 lemma binaryTM_loop :
152  ∀sig,M,i,t,q,tf,qf.
153  loopM sig M i (mk_config ?? q t) = Some ? (mk_config ?? qf tf) →
154  ∃k.loopM ? (mk_binaryTM sig M) k 
155   (mk_config ?? (state_bin_lift ? M q) (tape_bin_lift ? t)) = 
156   Some ? (mk_config ?? (state_bin_lift ? M qf) (tape_bin_lift ? tf)).
157 #sig #M #i elim i
158 [ #t #q #qf #tf change with (None ?) in ⊢ (??%?→?); #H destruct (H)
159 | -i #i #IH #t #q #tf #qf
160
161
162 (*
163 theorem sem_binaryTM : ∀sig,M.
164   mk_binaryTM sig M ⊫ R_bin_lift ? (R_TM ? M (start ? M)).
165 #sig #M #t #i generalize in match t; -t
166 @(nat_elim1 … i) #m #IH #intape #outc #Hloop
167
168 *)