matita/matita/lib/turing/universal/trans_step.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 include "turing/universal/trans_to_tuples.ma".
  14
  15 check TM
  16
  17 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
  18
  19 definition normalTM ≝ λn,t,h.
  20   λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h.
  21
  22 definition low_config: ∀n,h,t.config FinBool (initN n) → tape STape ≝
  23 λn,h.λtrans:trans_source n →trans_target n.λc.
  24   let q ≝ cstate … c in
  25   let q_low ≝  m_bits_of_state n h q in
  26   let current_low ≝
  27     match current … (ctape … c) with
  28     [ None ⇒ 〈null,false〉
  29     | Some b ⇒ 〈bit b,false〉] in
  30   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
  31   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
  32   let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? trans)) in
  33   mk_tape STape low_left (Some ? 〈grid,false〉)
  34     (q_low@current_low::〈grid,false〉::table@〈grid,false〉::low_right).
  35
  36 (*
  37 definition R_uni_step_true ≝ λt1,t2.
  38   ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
  39   table_TM (S n) (〈t0,false〉::table) →
  40   match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
  41     (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) →
  42   legal_tape ls 〈c0,false〉 rs →
  43   t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉
  44     (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) →
  45   ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs →
  46   s0 = bit false ∧
  47   ∃ls1,rs1,c2.
  48   (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉
  49     (newconfig@〈c2,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs1) ∧
  50    lift_tape ls1 〈c2,false〉 rs1 =
  51    tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
  52  *)