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