Acceptance by alternating Turing machines with a bounded number of alternations

Lax564036.AlternatingMachines · concepts/Lax564036/AlternatingMachines.lean · lax-564036

definition

Loading review…

Natural Language Statement

Definition

An alternating machine instance with $k$ blocks is a machine instance of the NP core, a finite structure describing a Turing machine with its input and a linear order of positions bounding tape and time, together with $k$ unary marks splitting the states into blocks. The blocks alternate in polarity, the first being existential or universal, and a state is universal when its block is. The block structure is well formed when every state lies in exactly one block, every transition stays in its block or moves to the next one, and the start states lie in the first block; a run then alternates at most $k - 1$ times.

A configuration accepts within a budget of steps when its state is accepting, or it is existential and some successor accepts within the remaining budget, or it is universal, has a successor, and every successor accepts within the remaining budget. The machine accepts when the initial configurations accept within as many steps as there are positions, some of them if the first block is existential, all of them and at least one if it is universal. An instance is a yes-instance of alternating machine acceptance with $k$ blocks when the machine and its blocks are well formed and it accepts; the problem is the decision problem of the structures isomorphic to such an instance.

Concept map

4 concepts; 16 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Lean source view on GitHub

Show types on hover

1	import Mathlib.ModelTheory.Semantics
2	import Mathlib.SetTheory.Cardinal.Finite
3	import Lax904597.Problems
4	import Lax485149.Problems
5	import Lax904597.Machines
6
7	/-!
8	---
9	title: Acceptance by alternating Turing machines with a bounded number of alternations
10	type: definition
11	---
12	An alternating machine instance with $k$ blocks is a machine instance of
13	the NP core, a finite structure describing a Turing machine with its input
14	and a linear order of positions bounding tape and time, together with $k$
15	unary marks splitting the states into blocks. The blocks alternate in
16	polarity, the first being existential or universal, and a state is
17	universal when its block is. The block structure is well formed when every
18	state lies in exactly one block, every transition stays in its block or
19	moves to the next one, and the start states lie in the first block; a run
20	then alternates at most $k - 1$ times.
21
22	A configuration accepts within a budget of steps when its state is
23	accepting, or it is existential and some successor accepts within the
24	remaining budget, or it is universal, has a successor, and every successor
25	accepts within the remaining budget. The machine accepts when the initial
26	configurations accept within as many steps as there are positions, some of
27	them if the first block is existential, all of them and at least one if it
28	is universal. An instance is a yes-instance of alternating machine
29	acceptance with $k$ blocks when the machine and its blocks are well formed
30	and it accepts; the problem is the decision problem of the structures
31	isomorphic to such an instance.
32	-/
33
34	namespace Lax564036.AlternatingMachines
35
36	open Lax904597.Problems Lax485149.Problems
37
38	open Lax904597.Machines
39
40	/-- An alternating Turing machine presented as relations on a universe: a
41	machine in the sense of `TMData`, together with marks
42	splitting its states into quantifier blocks. -/
43	structure ATMData (A : Type) extends TMData A where
44	/-- `Blk j q`: the state `q` belongs to the `j`-th quantifier block. -/
45	Blk : ℕ → A → Prop
46
47	/-- The polarity of the `j`-th quantifier block of a prefix starting with
48	polarity `start`: `true` for an existential block, `false` for a universal one.
49	The polarities alternate, so the parity of `j` decides. -/
50	def blockPol (start : Bool) (j : ℕ) : Bool :=
51	if j % 2 = 0 then start else !start
52
53	/-- Quantification with a polarity, guarded. Existentially, the guard is
54	conjoined; universally it is assumed – and required to be satisfiable by
55	something: a universal player with no legal move loses rather than winning
56	vacuously. -/
57	def guardQ (pol : Bool) {α : Type} (C P : α → Prop) : Prop :=
58	match pol with
59	\| true => ∃ a, C a ∧ P a
60	\| false => (∃ a, C a) ∧ ∀ a, C a → P a
61
62	namespace ATMData
63
64	variable {A : Type} (M : ATMData A)
65
66	/-- The state `q` is universal: it carries the mark of a block whose
67	polarity is universal, so the moves out of it belong to the universal
68	player. -/
69	def IsUniv (start : Bool) (q : A) : Prop := ∃ j, M.Blk j q ∧ blockPol start j = false
70
71	/-- Alternating acceptance within a budget. `M.AltAcc start n c` says the
72	configuration `c` accepts with `n` steps to spare: an accepting state accepts
73	outright, an existential configuration accepts when some successor does, and
74	a universal one when it has a successor and every successor accepts. -/
75	def AltAcc (start : Bool) : ℕ → Config A → Prop
76	\| 0, c => M.Acc c.state
77	\| n + 1, c => M.Acc c.state ∨
78	(M.IsUniv start c.state ∧ (∃ c', M.Step c c') ∧
79	∀ c', M.Step c c' → AltAcc start n c') ∨
80	(¬ M.IsUniv start c.state ∧ ∃ c', M.Step c c' ∧ AltAcc start n c')
81
82	/-- Alternating acceptance: an initial configuration accepts within as many
83	steps as there are positions – chosen by the player of block `0`, which is what
84	`guardQ` at the polarity `start` says: the residual freedom in the initial
85	configuration belongs to the same player as the first move. -/
86	def AltAccepts (start : Bool) : Prop :=
87	guardQ start (fun c₀ : Config A => M.IsInit c₀)
88	(fun c₀ => M.AltAcc start (Nat.card {p : A // M.Posn p} - 1) c₀)
89
90	/-- The block structure is well formed: every state carries exactly one of
91	the `k` block marks, every transition either stays in its block or moves to
92	the next one, and the run starts in block `0`. The second clause is what bounds
93	the number of alternations by `k - 1`. -/
94	def BlocksWellFormed (k : ℕ) : Prop :=
95	(∀ q, ∃ j, j < k ∧ M.Blk j q ∧ ∀ j', M.Blk j' q → j' = j) ∧
96	(∀ τ q q' j j', M.Tr τ → M.Src τ q → M.Dst τ q' → M.Blk j q → M.Blk j' q' →
97	j ≤ j' ∧ j' ≤ j + 1) ∧
98	∀ q, M.Start q → M.Blk 0 q
99
100	end ATMData
101
102	open FirstOrder
103
104	open FirstOrder.Language
105
106	/-- Relation symbols of alternating machine instances: those of machine
107	instances, and one unary mark per quantifier block. -/
108	inductive turingAltRel (k : ℕ) : ℕ → Type
109	/-- A symbol of the underlying machine vocabulary. -/
110	\| base {n : ℕ} : turingRel n → turingAltRel k n
111	/-- `blk i q`: the state `q` belongs to the `i`-th quantifier block. -/
112	\| blk : Fin k → turingAltRel k 1
113
114	/-- The relational vocabulary of alternating machine instances with `k`
115	quantifier blocks. -/
116	def turingAlt (k : ℕ) : Language :=
117	⟨fun _ => Empty, turingAltRel k⟩
118
119	instance instIsRelationalTuringAlt (k : ℕ) : IsRelational (turingAlt k) :=
120	fun _ => ⟨fun f => Empty.elim f⟩
121
122	variable {k : ℕ}
123
124	/-- The position symbol. -/
125	abbrev atmPosn : (turingAlt k).Relations 1 := .base .posn
126
127	/-- The transition symbol. -/
128	abbrev atmTr : (turingAlt k).Relations 1 := .base .tr
129
130	/-- The start-state symbol. -/
131	abbrev atmStart : (turingAlt k).Relations 1 := .base .start
132
133	/-- The accepting-state symbol. -/
134	abbrev atmAcc : (turingAlt k).Relations 1 := .base .acc
135
136	/-- The blank symbol. -/
137	abbrev atmBlank : (turingAlt k).Relations 1 := .base .blank
138
139	/-- The move-right symbol. -/
140	abbrev atmRight : (turingAlt k).Relations 1 := .base .right
141
142	/-- The order symbol. -/
143	abbrev atmLe : (turingAlt k).Relations 2 := .base .le
144
145	/-- The transition-source symbol. -/
146	abbrev atmSrc : (turingAlt k).Relations 2 := .base .tsrc
147
148	/-- The transition-read symbol. -/
149	abbrev atmRead : (turingAlt k).Relations 2 := .base .tread
150
151	/-- The transition-destination symbol. -/
152	abbrev atmDst : (turingAlt k).Relations 2 := .base .tdst
153
154	/-- The transition-write symbol. -/
155	abbrev atmWrite : (turingAlt k).Relations 2 := .base .twrite
156
157	/-- The input symbol. -/
158	abbrev atmInp : (turingAlt k).Relations 2 := .base .inp
159
160	/-- The mark of the `i`-th quantifier block. -/
161	abbrev atmBlk (i : Fin k) : (turingAlt k).Relations 1 := .blk i
162
163	open FirstOrder
164
165	open Language Structure
166
167	section Shorthands
168
169	variable {k : ℕ} {A : Type} [(turingAlt k).Structure A]
170
171	/-- Being a position. -/
172	def ATMPosn (a : A) : Prop := RelMap (atmPosn (k := k)) ![a]
173
174	/-- Being a transition. -/
175	def ATMTr (a : A) : Prop := RelMap (atmTr (k := k)) ![a]
176
177	/-- Being a start state. -/
178	def ATMStart (a : A) : Prop := RelMap (atmStart (k := k)) ![a]
179
180	/-- Being an accepting state. -/
181	def ATMAcc (a : A) : Prop := RelMap (atmAcc (k := k)) ![a]
182
183	/-- Being the blank symbol. -/
184	def ATMBlank (a : A) : Prop := RelMap (atmBlank (k := k)) ![a]
185
186	/-- Moving the head right. -/
187	def ATMRight (a : A) : Prop := RelMap (atmRight (k := k)) ![a]
188
189	/-- The order on positions. -/
190	def ATMLe (a b : A) : Prop := RelMap (atmLe (k := k)) ![a, b]
191
192	/-- The state a transition applies in. -/
193	def ATMSrc (a b : A) : Prop := RelMap (atmSrc (k := k)) ![a, b]
194
195	/-- The symbol a transition reads. -/
196	def ATMRead (a b : A) : Prop := RelMap (atmRead (k := k)) ![a, b]
197
198	/-- The state a transition moves to. -/
199	def ATMDst (a b : A) : Prop := RelMap (atmDst (k := k)) ![a, b]
200
201	/-- The symbol a transition writes. -/
202	def ATMWrite (a b : A) : Prop := RelMap (atmWrite (k := k)) ![a, b]
203
204	/-- The initial contents of a cell. -/
205	def ATMInp (a b : A) : Prop := RelMap (atmInp (k := k)) ![a, b]
206
207	/-- The block of a state, read off the marks: the marks of the vocabulary are
208	indexed by `Fin k`, so a block index beyond `k` marks nothing. -/
209	def ATMBlk (j : ℕ) (a : A) : Prop := ∃ h : j < k, RelMap (atmBlk (⟨j, h⟩ : Fin k)) ![a]
210
211	/-- The alternating machine an instance describes. -/
212	def atmData (k : ℕ) (A : Type) [(turingAlt k).Structure A] : ATMData A where
213	Posn := ATMPosn (k := k)
214	Le := ATMLe (k := k)
215	Tr := ATMTr (k := k)
216	Start := ATMStart (k := k)
217	Acc := ATMAcc (k := k)
218	Blank := ATMBlank (k := k)
219	Right := ATMRight (k := k)
220	Src := ATMSrc (k := k)
221	Read := ATMRead (k := k)
222	Dst := ATMDst (k := k)
223	Write := ATMWrite (k := k)
224	Inp := ATMInp (k := k)
225	Blk := ATMBlk (k := k)
226
227	end Shorthands
228
229	/-- The instance describes a well-formed alternating machine, with well-formed
230	blocks, that accepts its input. -/
231	def ATMAccepts (k : ℕ) (start : Bool) (A : Type) [(turingAlt k).Structure A] : Prop :=
232	(atmData k A).toTMData.WellFormed ∧ ATMData.BlocksWellFormed (atmData k A) k ∧
233	ATMData.AltAccepts (atmData k A) start
234
235	/-- Alternating machine acceptance: does the alternating machine described
236	by the instance accept its input within as many steps as there are positions?
237	The first block is existential when `start` is `true`. -/
238	def ATMAccept (k : ℕ) (start : Bool) : DecisionProblem (turingAlt k) :=
239	DecisionProblem.ofPred fun A _ => ATMAccepts k start A
240
241	end Lax564036.AlternatingMachines
242

Discussion

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

Loading discussion…

Lax Lean Archive

Acceptance by alternating Turing machines with a bounded number of alternations

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments