]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/turing.ma
Definition of complexity
[helm.git] / matita / matita / lib / turing / turing.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/vectors.ma".
13
14 record tape (sig:FinSet): Type[0] ≝ 
15 { left : list sig;
16   right: list sig
17 }.
18
19 inductive move : Type[0] ≝
20 | L : move 
21 | R : move
22 | N : move. 
23
24 (* We do not distinuish an input tape *)
25
26 record TM (sig:FinSet): Type[1] ≝ 
27 { states : FinSet;
28   tapes_no: nat; (* additional working tapes *)
29   trans : states × (Vector (option sig) (S tapes_no)) → 
30     states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
31   output: list sig;
32   start: states;
33   halt : states → bool
34 }.
35
36 record config (sig:FinSet) (M:TM sig): Type[0] ≝
37 { state : states sig M;
38   tapes : Vector (tape sig) (S (tapes_no sig M));
39   out : list sig
40 }.
41
42 definition option_hd ≝ λA.λl:list A.
43   match l with
44   [nil ⇒ None ?
45   |cons a _ ⇒ Some ? a
46   ].
47
48 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
49   match \snd m with
50   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
51   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
52   | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
53   ].
54
55 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
56   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
57
58 definition opt_cons ≝ λA.λa:option A.λl:list A.
59   match a with
60   [ None ⇒ l
61   | Some a ⇒ a::l
62   ].
63
64 definition step ≝ λsig.λM:TM sig.λc:config sig M.
65   let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
66   mk_config ?? 
67     news 
68     (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
69     (opt_cons ? outchar (out ?? c)).
70
71 definition empty_tapes ≝ λsig.λn.
72 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
73 elim n // normalize //
74 qed.
75
76 definition init ≝ λsig.λM:TM sig.λi:(list sig).
77   mk_config ??
78     (start sig M)
79     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
80     [ ].
81
82 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
83   halt sig M (state sig M c).
84
85 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
86   match n with 
87   [ O ⇒ None ?
88   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
89   ].
90
91 (* Compute ? M f states that f is computed by M *)
92 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
93 ∀l.∃i.∃c.
94   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
95   out ?? c = f l.
96
97 (* for decision problems, we accept a string if on termination
98 output is not empty *)
99
100 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
101 ∀l.∃i.∃c.
102   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
103   (isnilb ? (out ?? c) = false).
104
105 (* alternative approach.
106 We define the notion of computation. The notion must be constructive,
107 since we want to define functions over it, like lenght and size 
108
109 Perche' serve Type[2] se sposto a e b a destra? *)
110
111 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
112   mk_move: p a = false → b = f a → cmove A f p a b.
113   
114 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
115 | empty : ∀a. cstar A M a a
116 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
117
118 definition computation ≝ λsig.λM:TM sig.
119   cstar ? (cmove ? (step sig M) (stop sig M)).
120
121 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
122   ∀l.∃c.computation sig M (init sig M l) c → 
123    (stop sig M c = true) ∧ out ?? c = f l.
124
125 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
126   ∀l.∃c.computation sig M (init sig M l) c → 
127    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).