Wide machines

Lax822549.WideMachines · concepts/Lax822549/WideMachines.lean · lax-822549

definition

Loading review…

Natural Language Statement

Definition

A wide machine is a Turing machine whose control is an ordinary part of its instance and whose tape is addressed by the subsets of the instance: its points are the subsets of the universe and its elements, the subsets being the tape cells and the time steps, ordered as binary numbers. An instance of size $n$ thus describes a machine with $2^n$ cells and $2^n$ steps. Wide acceptance holds of a well-formed instance whose machine accepts within its $2^n$ steps; wide acceptance in space holds when it accepts within its $2^n$ cells, with no bound on the number of steps, and its deterministic form when moreover the machine is deterministic.

Concept map

6 concepts; 5 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Order.PiLex
2	import Mathlib.Data.Prod.Lex
3	import Mathlib.Data.Fintype.EquivFin
4	import Mathlib.ModelTheory.Order
5	import Mathlib.ModelTheory.Semantics
6	import Mathlib.ModelTheory.Complexity
7	import Mathlib.Tactic.FinCases
8	import Mathlib.Logic.Equiv.Fin.Basic
9	import Mathlib.Data.Finite.Sigma
10	import Mathlib.Data.Fintype.Lattice
11	import Mathlib.Order.Lattice.Nat
12	import Mathlib.Data.Set.Card
13	import Mathlib.Data.Fintype.Pigeonhole
14	import Mathlib.Dynamics.FixedPoints.Basic
15	import Mathlib.Algebra.BigOperators.Finprod
16	import Mathlib.Data.Set.Finite.Lemmas
17	import Mathlib.SetTheory.Cardinal.Finite
18	import Mathlib.Logic.Equiv.Prod
19	import Lax904597.Machines
20	import Lax904597.Problems
21	import Lax485149.Problems
22	import Lax134656.SpaceBoundedMachines
23	import Lax535992.DeterministicMachines
24
25	/-!
26	---
27	title: Wide machines
28	type: definition
29	---
30	A wide machine is a Turing machine whose control is an ordinary part of its
31	instance and whose tape is addressed by the subsets of the instance: its
32	points are the subsets of the universe and its elements, the subsets being
33	the tape cells and the time steps, ordered as binary numbers. An instance of
34	size $n$ thus describes a machine with $2^n$ cells and $2^n$ steps. Wide
35	acceptance holds of a well-formed instance whose machine accepts within its
36	$2^n$ steps; wide acceptance in space holds when it accepts within its $2^n$
37	cells, with no bound on the number of steps, and its deterministic form when
38	moreover the machine is deterministic.
39	-/
40
41	namespace Lax822549.WideMachines
42
43	open Lax904597.Machines
44
45	open FirstOrder
46
47	open Language Structure
48
49	section Addresses
50
51	variable {α : Type}
52
53	/-- The binary-number order on addresses: the two subsets agree, or, at some
54	element where the first is out and the second in, they agree at every strictly
55	smaller element. Written with the strict order spelled out as
56	`Le y x ∧ ¬ Le x y`, which is the shape the defining sentence of the expansion
57	realizes to. -/
58	def WMSetLe (Le : α → α → Prop) (s t : α → Prop) : Prop :=
59	(∀ x, s x ↔ t x) ∨
60	∃ x, (∀ y, (Le y x ∧ ¬Le x y) → (s y ↔ t y)) ∧ ¬s x ∧ t x
61
62	/-- The address of an element: the initial segment it cuts, which is where
63	the element's input symbol is written. -/
64	def WMDown (Le : α → α → Prop) (s : α → Prop) (x : α) : Prop := ∀ y, s y ↔ Le y x
65
66	/-- The cell of an element on a file: the initial segment it cuts among the
67	elements the file has a register for. The wide machine's register channel and
68	the wide tiling's bottom row are both described at these addresses – a file of
69	cells rather than the ruler of all the segments. -/
70	def WMFileSeg (Le : α → α → Prop) (Has : α → Prop) (s : α → Prop) (x : α) : Prop :=
71	∀ y, s y ↔ (Le y x ∧ Has y)
72
73	end Addresses
74
75	open FirstOrder
76
77	open FirstOrder.Language
78
79	/-- Relation symbols of wide-machine instances: the control of
80	`FirstOrder.Language.turing`, with the positions and their order replaced by an
81	order on the elements – the digits of an address. -/
82	inductive wideRel : ℕ → Type
83	/-- `wmLe x y`: the order on the elements, along which an address is read as a
84	binary number. -/
85	\| wle : wideRel 2
86	/-- `wmTr τ`: `τ` is a transition. -/
87	\| tr : wideRel 1
88	/-- `wmStart q`: `q` is a start state. -/
89	\| start : wideRel 1
90	/-- `wmAcc q`: `q` is an accepting state. -/
91	\| acc : wideRel 1
92	/-- `wmBlank a`: `a` is the blank symbol. -/
93	\| blank : wideRel 1
94	/-- `wmRight τ`: the transition `τ` moves the head right. -/
95	\| right : wideRel 1
96	/-- `wmSrc τ q`: `τ` applies in the state `q`. -/
97	\| src : wideRel 2
98	/-- `wmRead τ a`: `τ` applies when reading the symbol `a`. -/
99	\| read : wideRel 2
100	/-- `wmDst τ q`: `τ` moves to the state `q`. -/
101	\| dst : wideRel 2
102	/-- `wmWrite τ a`: `τ` writes the symbol `a`. -/
103	\| write : wideRel 2
104	/-- `wmInp x a`: the address `{y \| y ≤ x}` initially holds the symbol `a`. -/
105	\| inp : wideRel 2
106	deriving DecidableEq
107
108	/-- The relational vocabulary of wide-machine instances. -/
109	def wide : Language :=
110	⟨fun _ => Empty, wideRel⟩
111
112	instance instIsRelationalWide : wide.IsRelational :=
113	fun _ => (inferInstance : IsEmpty Empty)
114
115	/-- The order on the elements of the instance. -/
116	abbrev wmLe : wide.Relations 2 := .wle
117
118	/-- The transition symbol. -/
119	abbrev wmTr : wide.Relations 1 := .tr
120
121	/-- The start-state symbol. -/
122	abbrev wmStart : wide.Relations 1 := .start
123
124	/-- The accepting-state symbol. -/
125	abbrev wmAcc : wide.Relations 1 := .acc
126
127	/-- The blank symbol. -/
128	abbrev wmBlank : wide.Relations 1 := .blank
129
130	/-- The move-right symbol. -/
131	abbrev wmRight : wide.Relations 1 := .right
132
133	/-- The transition-source symbol. -/
134	abbrev wmSrc : wide.Relations 2 := .src
135
136	/-- The transition-read symbol. -/
137	abbrev wmRead : wide.Relations 2 := .read
138
139	/-- The transition-destination symbol. -/
140	abbrev wmDst : wide.Relations 2 := .dst
141
142	/-- The transition-write symbol. -/
143	abbrev wmWrite : wide.Relations 2 := .write
144
145	/-- The input symbol. -/
146	abbrev wmInp : wide.Relations 2 := .inp
147
148	open FirstOrder
149
150	open Language Structure
151
152	section Shorthands
153
154	variable {A : Type} [wide.Structure A]
155
156	/-- The order on the elements of the instance. -/
157	def WMLe (a b : A) : Prop := RelMap wmLe ![a, b]
158
159	/-- Being a transition. -/
160	def WMTr (a : A) : Prop := RelMap wmTr ![a]
161
162	/-- Being a start state. -/
163	def WMStart (a : A) : Prop := RelMap wmStart ![a]
164
165	/-- Being an accepting state. -/
166	def WMAcc (a : A) : Prop := RelMap wmAcc ![a]
167
168	/-- Being the blank symbol. -/
169	def WMBlank (a : A) : Prop := RelMap wmBlank ![a]
170
171	/-- Moving the head right. -/
172	def WMRight (a : A) : Prop := RelMap wmRight ![a]
173
174	/-- The state a transition applies in. -/
175	def WMSrc (a b : A) : Prop := RelMap wmSrc ![a, b]
176
177	/-- The symbol a transition reads. -/
178	def WMRead (a b : A) : Prop := RelMap wmRead ![a, b]
179
180	/-- The state a transition moves to. -/
181	def WMDst (a b : A) : Prop := RelMap wmDst ![a, b]
182
183	/-- The symbol a transition writes. -/
184	def WMWrite (a b : A) : Prop := RelMap wmWrite ![a, b]
185
186	/-- The input at an initial-segment address. -/
187	def WMInp (a b : A) : Prop := RelMap wmInp ![a, b]
188
189	end Shorthands
190
191	section Machine
192
193	variable (A : Type)
194
195	/-- The universe of a wide machine: the addresses – the subsets of the
196	instance, which are its tape cells and its time steps – together with the
197	elements of the instance, which are its control. An `abbrev`, so that the sum
198	structure stays visible to `rw` and to the elaborator. -/
199	abbrev WPoint : Type := (A → Prop) ⊕ A
200
201	variable {A} [wide.Structure A]
202
203	/-- Being a position: the addresses are the positions, the control elements are
204	not. -/
205	def wpPosn : WPoint A → Prop
206	\| Sum.inl _ => True
207	\| Sum.inr _ => False
208
209	/-- The order on the universe: addresses first, in the binary-number order they
210	inherit from the instance's own order, then the control elements in that same
211	order. -/
212	def wpLe : WPoint A → WPoint A → Prop
213	\| Sum.inl s, Sum.inl t => WMSetLe WMLe s t
214	\| Sum.inl _, Sum.inr _ => True
215	\| Sum.inr _, Sum.inl _ => False
216	\| Sum.inr x, Sum.inr y => WMLe x y
217
218	/-- A mark of the control, read on the universe of the machine: no address
219	carries it. -/
220	def wpMark (R : A → Prop) : WPoint A → Prop
221	\| Sum.inl _ => False
222	\| Sum.inr x => R x
223
224	/-- A binary attribute of the control, read on the universe of the machine. -/
225	def wpAttr (R : A → A → Prop) : WPoint A → WPoint A → Prop
226	\| Sum.inr x, Sum.inr y => R x y
227	\| _, _ => False
228
229	/-- The initial tape: the address cutting the initial segment of `x` holds the
230	input symbol of `x`. -/
231	def wpInp : WPoint A → WPoint A → Prop
232	\| Sum.inl s, Sum.inr y => ∃ x, WMDown WMLe s x ∧ WMInp x y
233	\| _, _ => False
234
235	variable (A) in
236	/-- The wide machine an instance describes: the control read off the
237	instance, the positions being the addresses. -/
238	def wideData : TMData (WPoint A) where
239	Posn := wpPosn
240	Le := wpLe
241	Tr := wpMark WMTr
242	Start := wpMark WMStart
243	Acc := wpMark WMAcc
244	Blank := wpMark WMBlank
245	Right := wpMark WMRight
246	Src := wpAttr WMSrc
247	Read := wpAttr WMRead
248	Dst := wpAttr WMDst
249	Write := wpAttr WMWrite
250	Inp := wpInp
251
252	end Machine
253
254	open FirstOrder
255
256	open Language Structure
257
258	section RegCell
259
260	variable {A : Type} [wide.Structure A]
261
262	/-- An element the channel writes for: one that carries an input symbol.
263	These are the elements the file has registers for. -/
264	def WMHasInp (x : A) : Prop := ∃ a : A, WMInp x a
265
266	/-- Being the cell of an element at the register channel, as the model reads
267	it off an address. -/
268	def WMRegSeg (s : A → Prop) (x : A) : Prop := ∀ y, s y ↔ (WMLe y x ∧ WMHasInp y)
269
270	end RegCell
271
272	open Lax904597.Problems Lax485149.Problems
273
274	/-- Wide acceptance: the wide machine of the instance is well formed and
275	accepts within its `2 ^ n` steps. -/
276	def WideAccept : DecisionProblem wide :=
277	DecisionProblem.ofPred fun A _ => TMData.WellFormed (wideData A) ∧ TMData.Accepts (wideData A)
278
279	/-- Wide acceptance in space: the wide machine of the instance is well formed
280	and accepts within its `2 ^ n` cells. -/
281	def WideAcceptSpace : DecisionProblem wide :=
282	DecisionProblem.ofPred fun A _ =>
283	TMData.WellFormed (wideData A) ∧ Lax134656.SpaceBoundedMachines.TMData.AcceptsSpace (wideData A)
284
285	/-- Deterministic wide acceptance in space: the wide machine is moreover
286	deterministic. -/
287	def DWideAcceptSpace : DecisionProblem wide :=
288	DecisionProblem.ofPred fun A _ =>
289	TMData.WellFormed (wideData A) ∧ Lax535992.DeterministicMachines.TMData.Deterministic (wideData A) ∧
290	Lax134656.SpaceBoundedMachines.TMData.AcceptsSpace (wideData A)
291
292	end Lax822549.WideMachines
293

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Wide machines

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments