matita/matita/lib/turing/universal/copy.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
  13 (* COMPARE BIT
  14
  15 *)
  16
  17 include "turing/universal/tuples.ma".
  18
  19 definition write_states ≝ initN 2.
  20
  21 definition write ≝ λalpha,c.
  22   mk_TM alpha write_states
  23   (λp.let 〈q,a〉 ≝ p in
  24     match q with
  25     [ O ⇒ 〈1,Some ? 〈c,N〉〉
  26     | S _ ⇒ 〈1,None ?〉 ])
  27   O (λx.x == 1).
  28
  29 definition R_write ≝ λalpha,c,t1,t2.
  30   ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
  31
  32 axiom sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
  33
  34 definition copy_step_subcase ≝
  35   λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
  36     (seq (FinProd alpha FinBool) (adv_mark_r …)
  37       (seq ? (move_l …)
  38         (seq ? (adv_to_mark_l … (is_marked alpha))
  39           (seq ? (write ? 〈c,false〉)
  40             (seq ? (move_r …)
  41               (seq ? (mark …)
  42                 (seq ? (move_r …) (adv_to_mark_r … (is_marked alpha)))))))))
  43     elseM tc_true.
  44
  45 definition R_copy_step_subcase ≝
  46   λalpha,c,RelseM,t1,t2.
  47     ∀ls,x,rs.t1 = midtape (FinProd … alpha FinBool) ls 〈x,true〉 rs →
  48     (x = c ∧
  49      ∀a,l1,x0,a0,l2,l3. (∀c.memb ? c l1 = true → is_marked ? c = false) →
  50      ls = l1@〈a0,false〉::〈x0,true〉::l2 →
  51      rs = 〈a,false〉::l3 →
  52      t2 = midtape ? (〈x,false〉::l1@〈a0,true〉::〈x,false〉::l2) 〈a,true〉 l3) ∨
  53     (x ≠ c ∧ RelseM t1 t2).
  54
  55 axiom sem_copy_step_subcase :
  56   ∀alpha,c,elseM,RelseM.
  57   Realize ? (copy_step_subcase alpha c elseM) (R_copy_step_subcase alpha c RelseM).
  58
  59 (*
  60 if current = 0,tt
  61    then advance_mark_r;
  62         move_l;
  63         advance_to_mark_l;
  64         write(0,ff)
  65         move_r;
  66         mark;
  67         move_r;
  68         advance_to_mark_r;
  69 else if current = 1,tt
  70    then advance_mark_r;
  71         move_l;
  72         advance_to_mark_l;
  73         write(1,ff)
  74         move_r;
  75         mark;
  76         move_r;
  77         advance_to_mark_r;
  78 else nop
  79 *)
  80
  81 definition copy_step ≝
  82   ifTM ? (test_char STape (λc.is_bit (\fst c)))
  83   (single_finalTM ? (copy_step_subcase FSUnialpha (bit false)
  84     (copy_step_subcase FSUnialpha (bit true) (nop ?))))
  85   (nop ?)
  86   tc_true.
  87
  88 definition R_copy_step_true ≝
  89   λt1,t2.
  90     ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs →
  91     ∃x. c = bit x ∧
  92     (∀a,l1,c0,a0,l2,l3. (∀y.memb ? y l1 = true → is_marked ? y = false) →
  93      ls = l1@〈a0,false〉::〈c0,true〉::l2 →
  94      rs = 〈a,false〉::l3 →
  95      t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3).
  96
  97 definition R_copy_step_false ≝
  98   λt1,t2.
  99    ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
 100    is_bit (\fst c) = false ∧ t2 = t1.
 101
 102 axiom sem_comp_step :
 103   accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false.
 104
 105 definition copy ≝ whileTM ? copy_step (inr … (inl … (inr … 0))).
 106
 107 definition R_copy ≝ λt1,t2.
 108   ∀ls,c,rs. ∀l1,d,l2,l3,l4,l5,c0.
 109   t1 = midtape ? ls 〈c,true〉 rs →
 110   (* l1 è la stringa sorgente da copiare, l4@〈c0,true〉 è la sua destinazione *)
 111   〈c,false〉::rs = l1@〈d,false〉::l2 → only_bits l1 → is_bit d = false →
 112    ls = l3@l4@〈c0,true〉::l5 → |l4@[〈c0,true〉]| = |l1| →
 113    no_marks (l3@l4) →
 114   (∀l4',d'.l4@[〈c0,false〉] = 〈d',false〉::l4' →
 115    t2 = midtape STape (reverse ? l1@l3@〈d',true〉::l4'@l5) 〈d,true〉 l2).