matita/matita/lib/turing/turing_old.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/finset.ma".
  13
  14 record Vector (A:Type[0]) (n:nat): Type[0] ≝
  15 { vec :> list A;
  16   len: length ? vec = n
  17 }.
  18
  19 record TM (sig:FinSet): Type[1] ≝
  20 { states : FinSet;
  21   tapes_no: nat;
  22   trans : states × (option sig) × (Vector (option sig) tapes_no) →
  23     states × bool × (Vector (list sig) tapes_no);
  24   start: states;
  25   halt : states
  26 }.
  27
  28 definition config ≝ λsig.λM:TM sig.
  29   states sig M × (list sig) × (Vector (list sig) (tapes_no sig M)).
  30
  31 definition option_hd ≝ λA.λl:list A.
  32   match l with
  33   [nil ⇒ None ?
  34   |cons a _ ⇒ Some ? a
  35   ].
  36
  37 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
  38 #A #l elim l //
  39 qed.
  40
  41 definition vec_tail ≝ λA.λn.λv:Vector A n.
  42 mk_Vector A (pred n) (tail A v) ?.
  43 >length_tail >(len A n v) //
  44 qed.
  45
  46 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
  47 mk_Vector A (S n) (cons A a v) ?.
  48 normalize >(len A n v) //
  49 qed.
  50
  51 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
  52 #A #B #l #f elim l //
  53 qed.
  54
  55 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
  56 mk_Vector B n (map ?? f v)
  57   (trans_eq … (length_map …) (len A n v)).
  58
  59 definition hds ≝ λsig.λM.λc:config sig M. vec_map ?? (option_hd ?) (tapes_no sig M) (\snd c).
  60
  61 definition tls ≝ λsig.λM.λc:config sig M.vec_map ?? (tail ?) (tapes_no sig M) (\snd c).
  62
  63 let rec compose A B C (f:A→B→C) l1 l2 on l1 ≝
  64    match l1 with
  65    [ nil ⇒ nil C
  66    | cons a tlA ⇒
  67      match l2 with
  68      [nil ⇒ nil C
  69      |cons b tlB ⇒ (f a b)::compose A B C f tlA tlB
  70      ]
  71    ].
  72
  73 lemma length_compose: ∀A,B,C.∀f:A→B→C.∀l1,l2.
  74 length C (compose  A B C f l1 l2) =
  75   min (length A l1) (length B l2).
  76 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
  77 #b #tlB lapply (Hind tlB) normalize
  78 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
  79 normalize //
  80 qed.
  81
  82 definition compose_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
  83 mk_Vector C n (compose A B C f vA vB) ?.
  84 >length_compose >(len A n vA) >(len B n vB) normalize
  85 >(le_to_leb_true … (le_n n)) //
  86 qed.
  87
  88 definition step ≝ λsig.λM:TM sig.λc:config sig M.
  89   match (trans sig M 〈〈\fst (\fst c),option_hd ? (\snd (\fst c))〉,hds sig M c〉) with
  90   [mk_Prod p l ⇒
  91     let work_tapes ≝ compose_vec ??? (append ?) (tapes_no sig M) l (tls sig M c) in
  92     match p with
  93     [mk_Prod s b ⇒
  94       let old_input ≝ \snd (\fst c) in
  95       let input ≝ if b then tail ? old_input else  old_input in
  96       〈〈s,input〉,work_tapes〉]].
  97
  98 definition empty_tapes ≝ λsig.λM:TM sig.
  99 mk_Vector ? (tapes_no sig M) (make_list (list sig) [ ] (tapes_no sig M)) ?.
 100 elim (tapes_no sig M) // normalize //
 101 qed.
 102
 103 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 104   〈〈start sig M,i〉,empty_tapes sig M〉.
 105
 106 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 107   eqb (states sig M) (\fst(\fst c)) (halt sig M).
 108
 109 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 110   match n with
 111   [ O ⇒ None ?
 112   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 113   ].
 114
 115 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 116 ∀l.∃i.∃c.((loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c) ∧
 117   (hd ? (\snd c) [ ] = f l)).
 118
 119 (* An extended machine *)