]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/turing/oracle.ma
progresprogresss
[helm.git] / matita / matita / lib / turing / oracle.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 "turing/turing.ma". 
13
14 (* Oracle machines *)
15
16 record TM (sig:FinSet): Type[1] ≝ 
17 { states : FinSet;
18   tapes_no: nat; (* additional working tapes *)
19   trans : states × (Vector (option sig) (S tapes_no)) → 
20     states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
21   output: list sig;
22   start: states;
23   halt : states → bool
24 }.
25
26 inductive oracle_states :Type[0] ≝
27   | query : oracle_states
28   | yes : oracle_states
29   | no : oracle_states.
30
31 record config (sig:FinSet) (M:TM sig): Type[0] ≝
32 { state : states sig M;
33   query : list sig;
34   tapes : Vector (tape sig) (S (tapes_no sig M));
35   out : list sig
36 }.
37
38 definition option_hd ≝ λA.λl:list A.
39   match l with
40   [nil ⇒ None ?
41   |cons a _ ⇒ Some ? a
42   ].
43
44 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
45   match \snd m with
46   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
47   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
48   | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
49   ].
50
51 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
52   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
53
54 definition opt_cons ≝ λA.λa:option A.λl:list A.
55   match a with
56   [ None ⇒ l
57   | Some a ⇒ a::l
58   ].
59
60 definition step ≝ λsig.λM:TM sig.λc:config sig M.
61   let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
62   mk_config ?? 
63     news 
64     (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
65     (opt_cons ? outchar (out ?? c)).
66
67 definition empty_tapes ≝ λsig.λn.
68 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
69 elim n // normalize //
70 qed.
71
72 definition init ≝ λsig.λM:TM sig.λi:(list sig).
73   mk_config ??
74     (start sig M)
75     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
76     [ ].
77
78 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
79   halt sig M (state sig M c).
80
81 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
82   match n with 
83   [ O ⇒ None ?
84   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
85   ].
86
87 (* Compute ? M f states that f is computed by M *)
88 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
89 ∀l.∃i.∃c.
90   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
91   out ?? c = f l.
92
93 (* for decision problems, we accept a string if on termination
94 output is not empty *)
95
96 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
97 ∀l.∃i.∃c.
98   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
99   (isnilb ? (out ?? c) = false).