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
  15 (* definition zero : ∀n.initN n ≝ λn.mk_Sig ?? 0 (le_O_n n). *)
  16
  17 record normalTM : Type[0] ≝
  18 { no_states : nat;
  19   pos_no_states : (0 < no_states);
  20   ntrans : trans_source no_states → trans_target no_states;
  21   nhalt : initN no_states → bool
  22 }.
  23
  24 definition normalTM_to_TM ≝ λM:normalTM.
  25   mk_TM FinBool (initN (no_states M))
  26    (ntrans M) (mk_Sig ?? 0 (pos_no_states M)) (nhalt M).
  27
  28 coercion normalTM_to_TM.
  29
  30 definition nconfig ≝ λn. config FinBool (initN n).
  31
  32 (*
  33 definition normalTM ≝ λn,t,h.
  34   λk:0<n.mk_TM FinBool (initN n) t (mk_Sig ?? 0 k) h. *)
  35
  36 definition low_config: ∀M:normalTM.nconfig (no_states M) → tape STape ≝
  37 λM:normalTM.λc.
  38   let n ≝ no_states M in
  39   let h ≝ nhalt M in
  40   let t ≝ntrans M in
  41   let q ≝ cstate … c in
  42   let q_low ≝  m_bits_of_state n h q in
  43   let current_low ≝
  44     match current … (ctape … c) with
  45     [ None ⇒ 〈null,false〉
  46     | Some b ⇒ 〈bit b,false〉] in
  47   let low_left ≝ map … (λb.〈bit b,false〉) (left … (ctape …c)) in
  48   let low_right ≝ map … (λb.〈bit b,false〉) (right … (ctape …c)) in
  49   let table ≝ flatten ? (tuples_of_pairs n h (graph_enum ?? t)) in
  50   mk_tape STape low_left (Some ? 〈grid,false〉)
  51     (q_low@current_low::〈grid,false〉::table@〈grid,false〉::low_right).
  52
  53 definition low_step_R_true ≝ λt1,t2.
  54   ∀M:normalTM.
  55   ∀c: nconfig (no_states M).
  56     t1 = low_config M c →
  57     halt ? M (cstate … c) = false ∧
  58       t2 = low_config M (step ? M c).
  59
  60 definition low_step_R_false ≝ λt1,t2.
  61   ∀M:normalTM.
  62   ∀c: nconfig (no_states M).
  63     t1 = low_config M c → halt ? M (cstate … c) = true  ∧ t1 = t2.
  64
  65 definition low_R ≝ λM,qstart,R,t1,t2.
  66     ∀tape1. t1 = low_config M (mk_config ?? qstart tape1) →
  67     ∃q,tape2.R tape1 tape2 ∧
  68     halt ? M q = true ∧ t2 = low_config M (mk_config ?? q tape2).
  69
  70 definition R_TM ≝ λsig.λM:TM sig.λq.λt1,t2.
  71 ∃i,outc.
  72   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (mk_config ?? q t1) = Some ? outc ∧
  73   t2 = (ctape ?? outc).
  74
  75 (*
  76 definition universal_R ≝ λM,R,t1,t2.
  77     Realize ? M R →
  78     ∀tape1,tape2.
  79     R tape1 tape 2 ∧
  80     t1 = low_config M (initc ? M tape1) ∧
  81     ∃q.halt ? M q = true → t2 = low_config M (mk_config ?? q tape2).*)
  82
  83 axiom uni_step: TM STape.
  84 axiom us_acc: states ? uni_step.
  85
  86 axiom sem_uni_step: accRealize ? uni_step us_acc low_step_R_true low_step_R_false.
  87
  88 definition universalTM ≝ whileTM ? uni_step us_acc.
  89
  90 theorem sem_universal: ∀M:normalTM. ∀qstart.
  91   WRealize ? universalTM (low_R M qstart (R_TM FinBool M qstart)).
  92 #M #q #intape #i #outc #Hloop
  93 lapply (sem_while … sem_uni_step intape i outc Hloop)
  94   [@daemon] -Hloop
  95 * #ta * #Hstar generalize in match q; -q
  96 @(star_ind_l ??????? Hstar)
  97   [#tb #q0 whd in ⊢ (%→?); #Htb #tape1 #Htb1
  98    cases (Htb … Htb1) -Htb #Hhalt #Htb
  99    <Htb >Htb1 @ex_intro
 100    [|%{tape1} %
 101      [ %
 102        [ whd @(ex_intro … 1) @(ex_intro … (mk_config … q0 tape1))
 103         % [|%] whd in ⊢ (??%?); >Hhalt %
 104        | @Hhalt ]
 105      | % ]
 106    ]
 107   |#tb #tc #td whd in ⊢ (%→?); #Htc #Hstar1 #IH
 108    #q #Htd #tape1 #Htb
 109    lapply (IH (\fst (trans ? M 〈q,current ? tape1〉)) Htd) -IH
 110    #IH cases (Htc … Htb); -Htc #Hhaltq
 111    whd in match (step ???); >(eq_pair_fst_snd ?? (trans ???))
 112    #Htc change with (mk_config ????) in Htc:(???(??%));
 113    cases (IH ? Htc) #q1 * #tape2 * * #HRTM #Hhaltq1 #Houtc
 114    @(ex_intro … q1) @(ex_intro … tape2) %
 115     [%
 116       [cases HRTM #k * #outc1 * #Hloop #Houtc1
 117        @(ex_intro … (S k)) @(ex_intro … outc1) %
 118         [>loop_S_false [2://] whd in match (step ???);
 119          >(eq_pair_fst_snd ?? (trans ???)) @Hloop
 120         |@Houtc1
 121         ]
 122       |@Hhaltq1]
 123     |@Houtc
 124     ]
 125   ]
 126 qed.
 127
 128 lemma R_TM_to_R: ∀sig,M,R. ∀t1,t2.
 129   WRealize sig M R → R_TM ? M (start ? M) t1 t2 → R t1 t2.
 130 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
 131 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
 132 qed.
 133
 134 axiom WRealize_to_WRealize: ∀sig,M,R1,R2.
 135   (∀t1,t2.R1 t1 t2 → R2 t1 t2) → WRealize sig M R1 → WRealize ? M R2.
 136
 137 theorem sem_universal2: ∀M:normalTM. ∀R.
 138   WRealize ? M R → WRealize ? universalTM (low_R M (start ? M) R).
 139 #M #R #HMR lapply (sem_universal … M (start ? M)) @WRealize_to_WRealize
 140 #t1 #t2 whd in ⊢ (%→%); #H #tape1 #Htape1 cases (H ? Htape1)
 141 #q * #tape2 * * #HRTM #Hhalt #Ht2 @(ex_intro … q) @(ex_intro … tape2)
 142 % [% [@(R_TM_to_R … HRTM) @HMR | //] | //]
 143 qed.
 144