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