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.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "basics/vectors.ma".
14 record tape (sig:FinSet): Type[0] ≝
19 inductive move : Type[0] ≝
24 (* We do not distinuish an input tape *)
26 record TM (sig:FinSet): Type[1] ≝
28 tapes_no: nat; (* additional working tapes *)
29 trans : states × (Vector (option sig) (S tapes_no)) →
30 states × (Vector (sig × move) (S tapes_no)) × (option sig) ;
36 record config (sig:FinSet) (M:TM sig): Type[0] ≝
37 { state : states sig M;
38 tapes : Vector (tape sig) (S (tapes_no sig M));
42 definition option_hd ≝ λA.λl:list A.
48 definition tape_move ≝ λsig.λt: tape sig.λm:sig × move.
50 [ R ⇒ mk_tape sig ((\fst m)::(left ? t)) (tail ? (right ? t))
51 | L ⇒ mk_tape sig (tail ? (left ? t)) ((\fst m)::(right ? t))
52 | N ⇒ mk_tape sig (left ? t) ((\fst m)::(tail ? (right ? t)))
55 definition current_chars ≝ λsig.λM:TM sig.λc:config sig M.
56 vec_map ?? (λt.option_hd ? (right ? t)) (S (tapes_no sig M)) (tapes ?? c).
58 definition opt_cons ≝ λA.λa:option A.λl:list A.
64 definition step ≝ λsig.λM:TM sig.λc:config sig M.
65 let 〈news,mvs,outchar〉 ≝ trans sig M 〈state ?? c,current_chars ?? c〉 in
68 (pmap_vec ??? (tape_move sig) ? (tapes ?? c) mvs)
69 (opt_cons ? outchar (out ?? c)).
71 definition empty_tapes ≝ λsig.λn.
72 mk_Vector ? n (make_list (tape sig) (mk_tape sig [] []) n) ?.
73 elim n // normalize //
76 definition init ≝ λsig.λM:TM sig.λi:(list sig).
79 (vec_cons ? (mk_tape sig [] i) ? (empty_tapes sig (tapes_no sig M)))
82 definition stop ≝ λsig.λM:TM sig.λc:config sig M.
83 halt sig M (state sig M c).
85 let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
88 | S m ⇒ if p a then (Some ? a) else loop A m f p (f a)
91 (* Compute ? M f states that f is computed by M *)
92 definition Compute ≝ λsig.λM:TM sig.λf:(list sig) → (list sig).
94 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
97 (* for decision problems, we accept a string if on termination
98 output is not empty *)
100 definition ComputeB ≝ λsig.λM:TM sig.λf:(list sig) → bool.
102 loop ? i (step sig M) (stop sig M) (init sig M l) = Some ? c ∧
103 (isnilb ? (out ?? c) = false).