Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes.
Require Import Vector List.
Unset Implicit Arguments.
Section Fix_Sigma.
Variable Σ : Type.
Inductive tape : Type :=
| niltape : tape
| leftof : Σ -> list Σ -> tape
| rightof : Σ -> list Σ -> tape
| midtape : list Σ -> Σ -> list Σ -> tape.
Definition current (t : tape) : option Σ :=
match t with
| midtape _ a _ => Some a
| _ => None
end.
Inductive move : Type := Lmove : move | Rmove : move | Nmove : move.
Definition mv (m : move) (t : tape) :=
match m, t with
| Lmove, rightof l ls => midtape ls l nil
| Lmove, midtape nil m rs => leftof m rs
| Lmove, midtape (l :: ls) m rs => midtape ls l (m :: rs)
| Rmove, leftof r rs => midtape nil r rs
| Rmove, midtape ls m nil => rightof m ls
| Rmove, midtape ls m (r :: rs) => midtape (m :: ls) r rs
| _, _ => t
end.
Definition wr (s : option Σ) (t : tape) : tape :=
match s, t with
| None, t => t
| Some a, niltape => midtape nil a nil
| Some a, leftof r rs => midtape nil a (r :: rs)
| Some a, midtape ls b rs => midtape ls a rs
| Some a, rightof l ls => midtape (l :: ls) a nil
end.
End Fix_Sigma.
Arguments niltape _, {_}.
Arguments leftof _ _ _, {_} _ _.
Arguments rightof _ _ _, {_} _ _.
Arguments midtape _ _ _ _, {_} _ _ _.
Arguments current {_} _.
Arguments wr {_} _ _.
Arguments mv {_} _.
Section Fix_Alphabet.
Variable Σ : finType.
Variable n : nat.
Record TM : Type :=
{
state : finType;
trans : state * (Vector.t (option Σ) n) -> state * (Vector.t ((option Σ) * move) n);
start: state;
halt : state -> bool
}.
Inductive eval (M : TM) (q : state M) (t : Vector.t (tape Σ) n) : state M -> Vector.t (tape Σ) n -> Prop :=
| eval_halt :
halt M q = true ->
eval M q t q t
| eval_step q' a q'' t' :
halt M q = false ->
trans M (q, Vector.map current t) = (q', a) ->
eval M q' (Vector.map2 (fun tp '(c,m) => mv m (wr c tp)) t a) q'' t' ->
eval M q t q'' t'.
End Fix_Alphabet.
Arguments state {_ _} m : rename.
Arguments trans {_ _} m _, {_ _ m} _ : rename.
Arguments start {_ _} m : rename.
Arguments halt {_ _} m _, {_ _ m} _ : rename.
Arguments eval {_ _} _ _ _ _ _.
Arguments Build_TM {_ _ _} _ _ _.
Definition HaltsTM {Σ: finType} {n: nat} (M : TM Σ n) (t : Vector.t (tape Σ) n) :=
exists q' t', eval M (start M) t q' t'.
Arguments HaltsTM _ _ _ _, {_ _} _ _.
Definition HaltTM (n : nat) : {Σ : finType & TM Σ n & Vector.t (tape Σ) n} -> Prop :=
fun '(existT2 _ _ Σ M t) => HaltsTM M t.
Definition HaltMTM : {'(n,Σ) : nat * finType & TM Σ n & Vector.t (tape Σ) n} -> Prop :=
fun '(existT2 _ _ (n, Σ) M t) => HaltsTM M t.