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