]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/turing_old.ma
sempre li
[helm.git] / matita / matita / lib / turing / turing_old.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 "basics/finset.ma".
13
14 record Vector (A:Type[0]) (n:nat): Type[0] ≝ 
15 { vec :> list A;
16   len: length ? vec = n
17 }.
18
19 record TM (sig:FinSet): Type[1] ≝ 
20 { states : FinSet;
21   tapes_no: nat;
22   trans : states × (option sig) × (Vector (option sig) tapes_no) → 
23     states × bool × (Vector (list sig) tapes_no);
24   start: states;
25   halt : states
26 }.
27
28 definition config ≝ λsig.λM:TM sig.
29   states sig M × (list sig) × (Vector (list sig) (tapes_no sig M)).
30
31 definition option_hd ≝ λA.λl:list A.
32   match l with
33   [nil ⇒ None ?
34   |cons a _ ⇒ Some ? a
35   ].
36
37 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
38 #A #l elim l // 
39 qed.
40
41 definition vec_tail ≝ λA.λn.λv:Vector A n.
42 mk_Vector A (pred n) (tail A v) ?.
43 >length_tail >(len A n v) //
44 qed.
45
46 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
47 mk_Vector A (S n) (cons A a v) ?.
48 normalize >(len A n v) //
49 qed.
50
51 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
52 #A #B #l #f elim l // #a #tl #Hind normalize //
53 qed.
54
55 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
56 mk_Vector B n (map ?? f v) 
57   (trans_eq … (length_map …) (len A n v)).
58   
59 definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
60
61 definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
62
63 let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
64    match l1 with
65    [ nil ⇒ nil C
66    | cons a tlA ⇒ 
67      match l2 with
68      [nil ⇒ nil C
69      |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
70      ]
71    ].
72
73 lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
74 length C (compose  A B C f l1 l2) = 
75   min (length A l1) (length B l2).
76 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
77 #b #tlB lapply (Hind tlB) normalize 
78 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
79 normalize //
80 qed.
81
82 definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
83 mk_Vector C n (compose A B C f vA vB) ?.
84 >length_compose >(len A n vA) >(len B n vB) normalize 
85 >(le_to_leb_true … (le_n n)) //
86 qed.
87
88 definition step ≝ λsig.λM:TM sig.λc:config sig M.
89   match (trans sig M 〈〈\fst (\fst c),option_hd ? (\snd (\fst c))〉,hds sig M c〉) with
90   [mk_Prod p l ⇒ 
91     let work_tapes ≝ compose_vec ??? (append ?) (tapes_no sig M) l (tls sig M c) in
92     match p with 
93     [mk_Prod s b ⇒ 
94       let old_input ≝ \snd (\fst c) in
95       let input ≝ if b then tail ? old_input else  old_input in
96       〈〈s,input〉,work_tapes〉]].
97
98 definition empty_tapes ≝ λsig.λM:TM sig.
99 mk_Vector ? (tapes_no sig M) (make_list (list sig) [ ] (tapes_no sig M)) ?.
100 elim (tapes_no sig M) // normalize //
101 qed.
102
103 definition init ≝ λsig.λM:TM sig.λi:(list sig).
104   〈〈start sig M,i〉,empty_tapes sig M〉.
105
106 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
107   eqb (states sig M) (\fst(\fst c)) (halt sig M).
108
109 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
110   match n with 
111   [ O ⇒ None ?
112   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
113   ].
114
115 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
116 ∀l.∃i.∃c.((loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c) ∧
117   (hd ? (\snd c) [ ] = f l)).
118
119 (* An extended machine *)