The number written by a deterministic Turing machine

Lax366625.MachineNumbers · concepts/Lax366625/MachineNumbers.lean · lax-366625

definition

Loading review…

Natural Language Statement

Definition

An instance is a machine instance of the NP core, extended by two marks: the output cells of the tape, and the symbols read as the digit $1$ . The output cells are ordered by the order of the tape, and the rank of an output cell is the number of output cells before it. If the instance describes a well-formed deterministic machine, the number it writes is $\sum 2^{r(p)}$ over the output cells $p$ holding a symbol read as $1$ in the configuration where the machine halts in an accepting state, $r(p)$ being the rank of $p$ ; otherwise it is $0$ . The machine halts in a configuration when that configuration is reached from an initial one within the bound of the instance and no step leaves it.

Concept map

8 concepts; 13 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.Algebra.BigOperators.Finprod
2	import Mathlib.Data.Set.Finite.Lemmas
3	import Mathlib.Data.Fintype.EquivFin
4	import Mathlib.Data.Set.Card
5	import Mathlib.SetTheory.Cardinal.Finite
6	import Mathlib.Logic.Equiv.Prod
7	import Mathlib.ModelTheory.Syntax
8	import Mathlib.ModelTheory.Semantics
9	import Mathlib.Order.PiLex
10	import Mathlib.Data.Prod.Lex
11	import Mathlib.ModelTheory.Order
12	import Mathlib.ModelTheory.Complexity
13	import Mathlib.Tactic.FinCases
14	import Mathlib.Logic.Equiv.Fin.Basic
15	import Mathlib.Data.Finite.Sigma
16	import Mathlib.Data.Fintype.Lattice
17	import Mathlib.Order.Lattice.Nat
18	import Mathlib.Data.Fintype.Pigeonhole
19	import Mathlib.Dynamics.FixedPoints.Basic
20	import Lax904597.Machines
21	import Lax535992.DeterministicMachines
22	import Lax366625.CountingProblems
23
24	/-!
25	---
26	title: The number written by a deterministic Turing machine
27	type: definition
28	---
29	An instance is a machine instance of the NP core, extended by two marks: the
30	output cells of the tape, and the symbols read as the digit $1$ . The output
31	cells are ordered by the order of the tape, and the rank of an output cell
32	is the number of output cells before it. If the instance describes a
33	well-formed deterministic machine, the number it writes is
34	$\sum 2^{r(p)}$ over the output cells $p$ holding a symbol read as $1$ in
35	the configuration where the machine halts in an accepting state, $r(p)$
36	being the rank of $p$ ; otherwise it is $0$ . The machine halts in a
37	configuration when that configuration is reached from an initial one within
38	the bound of the instance and no step leaves it.
39	-/
40
41	namespace Lax366625.MachineNumbers
42
43	open Lax904597.Machines
44
45	section Ripple
46
47	variable {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop}
48
49	/-- `p` is a highest position. -/
50	def MaxPos (Le : A → A → Prop) (Posn : A → Prop) (p : A) : Prop :=
51	Posn p ∧ ∀ q, Posn q → Le q p
52
53	end Ripple
54
55	open FirstOrder
56
57	open FirstOrder.Language
58
59	/-- The relation symbols of the language. -/
60	inductive tapeOutRel : ℕ → Type where
61	/-- `out p`: the cell `p` is an output cell, holding one digit. -/
62	\| out : tapeOutRel 1
63	/-- `one a`: the symbol `a` is read as the digit `1`. -/
64	\| one : tapeOutRel 1
65	deriving DecidableEq
66
67	/-- The symbols reading a number off the tape of a machine. -/
68	def tapeOut : FirstOrder.Language :=
69	⟨fun _ => Empty, tapeOutRel⟩
70
71	instance instIsRelationalTapeOut : FirstOrder.Language.IsRelational tapeOut := fun _ =>
72	(inferInstance : IsEmpty Empty)
73
74	/-- `out p`: the cell `p` is an output cell, holding one digit. -/
75	abbrev tpOut : tapeOut.Relations 1 :=
76	.out
77
78	/-- `one a`: the symbol `a` is read as the digit `1`. -/
79	abbrev tpOne : tapeOut.Relations 1 :=
80	.one
81
82	/-- The relational language of machines writing a number. -/
83	abbrev turingOut : Language.{0, 0} := turing.sum tapeOut
84
85	open FirstOrder
86
87	open Language Structure
88
89	namespace TMData
90
91	variable {A : Type} (M : TMData A)
92
93	/-- The machine halts in the configuration `c`: `c` is reached from an
94	initial configuration within the clock, and no step is possible from it. -/
95	def Halts (c : Config A) : Prop :=
96	∃ (c₀ : Config A) (n : ℕ), M.IsInit c₀ ∧ n < Nat.card {p : A // M.Posn p} ∧
97	M.StepsIn n c₀ c ∧ ∀ e, ¬M.Step c e
98
99	end TMData
100
101	/-- “Is an output cell”, in the vocabulary of machines writing a number. -/
102	abbrev mnOut : turingOut.Relations 1 := Sum.inr tpOut
103
104	/-- “Is read as the digit `1`”, in the vocabulary of machines writing a
105	number. -/
106	abbrev mnOne : turingOut.Relations 1 := Sum.inr tpOne
107
108	/-- The order of the tape, in the vocabulary of machines writing a number. -/
109	abbrev mnLe : turingOut.Relations 2 := Sum.inl tmLe
110
111	/-- A machine writing a number is a machine. -/
112	instance turingOutStructure (A : Type) [turingOut.Structure A] :
113	turing.Structure A :=
114	(LHom.sumInl : turing →ᴸ turingOut).reduct A
115
116	section Semantics
117
118	variable {A : Type} [turingOut.Structure A]
119
120	/-- The output cell `p` holds the digit `1` when the machine halts, in an
121	accepting state. -/
122	def OutDigit (p : A) : Prop :=
123	RelMap mnOut ![p] ∧ ∃ c : Config A, TMData.Halts (tmData A) c ∧ (tmData A).Acc c.state ∧
124	RelMap mnOne ![c.tape p]
125
126	/-- `q` is an output cell strictly before `p` on the tape. -/
127	def LowerCell (p q : A) : Prop :=
128	RelMap mnOut ![q] ∧ q ≠ p ∧ RelMap mnLe ![q, p]
129
130	/-- The rank of a cell among the output cells: the number of output cells
131	strictly before it on the tape. -/
132	noncomputable def cellRank (p : A) : ℕ :=
133	Nat.card {q : A // LowerCell p q}
134
135	variable (A) in
136	open Classical in
137	/-- The number written by a machine: each output cell holding the digit
138	`1` when the machine halts and accepts contributes two to the power of its
139	rank among the output cells. Instances that are not well-formed deterministic
140	machines write `0`. -/
141	noncomputable def machineNumber : ℕ :=
142	if (tmData A).WellFormed ∧ Lax535992.DeterministicMachines.TMData.Deterministic (tmData A) then
143	∑ᶠ p : A, if OutDigit p then 2 ^ cellRank p else 0
144	else 0
145
146	end Semantics
147
148	open Lax366625.CountingProblems
149
150	/-- The number written by a deterministic machine, as a counting problem. -/
151	noncomputable def DTMNumber : CountingProblem turingOut :=
152	CountingProblem.ofFun fun A _ => machineNumber A
153
154	end Lax366625.MachineNumbers
155

Builds on

Used by

From Mathlib

Discussion

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

Loading discussion…

Lax Lean Archive

The number written by a deterministic Turing machine

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments