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 axiom loop_incr : ∀A,f,p,k1,k2,a1,a2.
  67   loop A k1 f p a1 = Some ? a2 →
  68     loop A (k2+k1) f p a1 = Some ? a2.
  69
  70 axiom loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
  71  ∀k1,k2,a1,a2,a3,a4.
  72    loop A k1 f p a1 = Some ? a2 → f a2 = a3 →
  73      loop A k2 f q a3 = Some ? a4 →
  74        loop A (k1+k2) f q a1 = Some ? a4.
  75
  76 (*
  77 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
  78  ∀k1,k2,a1,a2,a3.
  79    loop A k1 f p a1 = Some ? a2 →
  80      loop A k2 f q a2 = Some ? a3 →
  81        loop A (k1+k2) f q a1 = Some ? a3.
  82 #Sig #f #p #q #Hpq #k1 elim k1
  83   [normalize #k2 #a1 #a2 #a3 #H destruct
  84   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
  85    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
  86    [#eqa1a2 destruct #H @loop_incr //
  87    |normalize >(Hpq … pa1) normalize
  88     #H1 #H2 @(Hind … H2) //
  89    ]
  90  ]
  91 qed.
  92 *)
  93
  94 definition initc ≝ λsig.λM:TM sig.λt.
  95   mk_config sig M (start sig M) t.
  96
  97 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
  98 ∀t.∃i.∃outc.
  99   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 100   R t (ctape ?? outc).
 101
 102 (* Compositions *)
 103
 104 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 105 λp. let 〈s,a〉 ≝ p in
 106   match s with
 107   [ inl s1 ⇒
 108       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 109       else
 110       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 111       〈inl … news1,m〉
 112   | inr s2 ⇒
 113       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 114       〈inr … news2,m〉
 115   ].
 116
 117 definition seq ≝ λsig. λM1,M2 : TM sig.
 118   mk_TM sig
 119     (FinSum (states sig M1) (states sig M2))
 120     (seq_trans sig M1 M2)
 121     (inl … (start sig M1))
 122     (λs.match s with
 123       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 124
 125 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 126   ∃am.R1 a1 am ∧ R2 am a2.
 127
 128 (*
 129 definition injectRl ≝ λsig.λM1.λM2.λR.
 130    λc1,c2. ∃c11,c12.
 131      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 132      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 133      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 134      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 135      R c11 c12.
 136
 137 definition injectRr ≝ λsig.λM1.λM2.λR.
 138    λc1,c2. ∃c21,c22.
 139      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 140      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 141      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 142      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 143      R c21 c22.
 144
 145 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 146   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 147   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 148   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 149
 150 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 151
 152 definition lift_confL ≝
 153   λsig,M1,M2,c.match c with
 154   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 155 definition lift_confR ≝
 156   λsig,M1,M2,c.match c with
 157   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 158
 159 definition halt_liftL ≝
 160   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 161   match s with
 162   [ inl s1 ⇒ halt sig M1 s1
 163   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 164
 165 axiom loop_dec : ∀A,k1,k2,f,p,q,a1,a2,a3.
 166   loop A k1 f p a1 = Some ? a2 →
 167     loop A k2 f q a2 = Some ? a3 →
 168       loop A (k1+k2) f q a1 = Some ? a3.
 169
 170 lemma p_halt_liftL : ∀sig,M1,M2,c.
 171   halt sig M1 (cstate … c) =
 172      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 173 #sig #M1 #M2 #c cases c #s #t %
 174 qed.
 175
 176 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 177   halt ? M1 s = false →
 178   trans sig M1 〈s,a〉 = 〈news,move〉 →
 179   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 180 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 181 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 182 qed.
 183
 184 lemma config_eq :
 185   ∀sig,M,c1,c2.
 186   cstate sig M c1 = cstate sig M c2 →
 187   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 188 #sig #M1 * #s1 #t1 * #s2 #t2 //
 189 qed.
 190
 191 lemma step_lift_confL : ∀sig,M1,M2,c0.
 192  halt ? M1 (cstate ?? c0) = false →
 193  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 194  lift_confL sig M1 M2 (step sig M1 c0).
 195 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 196 #rs #Hhalt
 197 whd in ⊢ (???(????%));whd in ⊢ (???%);
 198 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 199 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 200 #s0 #m0 #Heq whd in ⊢ (???%);
 201 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 202 >(trans_liftL … Heq)
 203 [% | //]
 204 qed.
 205
 206 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 207   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 208     loop ? k (step sig (seq sig M1 M2))
 209       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 210     Some ? (lift_confL … c2).
 211 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 212 elim k
 213 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 214 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 215  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 216  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 217  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 218    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 219    | // ]
 220  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 221    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 222     @step_lift_confL //
 223    | // ]
 224 qed.
 225
 226 axiom loop_liftR : ∀sig,k,M1,M2,c1,c2.
 227   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 228     loop ? k (step sig (seq sig M1 M2))
 229       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 230     Some ? (lift_confR … c2).
 231
 232 axiom loop_Some :
 233   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 234
 235 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 236   halt ? M1 s = true →
 237   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 238 #sig #M1 #M2 #s #a
 239 #Hhalt whd in ⊢ (??%?); >Hhalt %
 240 qed.
 241
 242 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 243   Realize sig M1 R1 → Realize sig M2 R2 →
 244     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 245 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 246 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 247 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 248 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 249 %
 250 [@(loop_split ??????????? (loop_liftL … Hloop1))
 251  [* *
 252    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 253    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 254  |
 255  |4:@(loop_liftR … Hloop2)
 256  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 257   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 258   >(trans_liftL_true sig M1 M2 ??)
 259   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 260     @config_eq //
 261   | @(loop_Some ?????? Hloop10) ]
 262  ]
 263 | STOP! (* ... *)
 264 ]
 265
 266 definition empty_tapes ≝ λsig.λn.
 267 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 268 elim n // normalize //
 269 qed.
 270
 271 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 272   mk_config ??
 273     (start sig M)
 274     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 275     [ ].
 276
 277 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 278   halt sig M (state sig M c).
 279
 280 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 281   match n with
 282   [ O ⇒ None ?
 283   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 284   ].
 285
 286 (* Compute ? M f states that f is computed by M *)
 287 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 288 ∀l.∃i.∃c.
 289   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 290   out ?? c = f l.
 291
 292 (* for decision problems, we accept a string if on termination
 293 output is not empty *)
 294
 295 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 296 ∀l.∃i.∃c.
 297   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 298   (isnilb ? (out ?? c) = false).
 299
 300 (* alternative approach.
 301 We define the notion of computation. The notion must be constructive,
 302 since we want to define functions over it, like lenght and size
 303
 304 Perche' serve Type[2] se sposto a e b a destra? *)
 305
 306 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 307   mk_move: p a = false → b = f a → cmove A f p a b.
 308
 309 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 310 | empty : ∀a. cstar A M a a
 311 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 312
 313 definition computation ≝ λsig.λM:TM sig.
 314   cstar ? (cmove ? (step sig M) (stop sig M)).
 315
 316 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 317   ∀l.∃c.computation sig M (init sig M l) c →
 318    (stop sig M c = true) ∧ out ?? c = f l.
 319
 320 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 321   ∀l.∃c.computation sig M (init sig M l) c →
 322    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).