-
Notifications
You must be signed in to change notification settings - Fork 0
/
TM.v
152 lines (109 loc) · 5.46 KB
/
TM.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(** * Halting problem for multi-tape and single-tape Turing machines HaltMTM and HaltTM 1 *)
Require Import Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes.
Require Import Vector List.
Unset Implicit Arguments.
(* * Turing machines *)
(* The definition of Turing machines is due to Asperti & Ricciotti's "A formalization of multi-tape Turing machines" (2015) and the accompanying Matita code. *)
Section Fix_Sigma.
(* The alphabet type *)
Variable Σ : Type.
(* ** Tapes
Tapes are either
- empty (niltape),
- non-empty with the head to the left of the content (leftof),
- non-empty with the head to the right of the content (rightof),
- or non-empty with the head on the content (midtape).
The representation does not allow for blank symbols, instead a blank symbol has to be part of the alphabet Σ. The seeming redundancy allows for a unique representation of every tape and no well-formedness predicate is needed.
*)
Inductive tape : Type :=
| niltape : tape
| leftof : Σ -> list Σ -> tape
| rightof : Σ -> list Σ -> tape
| midtape : list Σ -> Σ -> list Σ -> tape.
(* The current function returns the current symbol, if there is one. If None is returned, this means that the head is on a part of the tape which has never been written before. *)
Definition current (t : tape) : option Σ :=
match t with
| midtape _ a _ => Some a
| _ => None
end.
Inductive move : Type := Lmove : move | Rmove : move | Nmove : move.
(* Moving to the left on leftof and to the right on rightof has no effect.
*)
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.
(* The write function wr takes option Σ as argument. None indicates that nothing should be written. This is necessary because the current symbol might be None, i.e. one can not simply write the current symbol since it might not exist. *)
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.
(* Differences to traditional presentations:
The tape representation and the implementation of mv is different to presentations of Turing machines in the literature. Moving to the right while on a rightof tape is the identity. One can obtain the more traditional behaviour by assuming a blank symbol as part of the alphabet and always writing a blank when the current symbol is None.
This also means that moving n steps to the right, and then n steps to the left does not yield the same tape, since the moves to the right might have been uneffective. With an explicit blank symbol, moving n steps to the right while always writing the current symbol and the blank if current is None, and the moving n steps to the left is semantically the identity, but still not syntactically.
*)
Arguments niltape _, {_}.
Arguments leftof _ _ _, {_} _ _.
Arguments rightof _ _ _, {_} _ _.
Arguments midtape _ _ _ _, {_} _ _ _.
Arguments current {_} _.
Arguments wr {_} _ _.
Arguments mv {_} _.
Section Fix_Alphabet.
(* The alphabet type, assumed as finite type *)
Variable Σ : finType.
(* finType is defined as a pair of a type with decidable equality, and a duplicate-free list of all elements of the type.
We have
Lemma finType_equiv (X : finType) :
{n & {f : X -> Fin.t n & { g : Fin.t n -> X | (forall x, g (f x) = x) /\ forall i, f (g i) = i }}}.
in Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesEquiv.
*)
(* The number of tapes *)
Variable n : nat.
(* Definition of multi-tape Turing machines *)
Record TM : Type :=
{
(* type of states of the TM: *)
state : finType;
(* transition function: *)
trans : state * (Vector.t (option Σ) n) -> state * (Vector.t ((option Σ) * move) n);
(* start state: *)
start: state;
(* decidable subset of halting states: *)
halt : state -> bool
}.
(* evaluation relation, uses trans until a halting state is reached: *)
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.