Lax251941.TuringMachines

Single-tape Turing machines as string rewriting

concepts/Lax251941/TuringMachines.lean · lax-251941

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A (possibly nondeterministic) single-tape Turing machine, presented as in Sipser's Introduction to the Theory of Computation, Section 5.2: a finite transition table with entries $\delta(q, a) = (r, b, \mathrm{dir})$ , a start state and an accept state. A configuration is a string $u\,q\,v$ over tape symbols and states, where $u$ and $v$ are the tape contents to the left and to the right of the head and $q$ is the current state, and one step of the machine rewrites the configuration string locally around the state symbol: $q\,a \to b\,r$ for a move to the right, and $c\,q\,a \to r\,c\,b$ for a move to the left, which is possible only if there is a symbol $c$ to the left of the head; a blank may be appended at the right-hand end, standing for the infinitely many blanks that a written configuration suppresses. The machine accepts the input $w$ if some configuration containing the accept state is reachable from the starting configuration $q_0\,w$ .

This is the combinatorial shape that the reduction to the Post correspondence problem manipulates, so it is what the machine is here: a string rewriting system — an alphabet, a finite list of rules $u \to v$ applied in arbitrary context, and a list of symbols that may be appended on the right — whose rules are read off the transition table.

Lean source view on GitHub

