matita/matita/lib/turing/mono.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 (* include "basics/relations.ma". *)
  14
  15 record tape (sig:FinSet): Type[0] ≝
  16 { left : list sig;
  17   right: list sig
  18 }.
  19
  20 inductive move : Type[0] ≝
  21 | L : move
  22 | R : move
  23 .
  24
  25 (* We do not distinuish an input tape *)
  26
  27 record TM (sig:FinSet): Type[1] ≝
  28 { states : FinSet;
  29   trans : states × (option sig) → states × (option (sig × move));
  30   start: states;
  31   halt : states → bool
  32 }.
  33
  34 record config (sig:FinSet) (M:TM sig): Type[0] ≝
  35 { cstate : states sig M;
  36   ctape: tape sig
  37 }.
  38
  39 definition option_hd ≝ λA.λl:list A.
  40   match l with
  41   [nil ⇒ None ?
  42   |cons a _ ⇒ Some ? a
  43   ].
  44
  45 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
  46   match m with
  47   [ None ⇒ t
  48   | Some m1 ⇒
  49     match \snd m1 with
  50     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
  51     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
  52     ]
  53   ].
  54
  55 definition step ≝ λsig.λM:TM sig.λc:config sig M.
  56   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
  57   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
  58   mk_config ?? news (tape_move sig (ctape ?? c) mv).
  59
  60 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
  61   match n with
  62   [ O ⇒ None ?
  63   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
  64   ].
  65
  66 definition initc ≝ λsig.λM:TM sig.λt.
  67   mk_config sig M (start sig M) t.
  68
  69 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
  70 ∀t.∃i.∃outc.
  71   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
  72   R t (ctape ?? outc).
  73
  74 (* Compositions *)
  75
  76 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
  77 λp. let 〈s,a〉 ≝ p in
  78   match s with
  79   [ inl s1 ⇒
  80       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
  81       else
  82       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
  83       〈inl … news1,m〉
  84   | inr s2 ⇒
  85       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
  86       〈inr … news2,m〉
  87   ].
  88
  89 definition seq ≝ λsig. λM1,M2 : TM sig.
  90   mk_TM sig
  91     (FinSum (states sig M1) (states sig M2))
  92     (seq_trans sig M1 M2)
  93     (inl … (start sig M1))
  94     (λs.match s with
  95       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
  96
  97 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
  98   ∃am.R1 a1 am ∧ R2 am a2.
  99
 100 (*
 101 definition injectRl ≝ λsig.λM1.λM2.λR.
 102    λc1,c2. ∃c11,c12.
 103      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 104      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 105      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 106      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 107      R c11 c12.
 108
 109 definition injectRr ≝ λsig.λM1.λM2.λR.
 110    λc1,c2. ∃c21,c22.
 111      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 112      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 113      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 114      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 115      R c21 c22.
 116
 117 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 118   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 119   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 120   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 121
 122 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 123
 124 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 125   Realize sig M1 R1 → Realize sig M2 R2 →
 126     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 127 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 128 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 129 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 130 @(ex_intro … (S(k1+k2))) @
 131
 132
 133
 134
 135 definition empty_tapes ≝ λsig.λn.
 136 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 137 elim n // normalize //
 138 qed.
 139
 140 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 141   mk_config ??
 142     (start sig M)
 143     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 144     [ ].
 145
 146 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 147   halt sig M (state sig M c).
 148
 149 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 150   match n with
 151   [ O ⇒ None ?
 152   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 153   ].
 154
 155 (* Compute ? M f states that f is computed by M *)
 156 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 157 ∀l.∃i.∃c.
 158   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 159   out ?? c = f l.
 160
 161 (* for decision problems, we accept a string if on termination
 162 output is not empty *)
 163
 164 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 165 ∀l.∃i.∃c.
 166   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 167   (isnilb ? (out ?? c) = false).
 168
 169 (* alternative approach.
 170 We define the notion of computation. The notion must be constructive,
 171 since we want to define functions over it, like lenght and size
 172
 173 Perche' serve Type[2] se sposto a e b a destra? *)
 174
 175 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 176   mk_move: p a = false → b = f a → cmove A f p a b.
 177
 178 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 179 | empty : ∀a. cstar A M a a
 180 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 181
 182 definition computation ≝ λsig.λM:TM sig.
 183   cstar ? (cmove ? (step sig M) (stop sig M)).
 184
 185 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 186   ∀l.∃c.computation sig M (init sig M l) c →
 187    (stop sig M c = true) ∧ out ?? c = f l.
 188
 189 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 190   ∀l.∃c.computation sig M (init sig M l) c →
 191    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).