Singletape Turing Machines
Adopted definitions from the formalization of Multitape Turing Machines taken from Asperti, Riciotti "Formalizing Turing Machines" and accompanying Matita foramlisationSection Fix_Sigma.
Variable sig : finType.
Global Instance eq_dec_sig: eq_dec sig.
Proof. exact _. Defined.
Definition of the tape
Inductive tape : Type :=
| niltape : tape
| leftof : sig -> list sig -> tape
| rightof : sig -> list sig -> tape
| midtape : list sig -> sig -> list sig -> tape.
Global Instance eq_dec_tape: eq_dec tape.
Proof. unfold dec. decide equality; decide (e=e0); decide (l=l0); auto;
decide (l= l1); decide (l0=l2); auto.
Defined.
Definition tapeToList (t : tape) : list sig :=
match t with
| niltape => []
| leftof s r => s :: r
| rightof s l => List.rev (s :: l)
| midtape l c r => (List.rev l) ++ [c] ++ r
end.
Definition sizeOfTape t := |tapeToList t|.
(* symbol under head *)
Definition current :=
fun (t : tape) =>
match t with
| midtape _ c _ => Some c
| _ => None
end.
(* symbol-list left of head *)
Definition left :=
fun (t : tape) =>
match t with
| niltape => []
| leftof _ _ => []
| rightof s l => s :: l
| midtape l _ _ => l
end.
(* symbol-list right of head *)
Definition right :=
fun (t : tape) =>
match t with
| niltape => []
| leftof s r => s :: r
| rightof _ _ => []
| midtape _ _ r => r
end.
(* makes a tape from left, current, right *)
Definition mk_tape ls c rs :=
match c with
| Some c => midtape ls c rs
| None => match ls with
| List.nil => match rs with
| List.nil => niltape
| r :: rs => leftof r rs
end
| l :: ls => rightof l ls
end
end.
Inductive move : Type := L : move | R : move | N : move.
Global Instance move_eq_dec : eq_dec move.
Proof.
intros. hnf. decide equality.
Defined.
Global Instance move_finC : finTypeC (EqType move).
Proof.
apply (FinTypeC (enum := [L; R; N])).
intros []; now cbv.
Qed.
Record sTM : Type :=
{
states : finType; (* states of the TM *)
trans : states * (option sig) -> states * ((option sig) * move); (* the transition function *)
start: states; (* the start state *)
halt : states -> bool (* decidable subset of halting states *)
}.
Definition of tape movements
Definition tape_move_right :=
fun (t : tape) =>
match t with
niltape => niltape
| rightof _ _ =>t
| leftof a rs => midtape [ ] a rs
| midtape ls a rs =>
match rs with
[] => rightof a ls
| a0 :: rs0 => midtape (a::ls) a0 rs0
end
end.
Definition tape_move_left :=
fun (t : tape) =>
match t with
niltape => niltape
| leftof _ _ => t
| rightof a ls => midtape ls a [ ]
| midtape ls a rs =>
match ls with
[] => leftof a rs
| a0 :: ls0 => midtape ls0 a0 (a::rs)
end
end.
Definition tape_move := fun (t : tape) (m : move) =>
match m with R => tape_move_right t | L => tape_move_left t | N => t end.
Writing on the tape
Definition tape_write := fun (t : tape) (s : option sig) =>
match s with
None => t
| Some s0 => midtape (left t) s0 (right t)
end.
A single step of the machine
Definition tape_move_mono := fun (t : tape) (mv : option sig * move) =>
tape_move (tape_write t (fst mv)) (snd mv).
Record mconfig (states:finType) : Type :=
mk_mconfig
{
cstate : states;
ctape : tape
}.
Instance eq_dec_conf (s: finType): eq_dec (mconfig s).
Proof. intros x y. destruct x,y.
decide (cstate0 = cstate1); decide (ctape0 = ctape1);
try (right; intros H; now inversion H). left. now subst.
Qed.
Definition step :=
fun (M:sTM) (c:mconfig (states M)) =>
let (news,action) := trans (cstate c, current (ctape c))
in mk_mconfig news (tape_move_mono (ctape c) action).
Initial configuration
Run the machine i steps until it halts Returns None iff the maschine does not halt within i steps
Definition loop (A:Type) := fix l n (f:A -> A) (p : A -> bool) a {struct n}:=
if p a then Some a else
match n with
O => None
| S m => l m f p (f a)
end.
Definition loopM := fun (M :sTM) (i : nat) cin =>
loop i (@step M) (fun c => halt (cstate c)) cin.
if p a then Some a else
match n with
O => None
| S m => l m f p (f a)
end.
Definition loopM := fun (M :sTM) (i : nat) cin =>
loop i (@step M) (fun c => halt (cstate c)) cin.
Definition TMterminates (M: sTM) (start: mconfig (states M)) :=
exists i outc, loopM i start = Some outc.
Lemma loop_step_not A f p (a : A) i out:
loop i f p (f a) = out -> (p a = false) -> (loop (S i) f p a = out).
Proof.
destruct i; intros H HF; cbn in *; rewrite HF; destruct (p (f a)); assumption.
Qed.
Inductive reach (M: sTM) : mconfig (states M) -> mconfig (states M) -> Prop :=
|reachI c : reach c c
|reachS c d : reach (step c) d -> (halt (cstate c) = false) -> reach c d.
Hint Constructors reach.
Definition Halt (M: sTM) (start: mconfig (states M)) :=
exists (f: mconfig (states M)), halt (cstate f)=true /\ reach start f.
Lemma TM_terminates_Halt (M:sTM) (start: mconfig (states M)) :
TMterminates start <-> Halt start.
Proof.
split.
- intros [i [fin H]]. revert H. revert start. induction i; intros start H; cbn in *.
+ exists start. destruct (halt (cstate start)) eqn: HS. split; auto. inv H.
+ destruct (halt (cstate start)) eqn: HS.
* inv H. exists fin. now split.
* destruct (IHi (step start)) as [q [HF RF]]. unfold loopM. assumption.
exists q. split. assumption. now apply reachS.
- intros [f [HF RF]]. revert HF. induction RF; intros HR.
+ exists 0, c. cbn. now rewrite HR.
+ destruct (IHRF HR) as [i [out LH]]. exists (S i), out. now apply loop_step_not.
Qed.
End Fix_Sigma.
Definition HaltD (S: {sig:finType & sTM sig & tape sig}) :=
Halt (initc (projT2 (sigT_of_sigT2 S)) (projT3 S)).
Definition HaltD' (S: (sigT (fun (sig:finType) => (sigT (fun (M:sTM sig) => (mconfig sig (states M))))))) :=
Halt (projT2 (projT2 S)).
Definition Reach (S: (sigT (fun (sig:finType) =>
(sigT (fun (M:sTM sig) => prod (mconfig sig (states M))
(mconfig sig (states M))))))) :=
let (c1,c2) := (projT2 (projT2 S)) in
reach c1 c2.