matita/matita/lib/turing/while_machine.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 include "turing/mono.ma".
  13 include "basics/star.ma".
  14
  15 definition while_trans ≝ λsig. λM : TM sig. λq:states sig M. λp.
  16   let 〈s,a〉 ≝ p in
  17   if s == q then 〈start ? M, None ?〉
  18   else trans ? M p.
  19
  20 definition whileTM ≝ λsig. λM : TM sig. λqacc: states ? M.
  21   mk_TM sig
  22     (states ? M)
  23     (while_trans sig M qacc)
  24     (start sig M)
  25     (λs.halt sig M s ∧ ¬ s==qacc).
  26
  27 axiom daemon : ∀X:Prop.X.
  28
  29 lemma while_trans_false : ∀sig,M,q,p.
  30   \fst p ≠ q → trans sig (whileTM sig M q) p = trans sig M p.
  31 #sig #M #q * #q1 #a #Hq normalize >(\bf Hq) normalize //
  32 qed.
  33
  34 lemma loop_lift_acc : ∀A,B,k,lift,f,g,h,hlift,c1,c2,subh.
  35   (∀x.subh x = true → h x = true) →
  36   (∀x.subh x = false → hlift (lift x) = h x) →
  37   (∀x.h x = false → lift (f x) = g (lift x)) →
  38   subh c2 = false →
  39   loop A k f h c1 = Some ? c2 →
  40   loop B k g hlift (lift c1) = Some ? (lift … c2).
  41 #A #B #k #lift #f #g #h #hlift #c1 #c2 #subh #Hsubh #Hlift #Hfg #Hc2
  42 generalize in match c1; elim k
  43 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
  44 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
  45  cases (true_or_false (h c0)) #Hc0 >Hc0
  46    [ normalize #Heq destruct (Heq) >(Hlift … Hc2) >Hc0 //
  47    | normalize >(Hlift c0)
  48      [>Hc0 normalize <(Hfg … Hc0) @IH
  49      |cases (true_or_false (subh c0)) //
  50       #H <Hc0 @sym_eq >H @Hsubh //
  51    ]
  52  ]
  53 qed.
  54
  55 theorem sem_while: ∀sig,M,acc,Rtrue,Rfalse.
  56   halt sig M acc = true →
  57   accRealize sig M acc Rtrue Rfalse →
  58     Realize sig (whileTM sig M acc) ((star ? Rtrue) ∘ Rfalse).
  59 #sig #M #acc #Rtrue #Rfalse #Hacctrue #HaccR #t
  60 cases (HaccR t) #k * #outc * * #Hloop #HMtrue #HMfalse
  61 cases (true_or_false (cstate ?? outc == acc)) #Hacc
  62   [
  63   |@(ex_intro … k) @(ex_intro … outc) %
  64     [@(loop_lift_acc ?? k (λc.c) … Hloop)
  65       [@(λc. (cstate ?? c) == acc)
  66       |* #q #a #eqacc >(\P eqacc) //
  67       |#c #eqacc normalize >eqacc normalize
  68        cases (halt sig M ?) normalize //
  69       |* #s #a #halts whd in ⊢ (??%?);
  70        whd in ⊢ (???%); >while_trans_false
  71         [ % | @(not_to_not … not_eq_true_false) #eqs
  72          <Hacctrue <eqs //
  73         ]
  74       |@Hacc
  75       ]
  76     |@(ex_intro … t) % // @HMfalse @(\Pf Hacc)
  77     ]
  78   ]
  79 qed.
  80
  81   [cases (HR2 (ctape sig ? outc1)) #k2 * #outc2 * #Hloop2 #HM2
  82    @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … (lift_confL … outc2)))
  83    %
  84    [@(loop_split ???????????
  85     (loop_lift ???
  86       (lift_confL sig (states ? M1) (FinSum (states ? M2) (states ? M3)))
  87       (step sig M1) (step sig (ifTM sig M1 M2 M3 acc))
  88       (λc.halt sig M1 (cstate … c))
  89       (λc.halt_liftL ?? (halt sig M1) (cstate … c))
  90       … Hloop1))
  91      [* *
  92        [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
  93        | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
  94      || #c0 #Hhalt @daemon  (* <step_lift_confL // *)
  95      | #x <p_halt_liftL %
  96      |6:cases outc1 #s1 #t1 %
  97      |7:@(loop_lift … (initc ?? (ctape … outc1)) … Hloop2)
  98        [ * #s2 #t2 %
  99        | #c0 #Hhalt @daemon (* <step_lift_confR // *) ]
 100      |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 101       generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 102       >(trans_liftL_true sig M1 M2 ??)
 103        [ whd in ⊢ (??%?); whd in ⊢ (???%);
 104          @config_eq whd in ⊢ (???%); //
 105        | @(loop_Some ?????? Hloop10) ]
 106      ||4:cases outc1 #s1 #t1 %
 107      |5:
 108
 109          @(loop_liftR … Hloop2)
 110          |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 111           generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 112           >(trans_liftL_true sig M1 M2 ??)
 113            [ whd in ⊢ (??%?); whd in ⊢ (???%);
 114              @config_eq //
 115            | @(loop_Some ?????? Hloop10) ]
 116            ]
 117 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 118   % //
 119 ]
 120 qed.
 121 (* We do not distinuish an input tape *)
 122
 123 record TM (sig:FinSet): Type[1] ≝
 124 { states : FinSet;
 125   trans : states × (option sig) → states × (option (sig × move));
 126   start: states;
 127   halt : states → bool
 128 }.
 129
 130 record config (sig:FinSet) (M:TM sig): Type[0] ≝
 131 { cstate : states sig M;
 132   ctape: tape sig
 133 }.
 134
 135 definition option_hd ≝ λA.λl:list A.
 136   match l with
 137   [nil ⇒ None ?
 138   |cons a _ ⇒ Some ? a
 139   ].
 140
 141 definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
 142   match m with
 143   [ None ⇒ t
 144   | Some m1 ⇒
 145     match \snd m1 with
 146     [ R ⇒ mk_tape sig ((\fst m1)::(left ? t)) (tail ? (right ? t))
 147     | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m1)::(right ? t))
 148     ]
 149   ].
 150
 151 definition step ≝ λsig.λM:TM sig.λc:config sig M.
 152   let current_char ≝ option_hd ? (right ? (ctape ?? c)) in
 153   let 〈news,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
 154   mk_config ?? news (tape_move sig (ctape ?? c) mv).
 155
 156 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 157   match n with
 158   [ O ⇒ None ?
 159   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 160   ].
 161
 162 lemma loop_incr : ∀A,f,p,k1,k2,a1,a2.
 163   loop A k1 f p a1 = Some ? a2 →
 164     loop A (k2+k1) f p a1 = Some ? a2.
 165 #A #f #p #k1 #k2 #a1 #a2 generalize in match a1; elim k1
 166 [normalize #a0 #Hfalse destruct
 167 |#k1' #IH #a0 <plus_n_Sm whd in ⊢ (??%? → ??%?);
 168  cases (true_or_false (p a0)) #Hpa0 >Hpa0 whd in ⊢ (??%? → ??%?); // @IH
 169 ]
 170 qed.
 171
 172 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 173  ∀k1,k2,a1,a2,a3,a4.
 174    loop A k1 f p a1 = Some ? a2 →
 175      f a2 = a3 → q a2 = false →
 176        loop A k2 f q a3 = Some ? a4 →
 177          loop A (k1+k2) f q a1 = Some ? a4.
 178 #Sig #f #p #q #Hpq #k1 elim k1
 179   [normalize #k2 #a1 #a2 #a3 #a4 #H destruct
 180   |#k1' #Hind #k2 #a1 #a2 #a3 #a4 normalize in ⊢ (%→?);
 181    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 182    [#eqa1a2 destruct #eqa2a3 #Hqa2 #H
 183     whd in ⊢ (??(??%???)?); >plus_n_Sm @loop_incr
 184     whd in ⊢ (??%?); >Hqa2 >eqa2a3 @H
 185    |normalize >(Hpq … pa1) normalize
 186     #H1 #H2 #H3 @(Hind … H2) //
 187    ]
 188  ]
 189 qed.
 190
 191 (*
 192 lemma loop_split : ∀A,f,p,q.(∀b. p b = false → q b = false) →
 193  ∀k1,k2,a1,a2,a3.
 194    loop A k1 f p a1 = Some ? a2 →
 195      loop A k2 f q a2 = Some ? a3 →
 196        loop A (k1+k2) f q a1 = Some ? a3.
 197 #Sig #f #p #q #Hpq #k1 elim k1
 198   [normalize #k2 #a1 #a2 #a3 #H destruct
 199   |#k1' #Hind #k2 #a1 #a2 #a3 normalize in ⊢ (%→?→?);
 200    cases (true_or_false (p a1)) #pa1 >pa1 normalize in ⊢ (%→?);
 201    [#eqa1a2 destruct #H @loop_incr //
 202    |normalize >(Hpq … pa1) normalize
 203     #H1 #H2 @(Hind … H2) //
 204    ]
 205  ]
 206 qed.
 207 *)
 208
 209 definition initc ≝ λsig.λM:TM sig.λt.
 210   mk_config sig M (start sig M) t.
 211
 212 definition Realize ≝ λsig.λM:TM sig.λR:relation (tape sig).
 213 ∀t.∃i.∃outc.
 214   loop ? i (step sig M) (λc.halt sig M (cstate ?? c)) (initc sig M t) = Some ? outc ∧
 215   R t (ctape ?? outc).
 216
 217 (* Compositions *)
 218
 219 definition seq_trans ≝ λsig. λM1,M2 : TM sig.
 220 λp. let 〈s,a〉 ≝ p in
 221   match s with
 222   [ inl s1 ⇒
 223       if halt sig M1 s1 then 〈inr … (start sig M2), None ?〉
 224       else
 225       let 〈news1,m〉 ≝ trans sig M1 〈s1,a〉 in
 226       〈inl … news1,m〉
 227   | inr s2 ⇒
 228       let 〈news2,m〉 ≝ trans sig M2 〈s2,a〉 in
 229       〈inr … news2,m〉
 230   ].
 231
 232 definition seq ≝ λsig. λM1,M2 : TM sig.
 233   mk_TM sig
 234     (FinSum (states sig M1) (states sig M2))
 235     (seq_trans sig M1 M2)
 236     (inl … (start sig M1))
 237     (λs.match s with
 238       [ inl _ ⇒ false | inr s2 ⇒ halt sig M2 s2]).
 239
 240 definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
 241   ∃am.R1 a1 am ∧ R2 am a2.
 242
 243 (*
 244 definition injectRl ≝ λsig.λM1.λM2.λR.
 245    λc1,c2. ∃c11,c12.
 246      inl … (cstate sig M1 c11) = cstate sig (seq sig M1 M2) c1 ∧
 247      inl … (cstate sig M1 c12) = cstate sig (seq sig M1 M2) c2 ∧
 248      ctape sig M1 c11 = ctape sig (seq sig M1 M2) c1 ∧
 249      ctape sig M1 c12 = ctape sig (seq sig M1 M2) c2 ∧
 250      R c11 c12.
 251
 252 definition injectRr ≝ λsig.λM1.λM2.λR.
 253    λc1,c2. ∃c21,c22.
 254      inr … (cstate sig M2 c21) = cstate sig (seq sig M1 M2) c1 ∧
 255      inr … (cstate sig M2 c22) = cstate sig (seq sig M1 M2) c2 ∧
 256      ctape sig M2 c21 = ctape sig (seq sig M1 M2) c1 ∧
 257      ctape sig M2 c22 = ctape sig (seq sig M1 M2) c2 ∧
 258      R c21 c22.
 259
 260 definition Rlink ≝ λsig.λM1,M2.λc1,c2.
 261   ctape sig (seq sig M1 M2) c1 = ctape sig (seq sig M1 M2) c2 ∧
 262   cstate sig (seq sig M1 M2) c1 = inl … (halt sig M1) ∧
 263   cstate sig (seq sig M1 M2) c2 = inr … (start sig M2). *)
 264
 265 interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
 266
 267 definition lift_confL ≝
 268   λsig,M1,M2,c.match c with
 269   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inl … s) t ].
 270 definition lift_confR ≝
 271   λsig,M1,M2,c.match c with
 272   [ mk_config s t ⇒ mk_config ? (seq sig M1 M2) (inr … s) t ].
 273
 274 definition halt_liftL ≝
 275   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 276   match s with
 277   [ inl s1 ⇒ halt sig M1 s1
 278   | inr _ ⇒ true ]. (* should be vacuous in all cases we use halt_liftL *)
 279
 280 definition halt_liftR ≝
 281   λsig.λM1,M2:TM sig.λs:FinSum (states ? M1) (states ? M2).
 282   match s with
 283   [ inl _ ⇒ false
 284   | inr s2 ⇒ halt sig M2 s2 ].
 285
 286 lemma p_halt_liftL : ∀sig,M1,M2,c.
 287   halt sig M1 (cstate … c) =
 288      halt_liftL sig M1 M2 (cstate … (lift_confL … c)).
 289 #sig #M1 #M2 #c cases c #s #t %
 290 qed.
 291
 292 lemma trans_liftL : ∀sig,M1,M2,s,a,news,move.
 293   halt ? M1 s = false →
 294   trans sig M1 〈s,a〉 = 〈news,move〉 →
 295   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inl … news,move〉.
 296 #sig (*#M1*) * #Q1 #T1 #init1 #halt1 #M2 #s #a #news #move
 297 #Hhalt #Htrans whd in ⊢ (??%?); >Hhalt >Htrans %
 298 qed.
 299
 300 lemma config_eq :
 301   ∀sig,M,c1,c2.
 302   cstate sig M c1 = cstate sig M c2 →
 303   ctape sig M c1 = ctape sig M c2 →  c1 = c2.
 304 #sig #M1 * #s1 #t1 * #s2 #t2 //
 305 qed.
 306
 307 lemma step_lift_confL : ∀sig,M1,M2,c0.
 308  halt ? M1 (cstate ?? c0) = false →
 309  step sig (seq sig M1 M2) (lift_confL sig M1 M2 c0) =
 310  lift_confL sig M1 M2 (step sig M1 c0).
 311 #sig #M1 (* * #Q1 #T1 #init1 #halt1 *) #M2 * #s * #lt
 312 #rs #Hhalt
 313 whd in ⊢ (???(????%));whd in ⊢ (???%);
 314 lapply (refl ? (trans ?? 〈s,option_hd sig rs〉))
 315 cases (trans ?? 〈s,option_hd sig rs〉) in ⊢ (???% → %);
 316 #s0 #m0 #Heq whd in ⊢ (???%);
 317 whd in ⊢ (??(???%)?); whd in ⊢ (??%?);
 318 >(trans_liftL … Heq)
 319 [% | //]
 320 qed.
 321
 322 lemma loop_liftL : ∀sig,k,M1,M2,c1,c2.
 323   loop ? k (step sig M1) (λc.halt sig M1 (cstate ?? c)) c1 = Some ? c2 →
 324     loop ? k (step sig (seq sig M1 M2))
 325       (λc.halt_liftL sig M1 M2 (cstate ?? c)) (lift_confL … c1) =
 326     Some ? (lift_confL … c2).
 327 #sig #k #M1 #M2 #c1 #c2 generalize in match c1;
 328 elim k
 329 [#c0 normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 330 |#k0 #IH #c0 whd in ⊢ (??%? → ??%?);
 331  lapply (refl ? (halt ?? (cstate sig M1 c0)))
 332  cases (halt ?? (cstate sig M1 c0)) in ⊢ (???% → ?); #Hc0 >Hc0
 333  [ >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = true)
 334    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2) %
 335    | // ]
 336  | >(?: halt_liftL ??? (cstate sig (seq ? M1 M2) (lift_confL … c0)) = false)
 337    [whd in ⊢ (??%? → ??%?); #Hc2 <(IH ? Hc2) @eq_f
 338     @step_lift_confL //
 339    | // ]
 340 qed.
 341
 342 STOP!
 343
 344 lemma loop_liftR : ∀sig,k,M1,M2,c1,c2.
 345   loop ? k (step sig M2) (λc.halt sig M2 (cstate ?? c)) c1 = Some ? c2 →
 346     loop ? k (step sig (seq sig M1 M2))
 347       (λc.halt sig (seq sig M1 M2) (cstate ?? c)) (lift_confR … c1) =
 348     Some ? (lift_confR … c2).
 349 #sig #k #M1 #M2 #c1 #c2
 350 elim k
 351 [normalize in ⊢ (??%? → ?); #Hfalse destruct (Hfalse)
 352 |#k0 #IH whd in ⊢ (??%? → ??%?);
 353  lapply (refl ? (halt ?? (cstate sig M2 c1)))
 354  cases (halt ?? (cstate sig M2 c1)) in ⊢ (???% → ?); #Hc0 >Hc0
 355  [ >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = true)
 356    [ whd in ⊢ (??%? → ??%?); #Hc2 destruct (Hc2)
 357    | (* ... *) ]
 358  | >(?: halt ?? (cstate sig (seq ? M1 M2) (lift_confR … c1)) = false)
 359    [whd in ⊢ (??%? → ??%?); #Hc2 <IH
 360      [@eq_f (* @step_lift_confR // *)
 361      |
 362    | // ]
 363 qed. *)
 364
 365 lemma loop_Some :
 366   ∀A,k,f,p,a,b.loop A k f p a = Some ? b → p b = true.
 367 #A #k #f #p #a #b elim k
 368 [normalize #Hfalse destruct
 369 |#k0 #IH whd in ⊢ (??%? → ?); cases (p a)
 370  [ normalize #H1 destruct
 371
 372 lemma trans_liftL_true : ∀sig,M1,M2,s,a.
 373   halt ? M1 s = true →
 374   trans sig (seq sig M1 M2) 〈inl … s,a〉 = 〈inr … (start ? M2),None ?〉.
 375 #sig #M1 #M2 #s #a
 376 #Hhalt whd in ⊢ (??%?); >Hhalt %
 377 qed.
 378
 379 lemma eq_ctape_lift_conf_L : ∀sig,M1,M2,outc.
 380   ctape sig (seq sig M1 M2) (lift_confL … outc) = ctape … outc.
 381 #sig #M1 #M2 #outc cases outc #s #t %
 382 qed.
 383
 384 lemma eq_ctape_lift_conf_R : ∀sig,M1,M2,outc.
 385   ctape sig (seq sig M1 M2) (lift_confR … outc) = ctape … outc.
 386 #sig #M1 #M2 #outc cases outc #s #t %
 387 qed.
 388
 389 theorem sem_seq: ∀sig,M1,M2,R1,R2.
 390   Realize sig M1 R1 → Realize sig M2 R2 →
 391     Realize sig (seq sig M1 M2) (R1 ∘ R2).
 392 #sig #M1 #M2 #R1 #R2 #HR1 #HR2 #t
 393 cases (HR1 t) #k1 * #outc1 * #Hloop1 #HM1
 394 cases (HR2 (ctape sig M1 outc1)) #k2 * #outc2 * #Hloop2 #HM2
 395 @(ex_intro … (k1+k2)) @(ex_intro … (lift_confR … outc2))
 396 %
 397 [@(loop_split ??????????? (loop_liftL … Hloop1))
 398  [* *
 399    [ #sl #tl whd in ⊢ (??%? → ?); #Hl %
 400    | #sr #tr whd in ⊢ (??%? → ?); #Hr destruct (Hr) ]
 401  ||4:cases outc1 #s1 #t1 %
 402  |5:@(loop_liftR … Hloop2)
 403  |whd in ⊢ (??(???%)?);whd in ⊢ (??%?);
 404   generalize in match Hloop1; cases outc1 #sc1 #tc1 #Hloop10
 405   >(trans_liftL_true sig M1 M2 ??)
 406   [ whd in ⊢ (??%?); whd in ⊢ (???%);
 407     @config_eq //
 408   | @(loop_Some ?????? Hloop10) ]
 409  ]
 410 | @(ex_intro … (ctape ? (seq sig M1 M2) (lift_confL … outc1)))
 411   % //
 412 ]
 413 qed.
 414
 415 (* boolean machines: machines with two distinguished halting states *)
 416
 417
 418
 419 (* old stuff *)
 420 definition empty_tapes ≝ λsig.λn.
 421 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
 422 elim n // normalize //
 423 qed.
 424
 425 definition init ≝ λsig.λM:TM sig.λi:(list sig).
 426   mk_config ??
 427     (start sig M)
 428     (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
 429     [ ].
 430
 431 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
 432   halt sig M (state sig M c).
 433
 434 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
 435   match n with
 436   [ O ⇒ None ?
 437   | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
 438   ].
 439
 440 (* Compute ? M f states that f is computed by M *)
 441 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 442 ∀l.∃i.∃c.
 443   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 444   out ?? c = f l.
 445
 446 (* for decision problems, we accept a string if on termination
 447 output is not empty *)
 448
 449 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 450 ∀l.∃i.∃c.
 451   loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
 452   (isnilb ? (out ?? c) = false).
 453
 454 (* alternative approach.
 455 We define the notion of computation. The notion must be constructive,
 456 since we want to define functions over it, like lenght and size
 457
 458 Perche' serve Type[2] se sposto a e b a destra? *)
 459
 460 inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
 461   mk_move: p a = false → b = f a → cmove A f p a b.
 462
 463 inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
 464 | empty : ∀a. cstar A M a a
 465 | more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
 466
 467 definition computation ≝ λsig.λM:TM sig.
 468   cstar ? (cmove ? (step sig M) (stop sig M)).
 469
 470 definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
 471   ∀l.∃c.computation sig M (init sig M l) c →
 472    (stop sig M c = true) ∧ out ?? c = f l.
 473
 474 definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
 475   ∀l.∃c.computation sig M (init sig M l) c →
 476    (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).