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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
17 include "turing/universal/tuples.ma".
19 definition write_states ≝ initN 2.
21 definition write ≝ λalpha,c.
22 mk_TM alpha write_states
25 [ O ⇒ 〈1,Some ? 〈c,N〉〉
29 definition R_write ≝ λalpha,c,t1,t2.
30 ∀ls,x,rs.t1 = midtape alpha ls x rs → t2 = midtape alpha ls c rs.
32 axiom sem_write : ∀alpha,c.Realize ? (write alpha c) (R_write alpha c).
34 definition copy_step_subcase ≝
35 λalpha,c,elseM.ifTM ? (test_char ? (λx.x == 〈c,true〉))
36 (seq (FinProd alpha FinBool) (adv_mark_r …)
38 (seq ? (adv_to_mark_l … (is_marked alpha))
39 (seq ? (write ? 〈c,false〉)
42 (seq ? (move_r …) (adv_to_mark_r … (is_marked alpha)))))))))
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 →
49 ∀a,l1,x0,a0,l2,l3. (∀c.memb ? c l1 = true → is_marked ? c = false) →
50 ls = l1@〈a0,false〉::〈x0,true〉::l2 →
52 t2 = midtape ? (〈x,false〉::l1@〈a0,true〉::〈x,false〉::l2) 〈a,true〉 l3) ∨
53 (x ≠ c ∧ RelseM t1 t2).
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).
69 else if current = 1,tt
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 ?))))
88 definition R_copy_step_true ≝
90 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls 〈c,true〉 rs →
92 (∀a,l1,c0,a0,l2,l3. (∀y.memb ? y l1 = true → is_marked ? y = false) →
93 ls = l1@〈a0,false〉::〈c0,true〉::l2 →
95 t2 = midtape STape (〈bit x,false〉::l1@〈a0,true〉::〈bit x,false〉::l2) 〈a,true〉 l3).
97 definition R_copy_step_false ≝
99 ∀ls,c,rs.t1 = midtape (FinProd … FSUnialpha FinBool) ls c rs →
100 is_bit (\fst c) = false ∧ t2 = t1.
102 axiom sem_comp_step :
103 accRealize ? copy_step (inr … (inl … (inr … 0))) R_copy_step_true R_copy_step_false.
105 definition copy ≝ whileTM ? copy_step (inr … (inl … (inr … 0))).
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| →
114 (∀l4',d'.l4@[〈c0,false〉] = 〈d',false〉::l4' →
115 t2 = midtape STape (reverse ? l1@l3@〈d',true〉::l4'@l5) 〈d,true〉 l2).