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