-definition empty_tapes ≝ λsig.λn.
-mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
-elim n // normalize //
-qed.
-
-definition init ≝ λsig.λM:TM sig.λi:(list sig).
- mk_config ??
- (start sig M)
- (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
- [ ].
-
-definition stop ≝ λsig.λM:TM sig.λc:config sig M.
- halt sig M (state sig M c).
-
-let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
- match n with
- [ O ⇒ None ?
- | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
- ].
-
-(* Compute ? M f states that f is computed by M *)
-definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
-∀l.∃i.∃c.
- loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
- out ?? c = f l.
-
-(* for decision problems, we accept a string if on termination
-output is not empty *)
-
-definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
-∀l.∃i.∃c.
- loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
- (isnilb ? (out ?? c) = false).
-
-(* alternative approach.
-We define the notion of computation. The notion must be constructive,
-since we want to define functions over it, like lenght and size
-
-Perche' serve Type[2] se sposto a e b a destra? *)
-
-inductive cmove (A:Type[0]) (f:A→A) (p:A →bool) (a,b:A): Type[0] ≝
- mk_move: p a = false → b = f a → cmove A f p a b.
-
-inductive cstar (A:Type[0]) (M:A→A→Type[0]) : A →A → Type[0] ≝
-| empty : ∀a. cstar A M a a
-| more : ∀a,b,c. M a b → cstar A M b c → cstar A M a c.
-
-definition computation ≝ λsig.λM:TM sig.
- cstar ? (cmove ? (step sig M) (stop sig M)).
-
-definition Compute_expl ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
- ∀l.∃c.computation sig M (init sig M l) c →
- (stop sig M c = true) ∧ out ?? c = f l.
-
-definition ComputeB_expl ≝ λsig.λM:TM sig.λf:(list sig) → bool.
- ∀l.∃c.computation sig M (init sig M l) c →
- (stop sig M c = true) ∧ (isnilb ? (out ?? c) = false).