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).