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