matita/matita/lib/turing/universal/universal.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 include "turing/universal/uni_step.ma".
  15
  16 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
  17
  18 record normalTM : Type[0] ≝
  19 { no_states : nat;
  20   pos_no_states : (0 < no_states);
  21   ntrans : trans_source no_states → trans_target no_states;
  22   nhalt : initN no_states → bool
  23 }.
  24
  25 definition normalTM_to_TM ≝ λM:normalTM.
  26   mk_TM FinBool (initN (no_states M))
  27    (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
  28
  29 coercion normalTM_to_TM.
  30
  31 definition nconfig ≝ λn. config FinBool (initN n).
  32
  33 (*
  34 definition normalTM ≝ λn,t,h.
  35   λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
  36
  37 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
  38 λM:normalTM.λc.
  39   let n ≝ no_states M in
  40   let h ≝ nhalt M in
  41   let t ≝ntrans M in
  42   let q ≝ cstate … c in
  43   let q_low ≝  m_bits_of_state n h q in
  44   let current_low ≝ match current … (ctape … c) with [ None ⇒ null | Some b ⇒ bit b] in
  45   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
  46   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
  47   let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? t)) in
  48   let right ≝ q_low@〈current_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right in
  49   mk_tape STape (〈grid,false〉::low_left) (option_hd … right) (tail … right).
  50
  51 lemma low_config_eq: ∀t,M,c. t = low_config M c →
  52   ∃low_left,low_right,table,q_low_hd,q_low_tl,c_low.
  53   low_left = map … (λb.〈bit b,false〉) (left … (ctape …c)) ∧
  54   low_right = map … (λb.〈bit b,false〉) (right … (ctape …c)) ∧
  55   table = flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M))) ∧
  56   〈q_low_hd,false〉::q_low_tl = m_bits_of_state (no_states M) (nhalt M) (cstate … c) ∧
  57   c_low =  match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b] ∧
  58   t = midtape STape (〈grid,false〉::low_left) 〈q_low_hd,false〉 (q_low_tl@〈c_low,false〉::〈grid,false〉::table@〈grid,false〉::low_right).
  59 #t #M #c #eqt
  60   @(ex_intro … (map … (λb.〈bit b,false〉) (left … (ctape …c))))
  61   @(ex_intro … (map … (λb.〈bit b,false〉) (right … (ctape …c))))
  62   @(ex_intro … (flatten ? (tuples_of_pairs (no_states M) (nhalt M) (graph_enum ?? (ntrans M)))))
  63   @(ex_intro … (\fst (hd ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c)) 〈bit true,false〉)))
  64   @(ex_intro … (tail ? (m_bits_of_state (no_states M) (nhalt M) (cstate … c))))
  65   @(ex_intro … (match current … (ctape … c) with [ None ⇒ null| Some b ⇒ bit b]))
  66 % [% [% [% [% // | // ] | // ] | // ] | >eqt //]
  67 qed.
  68
  69 definition low_step_R_true ≝ λt1,t2.
  70   ∀M:normalTM.
  71   ∀c: nconfig (no_states M).
  72     t1 = low_config M c →
  73     halt ? M (cstate … c) = false ∧
  74       t2 = low_config M (step ? M c).
  75
  76 lemma unistep_to_low_step: ∀t1,t2.
  77   R_uni_step_true t1 t2 → low_step_R_true t1 t2.
  78 #t1 #t2 (* whd in ⊢ (%→%); *) #Huni_step #M #c #eqt1
  79 cases (low_config_eq … eqt1)
  80 #low_left * #low_right * #table * #q_low_hd * #q_low_tl * #current_low
  81 ***** #Hlow_left #Hlow_right #Htable #Hq_low #Hcurrent_low #Ht1
  82 lapply (Huni_step ??????????????? Ht1)
  83 whd in match (low_config M c);
  84
  85 definition R_uni_step_true ≝ λt1,t2.
  86   ∀n,t0,table,s0,s1,c0,c1,ls,rs,curconfig,newconfig,mv.
  87   table_TM (S n) (〈t0,false〉::table) →
  88   match_in_table (S n) (〈s0,false〉::curconfig) 〈c0,false〉
  89     (〈s1,false〉::newconfig) 〈c1,false〉 〈mv,false〉 (〈t0,false〉::table) →
  90   legal_tape ls 〈c0,false〉 rs →
  91   t1 = midtape STape (〈grid,false〉::ls) 〈s0,false〉
  92     (curconfig@〈c0,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs) →
  93   ∀t1'.t1' = lift_tape ls 〈c0,false〉 rs →
  94   s0 = bit false ∧
  95   ∃ls1,rs1,c2.
  96   (t2 = midtape STape (〈grid,false〉::ls1) 〈s1,false〉
  97     (newconfig@〈c2,false〉::〈grid,false〉::〈t0,false〉::table@〈grid,false〉::rs1) ∧
  98    lift_tape ls1 〈c2,false〉 rs1 =
  99    tape_move STape t1' (map_move c1 mv) ∧ legal_tape ls1 〈c2,false〉 rs1).
 100
 101
 102 definition low_step_R_false ≝ λt1,t2.
 103   ∀M:normalTM.
 104   ∀c: nconfig (no_states M).
 105     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
 106
 107 definition low_R ≝ λM,qstart,R,t1,t2.
 108     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
 109     ∃q,tape2.R tape1 tape2 ∧
 110     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
 111
 112 definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
 113 ∃i,outc.
 114   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
 115   t2 = (ctape ?? outc).
 116
 117 (*
 118 definition universal_R ≝ λM,R,t1,t2.
 119     Realize ? M R →
 120     ∀tape1,tape2.
 121     R tape1 tape 2 ∧
 122     t1 = low_config M (initc ? M tape1) ∧
 123     ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
 124
 125 axiom uni_step: TM STape.
 126 axiom us_acc: states ? uni_step.
 127
 128 axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
 129
 130 definition universalTM ≝ whileTM ? uni_step us_acc.
 131
 132 theorem sem_universal: ∀M:normalTM. ∀qstart.
 133   WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
 134 #M #q #intape #i #outc #Hloop
 135 lapply (sem_while … sem_uni_step intape i outc Hloop)
 136   [@daemon] -Hloop
 137 * #ta * #Hstar generalize in match q; -q
 138 @(star_ind_l ??????? Hstar)
 139   [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
 140    cases (Htb … Htb1) -Htb #Hhalt #Htb
 141    <Htb >Htb1 @ex_intro
 142    [|%{tape1} %
 143      [ %
 144        [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
 145         % [|%] whd in ⊢ (??%?); >Hhalt %
 146        | @Hhalt ]
 147      | % ]
 148    ]
 149   |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH
 150    #q #Htd #tape1 #Htb
 151    lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH
 152    #IH cases (Htc … Htb); -Htc #Hhaltq
 153    whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???))
 154    #Htc change with (mk_config ????) in Htc:(???(??%));
 155    cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
 156    @(ex_intro … q1) @(ex_intro … tape2) %
 157     [%
 158       [cases HRTM #k * #outc1 * #Hloop #Houtc1
 159        @(ex_intro … (S k)) @(ex_intro … outc1) %
 160         [>loop_S_false [2://] whd in match (step ???);
 161          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
 162         |@Houtc1
 163         ]
 164       |@Hhaltq1]
 165     |@Houtc
 166     ]
 167   ]
 168 qed.
 169
 170 lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2.
 171   WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
 172 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
 173 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
 174 qed.
 175
 176 axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
 177   (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
 178
 179 theorem sem_universal2: ∀M:normalTM. ∀R.
 180   WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
 181 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 182 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 183 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 184 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 185 qed.
 186