turing.ma

   1 include "turing/mono.ma".
   2 include "basics/vectors.ma".
   3
   4 (* We do not distinuish an input tape *)
   5
   6 record mTM (sig:FinSet): Type[1] ≝
   7 { states : FinSet;
   8   tapes_no: nat; (* additional working tapes *)
   9   trans : states × (Vector (option sig) (S tapes_no)) →
  10     states  × (Vector (option (sig × move))(S tapes_no));
  11   start: states;
  12   halt : states → bool
  13 }.
  14
  15 record mconfig (sig,states:FinSet) (n:nat): Type[0] ≝
  16 { cstate : states;
  17   ctapes : Vector (tape sig) (S n)
  18 }.
  19
  20 definition current_chars ≝ λsig.λn.λtapes.
  21   vec_map ?? (current sig) (S n) tapes.
  22
  23 definition step ≝ λsig.λM:mTM sig.λc:mconfig sig (states ? M) (tapes_no ? M).
  24   let 〈news,mvs〉 ≝ trans sig M 〈cstate ??? c,current_chars ?? (ctapes ??? c)〉 in
  25   mk_mconfig ???
  26     news
  27     (pmap_vec ??? (tape_move sig) ? (ctapes ??? c) mvs).
  28
  29 definition empty_tapes ≝ λsig.λn.
  30 mk_Vector ? n (make_list (tape sig) (niltape sig) n) ?.
  31 elim n // normalize //
  32 qed.
  33
  34 (************************** Realizability *************************************)
  35 definition loopM ≝ λsig.λM:mTM sig.λi,cin.
  36   loop ? i (step sig M) (λc.halt sig M (cstate ??? c)) cin.
  37
  38 lemma loopM_unfold : ∀sig,M,i,cin.
  39   loopM sig M i cin = loop ? i (step sig M) (λc.halt sig M (cstate ??? c)) cin.
  40 // qed.
  41
  42 definition initc ≝ λsig.λM:mTM sig.λtapes.
  43   mk_mconfig sig (states sig M) (tapes_no sig M) (start sig M) tapes.
  44
  45 definition Realize ≝ λsig.λM:mTM sig.λR:relation (Vector (tape sig) ?).
  46 ∀t.∃i.∃outc.
  47   loopM sig M i (initc sig M t) = Some ? outc ∧ R t (ctapes ??? outc).
  48
  49 definition WRealize ≝ λsig.λM:mTM sig.λR:relation (Vector (tape sig) ?).
  50 ∀t,i,outc.
  51   loopM sig M i (initc sig M t) = Some ? outc → R t (ctapes ??? outc).
  52
  53 definition Terminate ≝ λsig.λM:mTM sig.λt. ∃i,outc.
  54   loopM sig M i (initc sig M t) = Some ? outc.
  55
  56 (* notation "M \vDash R" non associative with precedence 45 for @{ 'models $M $R}. *)
  57 interpretation "multi realizability" 'models M R = (Realize ? M R).
  58
  59 (* notation "M \VDash R" non associative with precedence 45 for @{ 'wmodels $M $R}. *)
  60 interpretation "weak multi realizability" 'wmodels M R = (WRealize ? M R).
  61
  62 interpretation "multi termination" 'fintersects M t = (Terminate ? M t).
  63
  64 lemma WRealize_to_Realize : ∀sig.∀M: mTM sig.∀R.
  65   (∀t.M ↓ t) → M ⊫ R → M ⊨ R.
  66 #sig #M #R #HT #HW #t cases (HT … t) #i * #outc #Hloop
  67 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
  68 qed.
  69
  70 theorem Realize_to_WRealize : ∀sig.∀M:mTM sig.∀R.
  71   M ⊨ R → M ⊫ R.
  72 #sig #M #R #H1 #inc #i #outc #Hloop
  73 cases (H1 inc) #k * #outc1 * #Hloop1 #HR >(loop_eq … Hloop Hloop1) //
  74 qed.
  75
  76 definition accRealize ≝ λsig.λM:mTM sig.λacc:states sig M.λRtrue,Rfalse.
  77 ∀t.∃i.∃outc.
  78   loopM sig M i (initc sig M t) = Some ? outc ∧
  79     (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
  80     (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
  81
  82 (* notation "M ⊨ [q: R1,R2]" non associative with precedence 45 for @{ 'cmodels $M $q $R1 $R2}. *)
  83 interpretation "conditional multi realizability" 'cmodels M q R1 R2 = (accRealize ? M q R1 R2).
  84
  85 (*************************** guarded realizablity *****************************)
  86 definition GRealize ≝ λsig.λM:mTM sig.λPre:Vector (tape sig) ? →Prop.λR:relation (Vector (tape sig) ?).
  87 ∀t.Pre t → ∃i.∃outc.
  88   loopM sig M i (initc sig M t) = Some ? outc ∧ R t (ctapes ??? outc).
  89
  90 definition accGRealize ≝ λsig.λM:mTM sig.λacc:states sig M.
  91 λPre: Vector (tape sig) ? → Prop.λRtrue,Rfalse.
  92 ∀t.Pre t → ∃i.∃outc.
  93   loopM sig M i (initc sig M t) = Some ? outc ∧
  94     (cstate ??? outc = acc → Rtrue t (ctapes ??? outc)) ∧
  95     (cstate ??? outc ≠ acc → Rfalse t (ctapes ??? outc)).
  96
  97 lemma WRealize_to_GRealize : ∀sig.∀M: mTM sig.∀Pre,R.
  98   (∀t.Pre t → M ↓ t) → M ⊫ R → GRealize sig M Pre R.
  99 #sig #M #Pre #R #HT #HW #t #HPre cases (HT … t HPre) #i * #outc #Hloop
 100 @(ex_intro … i) @(ex_intro … outc) % // @(HW … i) //
 101 qed.
 102
 103 lemma Realize_to_GRealize : ∀sig.∀M: mTM sig.∀P,R.
 104   M ⊨ R → GRealize sig M P R.
 105 #alpha #M #Pre #R #HR #t #HPre
 106 cases (HR t) -HR #k * #outc * #Hloop #HR
 107 @(ex_intro ?? k) @(ex_intro ?? outc) %
 108   [ @Hloop | @HR ]
 109 qed.
 110
 111 lemma acc_Realize_to_acc_GRealize: ∀sig.∀M:mTM sig.∀q:states sig M.∀P,R1,R2.
 112   M ⊨ [q:R1,R2] → accGRealize sig M q P R1 R2.
 113 #alpha #M #q #Pre #R1 #R2 #HR #t #HPre
 114 cases (HR t) -HR #k * #outc * * #Hloop #HRtrue #HRfalse
 115 @(ex_intro ?? k) @(ex_intro ?? outc) %
 116   [ % [@Hloop] @HRtrue | @HRfalse]
 117 qed.
 118
 119 (******************************** monotonicity ********************************)
 120 lemma Realize_to_Realize : ∀sig.∀M:mTM sig.∀R1,R2.
 121   R1 ⊆ R2 → Realize sig M R1 → Realize sig M R2.
 122 #alpha #M #R1 #R2 #Himpl #HR1 #intape
 123 cases (HR1 intape) -HR1 #k * #outc * #Hloop #HR1
 124 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
 125 qed.
 126
 127 lemma WRealize_to_WRealize: ∀sig.∀M:mTM sig.∀R1,R2.
 128   R1 ⊆ R2 → WRealize sig M R1 → WRealize ? M R2.
 129 #alpha #M #R1 #R2 #Hsub #HR1 #intape #i #outc #Hloop
 130 @Hsub @(HR1 … i) @Hloop
 131 qed.
 132
 133 lemma GRealize_to_GRealize : ∀sig.∀M:mTM sig.∀P,R1,R2.
 134   R1 ⊆ R2 → GRealize sig M P R1 → GRealize sig M P R2.
 135 #alpha #M #P #R1 #R2 #Himpl #HR1 #intape #HP
 136 cases (HR1 intape HP) -HR1 #k * #outc * #Hloop #HR1
 137 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
 138 qed.
 139
 140 lemma GRealize_to_GRealize_2 : ∀sig.∀M:mTM sig.∀P1,P2,R1,R2.
 141   P2 ⊆ P1 → R1 ⊆ R2 → GRealize sig M P1 R1 → GRealize sig M P2 R2.
 142 #alpha #M #P1 #P2 #R1 #R2 #Himpl1 #Himpl2 #H1 #intape #HP
 143 cases (H1 intape (Himpl1 … HP)) -H1 #k * #outc * #Hloop #H1
 144 @(ex_intro ?? k) @(ex_intro ?? outc) % /2/
 145 qed.
 146
 147 lemma acc_Realize_to_acc_Realize: ∀sig.∀M:mTM sig.∀q:states sig M.∀R1,R2,R3,R4.
 148   R1 ⊆ R3 → R2 ⊆ R4 → M ⊨ [q:R1,R2] → M ⊨ [q:R3,R4].
 149 #alpha #M #q #R1 #R2 #R3 #R4 #Hsub13 #Hsub24 #HRa #intape
 150 cases (HRa intape) -HRa #k * #outc * * #Hloop #HRtrue #HRfalse
 151 @(ex_intro ?? k) @(ex_intro ?? outc) %
 152   [ % [@Hloop] #Hq @Hsub13 @HRtrue // | #Hq @Hsub24 @HRfalse //]
 153 qed.
 154
 155 (**************************** A canonical relation ****************************)
 156
 157 definition R_mTM ≝ λsig.λM:mTM sig.λq.λt1,t2.
 158 ∃i,outc.
 159   loopM ? M i (mk_mconfig ??? q t1) = Some ? outc ∧
 160   t2 = (ctapes ??? outc).
 161
 162 lemma R_mTM_to_R: ∀sig.∀M:mTM sig.∀R. ∀t1,t2.
 163   M ⊫ R → R_mTM ? M (start sig M) t1 t2 → R t1 t2.
 164 #sig #M #R #t1 #t2 whd in ⊢ (%→?); #HMR * #i * #outc *
 165 #Hloop #Ht2 >Ht2 @(HMR … Hloop)
 166 qed.
 167
 168 (******************************** NOP Machine *********************************)
 169
 170 (* NO OPERATION
 171    t1 = t2
 172
 173 definition nop_states ≝ initN 1.
 174 definition start_nop : initN 1 ≝ mk_Sig ?? 0 (le_n … 1). *)
 175
 176 definition mnop ≝
 177   λalpha:FinSet.λn.mk_mTM alpha nop_states n
 178   (λp.let 〈q,a〉 ≝ p in 〈q,mk_Vector ? (S n) (make_list ? (None ?) (S n)) ?〉)
 179   start_nop (λ_.true).
 180 elim n normalize //
 181 qed.
 182
 183 definition R_mnop ≝ λalpha,n.λt1,t2:Vector (tape alpha) (S n).t2 = t1.
 184
 185 lemma sem_mnop :
 186   ∀alpha,n.mnop alpha n⊨ R_mnop alpha n.
 187 #alpha #n #intapes @(ex_intro ?? 1)
 188 @(ex_intro … (mk_mconfig ??? start_nop intapes)) % %
 189 qed.
 190
 191 lemma mnop_single_state: ∀sig,n.∀q1,q2:states ? (mnop sig n). q1 = q2.
 192 normalize #sig #n0 * #n #ltn1 * #m #ltm1
 193 generalize in match ltn1; generalize in match ltm1;
 194 <(le_n_O_to_eq … (le_S_S_to_le … ltn1)) <(le_n_O_to_eq … (le_S_S_to_le … ltm1))
 195 // qed.
 196
 197 (************************** Sequential Composition ****************************)
 198
 199 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 200 λp. let 〈s,a〉 ≝ p in
 201   match s with
 202   [ inl s1 ⇒
 203       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 204       else let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in 〈inl … news1,m〉
 205   | inr s2 ⇒ let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in 〈inr … news2,m〉
 206   ].
 207
 208 definition seq ≝ λsig. λM1,M2 : TM sig.
 209   mk_TM sig
 210     (FinSum (states sig M1) (states sig M2))
 211     (seq_trans sig M1 M2)
 212     (inl … (start sig M1))
 213     (λs.match s with
 214       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 215
 216 notation "a · b" right associative with precedence 65 for @{ 'middot $a $b}.
 217 interpretation "sequential composition" 'middot a b = (seq ? a b).
 218
 219 definition lift_confL ≝
 220   λsig,S1,S2,c.match c with
 221   [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inl … s) t ].
 222
 223 definition lift_confR ≝
 224   λsig,S1,S2,c.match c with
 225   [ mk_config s t ⇒ mk_config sig (FinSum S1 S2) (inr … s) t ].
 226
 227 definition halt_liftL ≝
 228   λS1,S2,halt.λs:FinSum S1 S2.
 229   match s with
 230   [ inl s1 ⇒ halt s1
 231   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 232
 233 definition halt_liftR ≝
 234   λS1,S2,halt.λs:FinSum S1 S2.
 235   match s with
 236   [ inl _ ⇒ false
 237   | inr s2 ⇒ halt s2 ].
 238
 239 lemma p_halt_liftL : ∀sig,S1,S2,halt,c.
 240   halt (cstate sig S1 c) =
 241      halt_liftL S1 S2 halt (cstate … (lift_confL … c)).
 242 #sig #S1 #S2 #halt #c cases c #s #t %
 243 qed.
 244
 245 lemma trans_seq_liftL : ∀sig,M1,M2,s,a,news,move.
 246   halt ? M1 s = false →
 247   trans sig M1 〈s,a〉 = 〈news,move〉 →
 248   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 249 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 250 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 251 qed.
 252
 253 lemma trans_seq_liftR : ∀sig,M1,M2,s,a,news,move.
 254   halt ? M2 s = false →
 255   trans sig M2 〈s,a〉 = 〈news,move〉 →
 256   trans sig (seq sig M1 M2) 〈inr … s,a〉 = 〈inr … news,move〉.
 257 #sig #M1 * #Q2 #T2 #init2 #halt2 #s #a #news #move
 258 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 259 qed.
 260
 261 lemma step_seq_liftR : ∀sig,M1,M2,c0.
 262  halt ? M2 (cstate ?? c0) = false →
 263  step sig (seq sig M1 M2) (lift_confR sig (states ? M1) (states ? M2) c0) =
 264  lift_confR sig (states ? M1) (states ? M2) (step sig M2 c0).
 265 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
 266   lapply (refl ? (trans ?? 〈s,current sig t〉))
 267   cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
 268   #s0 #m0 cases t
 269   [ #Heq #Hhalt
 270   | 2,3: #s1 #l1 #Heq #Hhalt
 271   |#ls #s1 #rs #Heq #Hhalt ]
 272   whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
 273   whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftR … Heq) //
 274 qed.
 275
 276 lemma step_seq_liftL : ∀sig,M1,M2,c0.
 277  halt ? M1 (cstate ?? c0) = false →
 278  step sig (seq sig M1 M2) (lift_confL sig (states ? M1) (states ? M2) c0) =
 279  lift_confL sig ?? (step sig M1 c0).
 280 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s #t
 281   lapply (refl ? (trans ?? 〈s,current sig t〉))
 282   cases (trans ?? 〈s,current sig t〉) in ⊢ (???% → %);
 283   #s0 #m0 cases t
 284   [ #Heq #Hhalt
 285   | 2,3: #s1 #l1 #Heq #Hhalt
 286   |#ls #s1 #rs #Heq #Hhalt ]
 287   whd in ⊢ (???(????%)); >Heq whd in ⊢ (???%);
 288   whd in ⊢ (??(???%)?); whd in ⊢ (??%?); >(trans_seq_liftL … Heq) //
 289 qed.
 290
 291 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 292   halt ? M1 s = true →
 293   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 294 #sig #M1 #M2 #s #a #Hhalt whd in ⊢ (??%?); >Hhalt %
 295 qed.
 296
 297 lemma eq_ctape_lift_conf_L : ∀sig,S1,S2,outc.
 298   ctape sig (FinSum S1 S2) (lift_confL … outc) = ctape … outc.
 299 #sig #S1 #S2 #outc cases outc #s #t %
 300 qed.
 301
 302 lemma eq_ctape_lift_conf_R : ∀sig,S1,S2,outc.
 303   ctape sig (FinSum S1 S2) (lift_confR … outc) = ctape … outc.
 304 #sig #S1 #S2 #outc cases outc #s #t %
 305 qed.
 306
 307 theorem sem_seq: ∀sig.∀M1,M2:TM sig.∀R1,R2.
 308   M1 ⊨ R1 → M2 ⊨ R2 → M1 · M2 ⊨ R1 ∘ R2.
 309 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 310 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 311 cases (HR2 (ctape sig (states ? M1) outc1)) #k2 * #outc2 * #Hloop2 #HM2
 312 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 313 %
 314 [@(loop_merge ???????????
 315    (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
 316    (step sig M1) (step sig (seq sig M1 M2))
 317    (λc.halt sig M1 (cstate … c))
 318    (λc.halt_liftL ?? (halt sig M1) (cstate … c)) … Hloop1))
 319   [ * *
 320    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 321    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 322   || #c0 #Hhalt <step_seq_liftL //
 323   | #x <p_halt_liftL %
 324   |6:cases outc1 #s1 #t1 %
 325   |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
 326     [ * #s2 #t2 %
 327     | #c0 #Hhalt <step_seq_liftR // ]
 328   |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 329    generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 330    >(trans_liftL_true sig M1 M2 ??)
 331     [ whd in ⊢ (??%?); whd in ⊢ (???%);
 332       @config_eq whd in ⊢ (???%); //
 333     | @(loop_Some ?????? Hloop10) ]
 334  ]
 335 | @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
 336   % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
 337 ]
 338 qed.
 339
 340 theorem sem_seq_app: ∀sig.∀M1,M2:TM sig.∀R1,R2,R3.
 341   M1 ⊨ R1 → M2 ⊨ R2 → R1 ∘ R2 ⊆ R3 → M1 · M2 ⊨ R3.
 342 #sig #M1 #M2 #R1 #R2 #R3 #HR1 #HR2 #Hsub
 343 #t cases (sem_seq … HR1 HR2 t)
 344 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
 345 % [@Hloop |@Hsub @Houtc]
 346 qed.
 347
 348 (* composition with guards *)
 349 theorem sem_seq_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2.
 350   GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
 351   (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) →
 352   GRealize sig (M1 · M2) Pre1 (R1 ∘ R2).
 353 #sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #HGR1 #HGR2 #Hinv #t1 #HPre1
 354 cases (HGR1 t1 HPre1) #k1 * #outc1 * #Hloop1 #HM1
 355 cases (HGR2 (ctape sig (states ? M1) outc1) ?)
 356   [2: @(Hinv … HPre1 HM1)]
 357 #k2 * #outc2 * #Hloop2 #HM2
 358 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 359 %
 360 [@(loop_merge ???????????
 361    (loop_lift ??? (lift_confL sig (states sig M1) (states sig M2))
 362    (step sig M1) (step sig (seq sig M1 M2))
 363    (λc.halt sig M1 (cstate … c))
 364    (λc.halt_liftL ?? (halt sig M1) (cstate … c)) … Hloop1))
 365   [ * *
 366    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 367    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 368   || #c0 #Hhalt <step_seq_liftL //
 369   | #x <p_halt_liftL %
 370   |6:cases outc1 #s1 #t1 %
 371   |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
 372     [ * #s2 #t2 %
 373     | #c0 #Hhalt <step_seq_liftR // ]
 374   |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 375    generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 376    >(trans_liftL_true sig M1 M2 ??)
 377     [ whd in ⊢ (??%?); whd in ⊢ (???%);
 378       @config_eq whd in ⊢ (???%); //
 379     | @(loop_Some ?????? Hloop10) ]
 380  ]
 381 | @(ex_intro … (ctape ? (FinSum (states ? M1) (states ? M2)) (lift_confL … outc1)))
 382   % // >eq_ctape_lift_conf_L >eq_ctape_lift_conf_R //
 383 ]
 384 qed.
 385
 386 theorem sem_seq_app_guarded: ∀sig.∀M1,M2:TM sig.∀Pre1,Pre2,R1,R2,R3.
 387   GRealize sig M1 Pre1 R1 → GRealize sig M2 Pre2 R2 →
 388   (∀t1,t2.Pre1 t1 → R1 t1 t2 → Pre2 t2) → R1 ∘ R2 ⊆ R3 →
 389   GRealize sig (M1 · M2) Pre1 R3.
 390 #sig #M1 #M2 #Pre1 #Pre2 #R1 #R2 #R3 #HR1 #HR2 #Hinv #Hsub
 391 #t #HPre1 cases (sem_seq_guarded … HR1 HR2 Hinv t HPre1)
 392 #k * #outc * #Hloop #Houtc @(ex_intro … k) @(ex_intro … outc)
 393 % [@Hloop |@Hsub @Houtc]
 394 qed.
 395
 396
 397
 398
 399
 400
 401
 402
 403 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 404   halt sig M (state sig M c).
 405
 406 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 407   match n with
 408   [ O ⇒ None ?
 409   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 410   ].
 411
 412 (* Compute ? M f states that f is computed by M *)
 413 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 414 ∀l.∃i.∃c.
 415   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 416   out ?? c = f l.
 417
 418 (* for decision problems, we accept a string if on termination
 419 output is not empty *)
 420
 421 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 422 ∀l.∃i.∃c.
 423   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 424   (isnilb ? (out ?? c) = false).
 425
 426 (* alternative approach.
 427 We define the notion of computation. The notion must be constructive,
 428 since we want to define functions over it, like lenght and size
 429
 430 Perche' serve Type[2] se sposto a e b a destra? *)
 431
 432 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 433   mk_move: p a = false → b = f a → cmove A f p a b.
 434
 435 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 436 | empty : ∀a. cstar A M a a
 437 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 438
 439 definition computation ≝ λsig.λM:TM sig.
 440   cstar ? (cmove ? (step sig M) (stop sig M)).
 441
 442 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 443   ∀l.∃c.computation sig M (init sig M l) c →
 444    (stop sig M c = true) ∧ out ?? c = f l.
 445
 446 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 447   ∀l.∃c.computation sig M (init sig M l) c →
 448    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).
 449