matita/matita/lib/turing/ntm.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/star.ma".
  13 include "turing/turing.ma".
  14
  15 (*
  16 record Vector (A:Type[0]) (n:nat): Type[0] ≝
  17 { vec :> list A;
  18   len: length ? vec = n
  19 }.
  20
  21 record tape (sig:FinSet): Type[0] ≝
  22 { left : list sig;
  23   right: list sig
  24 }.
  25
  26 inductive move : Type[0] ≝
  27 | L : move
  28 | R : move
  29 | N : move
  30 .
  31 *)
  32
  33 record NTM (sig:FinSet): Type[1] ≝
  34 { states : FinSet;
  35   tapes_no: nat; (* additional working tapes *)
  36   trans : list ((states × (Vector (option sig) (S tapes_no))) ×
  37     (states  × (Vector (sig × move) (S tapes_no))));
  38   output: list sig;
  39   start: states;
  40   halt : states → bool;
  41   accept : states → bool
  42 }.
  43
  44 record config (sig:FinSet) (M:NTM sig): Type[0] ≝
  45 { state : states sig M;
  46   tapes : Vector (tape sig) (S (tapes_no sig M))
  47 }.
  48
  49 (*
  50 definition option_hd ≝ λA.λl:list A.
  51   match l with
  52   [nil ⇒ None ?
  53   |cons a _ ⇒ Some ? a
  54   ].
  55
  56 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
  57 #A #l elim l //
  58 qed.
  59
  60 definition vec_tail ≝ λA.λn.λv:Vector A n.
  61 mk_Vector A (pred n) (tail A v) ?.
  62 >length_tail >(len A n v) //
  63 qed.
  64
  65 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
  66 mk_Vector A (S n) (cons A a v) ?.
  67 normalize >(len A n v) //
  68 qed.
  69
  70 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
  71 #A #B #l #f elim l // #a #tl #Hind normalize //
  72 qed.
  73
  74 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
  75 mk_Vector B n (map ?? f v)
  76   (trans_eq … (length_map …) (len A n v)).
  77
  78 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
  79   match \snd m with
  80   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
  81   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
  82   ].
  83 *)
  84
  85 (*
  86 definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
  87
  88 definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
  89 *)
  90 (*
  91 let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
  92    match l1 with
  93    [ nil ⇒ nil C
  94    | cons a tlA ⇒
  95      match l2 with
  96      [nil ⇒ nil C
  97      |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
  98      ]
  99    ].
 100
 101 lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
 102 length C (compose  A B C f l1 l2) =
 103   min (length A l1) (length B l2).
 104 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
 105 #b #tlB lapply (Hind tlB) normalize
 106 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
 107 normalize //
 108 qed.
 109
 110 definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
 111 mk_Vector C n (compose A B C f vA vB) ?.
 112 >length_compose >(len A n vA) >(len B n vB) normalize
 113 >(le_to_leb_true … (le_n n)) //
 114 qed.
 115 *)
 116
 117 definition current_chars ≝ λsig.λM:NTM sig.λc:config sig M.
 118   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
 119
 120 let rec mem A (a:A) (l:list A) on l ≝
 121   match l with
 122   [ nil ⇒ False
 123   | cons hd tl ⇒ a=hd ∨ mem A a tl
 124   ].
 125
 126 definition reach ≝ λsig.λM:NTM sig.λc,c1:config sig M.
 127   ∃q,l,q1,mvs.
 128     state ?? c = q ∧
 129     halt ?? q = false ∧
 130     current_chars ?? c = l ∧
 131     mem ? 〈〈q,l〉,〈q1,mvs〉〉 (trans ? M)  ∧
 132     state ?? c1 = q1 ∧
 133     tapes ?? c1 = (compose_vec ??? (tape_move sig) ? (tapes ?? c) mvs).
 134
 135 (*
 136 definition empty_tapes ≝ λsig.λn.
 137 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 138 elim n // normalize //
 139 qed.
 140 *)
 141
 142 definition init ≝ λsig.λM:NTM sig.λi:(list sig).
 143   mk_config ??
 144     (start sig M)
 145     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M))).
 146
 147 definition accepted ≝ λsig.λM:NTM sig.λw:(list sig).
 148 ∃c. star ? (reach sig M) (init sig M w) c ∧
 149   accept ?? (state ?? c) = true.
 150