1	import Mathlib.Computability.Primrec.List
2	import Mathlib.Logic.Relation
3
4	/-!
5	---
6	title: Single-tape Turing machines as string rewriting
7	type: definition
8	---
9	A (possibly nondeterministic) single-tape Turing machine, presented as in
10	Sipser's Introduction to the Theory of Computation, Section 5.2: a finite
11	transition table with entries $\delta(q, a) = (r, b, \mathrm{dir})$ , a start
12	state and an accept state. A configuration is a string $u\,q\,v$ over tape
13	symbols and states, where $u$ and $v$ are the tape contents to the left and to
14	the right of the head and $q$ is the current state, and one step of the machine
15	rewrites the configuration string locally around the state symbol:
16	$q\,a \to b\,r$ for a move to the right, and $c\,q\,a \to r\,c\,b$ for a move to
17	the left, which is possible only if there is a symbol $c$ to the left of the
18	head; a blank may be appended at the right-hand end, standing for the
19	infinitely many blanks that a written configuration suppresses. The machine
20	accepts the input $w$ if some configuration containing the accept state is
21	reachable from the starting configuration $q_0\,w$ .
22
23	This is the combinatorial shape that the reduction to the Post correspondence
24	problem manipulates, so it is what the machine is here: a *string rewriting
25	system* — an alphabet, a finite list of rules $u \to v$ applied in arbitrary
26	context, and a list of symbols that may be appended on the right — whose rules
27	are read off the transition table.
28
29	# Formalization notes
30
31	Tape symbols and states are natural numbers, `0` being the blank. The alphabet
32	`Sym` in which configurations are written also carries the four auxiliary
33	symbols of Sipser's reduction (`#`, the start marker, `∗`, `◇`); they play no
34	role in the definition of the machine and are here only so that computation
35	histories and configurations are strings over one and the same alphabet.
36
37	The tape symbols and the states of a machine are the finitely many that its
38	table, its two distinguished states and the input mention. A move to the left
39	needs the symbol to the left of the head, so there is one left rule per tape
40	symbol `c`; the machine never moves its head off the left end. `Reaches` is
41	the reflexive transitive closure of the one-step relation. The `Primcodable`
42	instance encodes a machine by its table and its two states, so that decision
43	problems about machines can be stated with mathlib's `ComputablePred`.
44	-/
45
46	namespace Lax251941.TuringMachines
47
48	/-- The symbols in which configurations of a Turing machine, and the strings of
49	Sipser's reduction, are written. -/
50	inductive Sym where
51	/-- A tape symbol; `Sym.tape 0` is the blank. -/
52	\| tape : ℕ → Sym
53	/-- A state of the machine. -/
54	\| state : ℕ → Sym
55	/-- The separator `#` between consecutive configurations of a history. -/
56	\| hash : Sym
57	/-- The marker opening a computation history. -/
58	\| start : Sym
59	/-- The auxiliary symbol `∗` of the reduction. -/
60	\| star : Sym
61	/-- The auxiliary symbol `◇` of the reduction. -/
62	\| diamond : Sym
63	deriving DecidableEq, Repr
64
65	/-- A string rewriting system: an alphabet, a finite list of rewriting rules
66	`u → v` applied in arbitrary context, and a list of symbols that may be appended
67	at the right end of a string. -/
68	structure SRS (α : Type*) where
69	/-- The alphabet. -/
70	alphabet : List α
71	/-- The rewriting rules `u → v`. -/
72	rules : List (List α × List α)
73	/-- Symbols that may be appended at the right-hand end of a string. -/
74	ext : List α
75
76	/-- One application of a rule, in a context `l _ r`. -/
77	inductive StepRule {α : Type*} (rules : List (List α × List α)) : List α → List α → Prop
78	\| mk (l u v r : List α) : (u, v) ∈ rules → StepRule rules (l ++ u ++ r) (l ++ v ++ r)
79
80	/-- One step of a rewriting system: a rule application, or appending one of the
81	designated symbols on the right. -/
82	inductive Step {α : Type*} (S : SRS α) : List α → List α → Prop
83	\| rule {a b : List α} : StepRule S.rules a b → Step S a b
84	\| ext {c : List α} {x : α} : x ∈ S.ext → Step S c (c ++ [x])
85
86	/-- Reachability: the reflexive transitive closure of `Step`. -/
87	def Reaches {α : Type*} (S : SRS α) : List α → List α → Prop := Relation.ReflTransGen (Step S)
88
89	/-- A single-tape Turing machine: a transition table whose entry `(q, a, r, b, dir)`
90	means `δ(q, a) = (r, b, dir)`, `dir = true` being a move to the right and
91	`dir = false` a move to the left, together with a start state and an accept
92	state. -/
93	structure TM where
94	/-- The transition table. -/
95	trans : List (ℕ × ℕ × ℕ × ℕ × Bool)
96	/-- The start state. -/
97	q0 : ℕ
98	/-- The accept state. -/
99	qacc : ℕ
100
101	namespace TM
102
103	variable (M : TM) (w : List ℕ)
104
105	/-- The tape symbols of a machine run on `w`: the blank, the letters of `w`, and
106	the symbols read or written by the table. -/
107	def tapeSyms : List ℕ :=
108	0 :: (w ++ M.trans.map (fun x => x.2.1) ++ M.trans.map (fun x => x.2.2.2.1))
109
110	/-- The states of a machine: the start state, the accept state and the states of
111	the table. -/
112	def states : List ℕ :=
113	M.q0 :: M.qacc :: (M.trans.map (fun x => x.1) ++ M.trans.map (fun x => x.2.2.1))
114
115	/-- The alphabet in which the configurations of a run on `w` are written. -/
116	def alphabet : List Sym :=
117	(M.tapeSyms w).map Sym.tape ++ M.states.map Sym.state
118
119	/-- The rewriting rules `q a → b r` of the moves to the right. -/
120	def rightRules : List (List Sym × List Sym) :=
121	M.trans.filterMap fun x =>
122	if x.2.2.2.2 then
123	some ([Sym.state x.1, Sym.tape x.2.1], [Sym.tape x.2.2.2.1, Sym.state x.2.2.1])
124	else none
125
126	/-- The rewriting rules `c q a → r c b` of the moves to the left, one for every
127	tape symbol `c` to the left of the head. -/
128	def leftRules : List (List Sym × List Sym) :=
129	(M.tapeSyms w).flatMap fun c =>
130	M.trans.filterMap fun x =>
131	if x.2.2.2.2 then none
132	else some ([Sym.tape c, Sym.state x.1, Sym.tape x.2.1],
133	[Sym.state x.2.2.1, Sym.tape c, Sym.tape x.2.2.2.1])
134
135	/-- The rewriting rules describing the single steps of the machine. -/
136	def transRules : List (List Sym × List Sym) := M.rightRules ++ M.leftRules w
137
138	/-- The rewriting system of the machine on the input `w`: its step rules, with a
139	blank appendable on the right. -/
140	def machineSRS : SRS Sym where
141	alphabet := M.alphabet w
142	rules := M.transRules w
143	ext := [Sym.tape 0]
144
145	/-- The starting configuration `q₀ w`. -/
146	def startCfg : List Sym := Sym.state M.q0 :: w.map Sym.tape
147
148	/-- The machine accepts `w` if a configuration containing the accept state is
149	reachable from the starting configuration. -/
150	def Accepts : Prop :=
151	∃ C, Reaches (M.machineSRS w) (M.startCfg w) C ∧ Sym.state M.qacc ∈ C
152
153	end TM
154
155	/-- A machine is encoded by its transition table and its two distinguished states.
156	-/
157	def tmEquiv : TM ≃ List (ℕ × ℕ × ℕ × ℕ × Bool) × ℕ × ℕ where
158	toFun M := (M.trans, M.q0, M.qacc)
159	invFun x := ⟨x.1, x.2.1, x.2.2⟩
160	left_inv := by rintro ⟨t, a, b⟩; rfl
161	right_inv := by rintro ⟨t, a, b⟩; rfl
162
163	instance : Primcodable TM := Primcodable.ofEquiv _ tmEquiv
164
165	end Lax251941.TuringMachines
166

Formalization notes

Tape symbols and states are natural numbers, $0$ being the blank. The alphabet $Sym$ in which configurations are written also carries the four auxiliary symbols of Sipser's reduction (`#`, the start marker, $∗$ , $◇$ ); they play no role in the definition of the machine and are here only so that computation histories and configurations are strings over one and the same alphabet.

The tape symbols and the states of a machine are the finitely many that its table, its two distinguished states and the input mention. A move to the left needs the symbol to the left of the head, so there is one left rule per tape symbol $c$ ; the machine never moves its head off the left end. $Reaches$ is the reflexive transitive closure of the one-step relation. The $Primcodable$ instance encodes a machine by its table and its two states, so that decision problems about machines can be stated with mathlib's $ComputablePred$ .

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Single-tape Turing machines as string rewriting

Flags

Flag this concept