The halting problem on machines of the NP core

Lax624099.Halting · concepts/Lax624099/Halting.lean · lax-624099

definition

Loading review…

Natural Language Statement

Definition

The halting problem reads the machine data of the NP core, a finite structure describing a nondeterministic Turing machine with its input and its positions, without any bound. The tape is an unbounded strip of pages, each a copy of the positions, so that a cell is a page number and a position, and every cell has a next one; a configuration is a state, the cell under the head and the symbol in every cell; the machine accepts when some run from an initial configuration, with the input on page zero and blanks elsewhere, reaches an accepting state in any number of steps. A machine instance is a yes-instance of HALT when it is well-formed and accepts its input in this unbounded sense; HALT is the decision problem of the structures isomorphic to such an instance.

Concept map

4 concepts; 18 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 Lax904597.Machines
8	import Lax904597.Problems
9	import Lax624099.Problems
10
11	/-!
12	---
13	title: The halting problem on machines of the NP core
14	type: definition
15	---
16	The halting problem reads the machine data of the NP core, a finite
17	structure describing a nondeterministic Turing machine with its input and
18	its positions, without any bound. The tape is an unbounded strip of pages,
19	each a copy of the positions, so that a cell is a page number and a
20	position, and every cell has a next one; a configuration is a state, the cell
21	under the head and the symbol in every cell; the machine accepts when some
22	run from an initial configuration, with the input on page zero and blanks
23	elsewhere, reaches an accepting state in any number of steps. A machine
24	instance is a yes-instance of HALT when it is well-formed and accepts its
25	input in this unbounded sense; HALT is the decision problem of the
26	structures isomorphic to such an instance.
27	-/
28
29	namespace Lax624099.Halting
30
31	open FirstOrder FirstOrder.Language
32	open Lax904597.Problems Lax904597.Machines Lax624099.Problems
33
34	section Ripple
35
36	variable {A : Type} [Finite A] {Le : A → A → Prop} {Posn : A → Prop}
37
38	/-- `p` is a highest position. -/
39	def MaxPos (Le : A → A → Prop) (Posn : A → Prop) (p : A) : Prop :=
40	Posn p ∧ ∀ q, Posn q → Le q p
41
42	end Ripple
43
44	/-- A configuration of a machine on an unbounded tape: the current state, the
45	cell the head is on, and the contents of every cell. A cell is a pair of a
46	page – an integer – and a position of the instance. -/
47	@[ext]
48	structure ConfigU (A : Type) where
49	/-- The current state. -/
50	state : A
51	/-- The cell the head is on. -/
52	head : ℤ × A
53	/-- The symbol in each cell. -/
54	tape : ℤ × A → A
55
56	namespace TMData
57
58	variable {A : Type} (M : TMData A)
59
60	/-- The next cell: one step along the order of the positions inside a page,
61	or the step from the last position of a page to the first position of the next
62	page. Since the pages are indexed by `ℤ`, every cell has a next one and a
63	previous one, on a well-formed machine with at least one position. -/
64	def SuccCell (c c' : ℤ × A) : Prop :=
65	(c'.1 = c.1 ∧ SuccPos M.Le M.Posn c.2 c'.2) ∨
66	(c'.1 = c.1 + 1 ∧ MaxPos M.Le M.Posn c.2 ∧ MinPos M.Le M.Posn c'.2)
67
68	/-- Being an initial configuration on an unbounded tape: a start state, the
69	head on the lowest position of page `0`, the input on page `0` and blanks
70	everywhere else. -/
71	def IsInitU (c : ConfigU A) : Prop :=
72	M.Start c.state ∧ c.head.1 = 0 ∧ MinPos M.Le M.Posn c.head.2 ∧
73	∀ z p, M.Posn p →
74	(z = 0 → M.InitTape p (c.tape (z, p))) ∧ (z ≠ 0 → M.Blank (c.tape (z, p)))
75
76	/-- One step on an unbounded tape: the clauses of
77	`DescriptiveComplexity.TMData.Step`, with `DescriptiveComplexity.TMData.SuccCell`
78	in place of `DescriptiveComplexity.SuccPos` for the move. -/
79	def StepU (c c' : ConfigU A) : Prop :=
80	∃ τ, M.Tr τ ∧ M.Src τ c.state ∧ M.Read τ (c.tape c.head) ∧
81	M.Dst τ c'.state ∧ M.Write τ (c'.tape c.head) ∧
82	(∀ x, x ≠ c.head → c'.tape x = c.tape x) ∧
83	((M.Right τ ∧ SuccCell M c.head c'.head) ∨
84	(¬ M.Right τ ∧ SuccCell M c'.head c.head))
85
86	/-- Reaching one configuration from another in exactly `n` steps. -/
87	def StepsInU : ℕ → ConfigU A → ConfigU A → Prop
88	\| 0, c, c' => c = c'
89	\| n + 1, c, c' => ∃ d, StepU M c d ∧ StepsInU n d c'
90
91	/-- Acceptance on an unbounded tape: some run from an initial configuration
92	reaches an accepting state, in any number of steps whatever.
93
94	This is `DescriptiveComplexity.TMData.Accepts` with the step bound dropped and
95	`DescriptiveComplexity.TMData.AcceptsSpace` with the space bound dropped: the
96	same `∃ n`, with nothing bounding it and nothing bounding the tape. A run is
97	still a finite object, so acceptance is an unbounded search over finite
98	witnesses – the shape of `∃SO[new]`, and the reason the halting problem is in
99	RE and in nothing smaller. -/
100	def AcceptsU : Prop :=
101	∃ (c₀ c : ConfigU A) (n : ℕ), IsInitU M c₀ ∧ StepsInU M n c₀ c ∧ M.Acc c.state
102
103	end TMData
104
105	/-- The machine described by the instance is well-formed and accepts its
106	input on an unbounded tape. -/
107	def HaltsOn (A : Type) [turing.Structure A] : Prop :=
108	(tmData A).WellFormed ∧ TMData.AcceptsU (tmData A)
109
110	/-- HALT: does the machine described by the instance accept its input, in any
111	number of steps and with as much tape as it likes? -/
112	def HALT : DecisionProblem turing :=
113	DecisionProblem.ofPred HaltsOn
114
115	end Lax624099.Halting
116

Discussion

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

Loading discussion…

Lax Lean Archive

The halting problem on machines of the NP core

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments