matita/matita/lib/turing/turing.ma

   1 (*
   2
   3 Macchina A:
   4 postcondizione
   5 PA(in,out) ≝
   6   ∀ls,cs,d,rs.
   7     left (tape in) = cs@'#'::ls →
   8     right (tape in) = d::rs →
   9     state in = q0 →
  10   left (tape out) = ls ∧
  11   right (tape out) = d::'#'::rev cs@rs ∧
  12   state out = qfinal
  13
  14 Macchina A0:
  15 postcondizione:
  16 PA0(in,out) ≝
  17   ∀ls,c,rs.
  18     left (tape in) = c::ls →
  19     right (tape in) = d::rs →
  20     state in = q0 →
  21   left (tape out) = ls ∧
  22   right (tape out) = d::c::rs
  23   state out = qfinal
  24
  25 Macchina A1
  26 postcondizione true:
  27 PA1t(in,out) ≝
  28   ∀c,rs.
  29     right (tape in) = c::rs →
  30     tape in = tape out ∧
  31     (c ≠ '#' → state out = qtrue)
  32
  33 postcondizione false:
  34 PA1f(in,out) ≝
  35   ∀c,rs.
  36     right (tape in) = c::rs →
  37     tape in = tape out ∧
  38     (c = '#' → state out = qfalse) ∧
  39
  40
  41 A = do A0 while A1 inv PA0 var |right (tape in)|;
  42
  43      posso assumere le precondizioni di A
  44      H1 : left (tape in) = c::cs@'#'::ls
  45      H2 : right (tape in) = d::rs
  46
  47      in particolare H2 → precondizioni di A1
  48
  49      eseguiamo dunque if A1 then (A0; A) else skip
  50
  51
  52
  53 by induction on left (tape in)
  54
  55      per casi su d =?= '#'
  56
  57      Hcase: d ≠ '#' ⇒
  58      eseguo (A1; A0; A)
  59      devo allora provare che PA1°PA0°PA(in,out) → PA(in,out)
  60      ∃s1,s2: PA1t(in,s1) ∧ PA0(s1,s2) ∧ PA(s2,out)
  61
  62      usando anche Hcase, ottengo che tape in = tape s1
  63      soddisfo allora le precondizioni di PA0(s1,s2) ottenendo che
  64      left (tape s2) = cs@'#'::ls
  65      right (tape s2) = d::c::rs
  66
  67      soddisfo allora le precondizioni di PA e per ipotesi induttiva
  68
  69
  70      left (tape s) = d::cs@'#'::ls
  71      right (tape s) =
  72
  73
  74
  75
  76
  77
  78
  79
  80 ∀inc.
  81   (∃ls,cs,d,rs. left inc = ... ∧ right inc = ... ∧ state inc = q0) →
  82 ∃i,outc. loop i step inc = Some ? outc
  83   ∧(∀ls,cs,d,rs.left inc = ... → right inc = ... →
  84     ∧ left outc = ls
  85     ∧ right outc = d::"#"::rev cs::rs
  86     ∧ state outc = qfinal)
  87
  88 ϕ1 M1 ψ1 → ϕ2 M2 ψ2 →
  89 (ψ1(in1,out1) → ϕ2(out1)) → (ψ2(out1,out2) → ψ3(in1,out2)) →
  90 ϕ1 (M1;M2) ψ3
  91
  92
  93
  94 -----------------------------------------------------
  95 {} (tmp ≝ x; x ≝ y; y ≝ tmp) {x = old(x), y = old(y)}
  96
  97
  98 ∀inc.
  99   ∀ls:list sig.
 100   ∀cs:list (sig\#).
 101   ∀d.sig.
 102   ∀rs:list sig.
 103   left inc = cs@"#"::ls →
 104   right inc = d::rs →
 105   state inc = q0 →
 106 ∃i,outc. loop i step inc = Some outc
 107   ∧
 108   (∀ls,cs,d,rs.left inc = ... → right inc = ... →
 109   ∧ left outc = ls
 110   ∧ right outc = d::"#"::rev cs::rs
 111   ∧ state outc = qfinal
 112
 113 *)
 114
 115
 116 (*
 117     ||M||  This file is part of HELM, an Hypertextual, Electronic
 118     ||A||  Library of Mathematics, developed at the Computer Science
 119     ||T||  Department of the University of Bologna, Italy.
 120     ||I||
 121     ||T||
 122     ||A||
 123     \   /  This file is distributed under the terms of the
 124      \ /   GNU General Public License Version 2
 125       V_____________________________________________________________*)
 126
 127 include "basics/vectors.ma".
 128
 129 record tape (sig:FinSet): Type[0] ≝
 130 { left : list sig;
 131   right: list sig
 132 }.
 133
 134 inductive move : Type[0] ≝
 135 | L : move
 136 | R : move
 137 | N : move.
 138
 139 (* We do not distinuish an input tape *)
 140
 141 record TM (sig:FinSet): Type[1] ≝
 142 { states : FinSet;
 143   tapes_no: nat; (* additional working tapes *)
 144   trans : states × (Vector (option sig) (S tapes_no)) →
 145     states  × (Vector (sig × move) (S tapes_no)) × (option sig) ;
 146   output: list sig;
 147   start: states;
 148   halt : states → bool
 149 }.
 150
 151 record config (sig:FinSet) (M:TM sig): Type[0] ≝
 152 { state : states sig M;
 153   tapes : Vector (tape sig) (S (tapes_no sig M));
 154   out : list sig
 155 }.
 156
 157 definition option_hd ≝ λA.λl:list A.
 158   match l with
 159   [nil ⇒ None ?
 160   |cons a _ ⇒ Some ? a
 161   ].
 162
 163 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
 164   match \snd m with
 165   [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
 166   | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
 167   | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
 168   ].
 169
 170 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
 171   vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
 172
 173 definition opt_cons ≝ λA.λa:option A.λl:list A.
 174   match a with
 175   [ None ⇒ l
 176   | Some a ⇒ a::l
 177   ].
 178
 179 definition step ≝ λsig.λM:TM sig.λc:config sig M.
 180   let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
 181   mk_config ??
 182     news
 183     (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
 184     (opt_cons ? outchar (out ?? c)).
 185
 186 definition empty_tapes ≝ λsig.λn.
 187 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 188 elim n // normalize //
 189 qed.
 190
 191 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 192   mk_config ??
 193     (start sig M)
 194     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 195     [ ].
 196
 197 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 198   halt sig M (state sig M c).
 199
 200 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 201   match n with
 202   [ O ⇒ None ?
 203   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 204   ].
 205
 206 (* Compute ? M f states that f is computed by M *)
 207 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 208 ∀l.∃i.∃c.
 209   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 210   out ?? c = f l.
 211
 212 (* for decision problems, we accept a string if on termination
 213 output is not empty *)
 214
 215 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 216 ∀l.∃i.∃c.
 217   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 218   (isnilb ? (out ?? c) = false).
 219
 220 (* alternative approach.
 221 We define the notion of computation. The notion must be constructive,
 222 since we want to define functions over it, like lenght and size
 223
 224 Perche' serve Type[2] se sposto a e b a destra? *)
 225
 226 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 227   mk_move: p a = false → b = f a → cmove A f p a b.
 228
 229 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 230 | empty : ∀a. cstar A M a a
 231 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 232
 233 definition computation ≝ λsig.λM:TM sig.
 234   cstar ? (cmove ? (step sig M) (stop sig M)).
 235
 236 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 237   ∀l.∃c.computation sig M (init sig M l) c →
 238    (stop sig M c = true) ∧ out ?? c = f l.
 239
 240 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 241   ∀l.∃c.computation sig M (init sig M l) c →
 242    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).