Space-bounded alternating acceptance by marking

The configuration graph of a space-bounded alternating machine is evaluated bottom-up Chandra, Kozen and Stockmeyer, Section 3 Sipser, Section 10.3. Starting from no views, a round of marking (Turing.MultiTapeATM.markStep) keeps the views of a list that are halted with output [true], or running with one (existential state) or all (universal state) of their successors already marked (Turing.MultiTapeATM.markGood). On a list closed under successors, i + 1 rounds mark exactly the views of the list that accept within i moves (Turing.MultiTapeATM.mem_markStep_iterate_iff).

Acceptance (Turing.MultiTapeATM.Accepts) is the least fixed point of the labelling, acceptance within some finite number of moves, so an infinite branch never helps a configuration accept. The marking computes exactly this least fixed point. Each round adds the views accepting within one more move, and by stabilization on the finite list (Turing.MultiTapeATM.viewAcceptsWithin_length) a view accepting within some number of moves accepts within as many moves as the list has entries. So after that many rounds plus one, the marked views are those accepting within some number of moves (Turing.MultiTapeATM.markAccepts_iff). A view whose acceptance would rely on an infinite branch is never marked, because the marking only ever adds views witnessed by finitely many moves.

The views are found by truncated breadth-first search (Turing.MultiTapeNTM.boundedSearch). Once N bounds the number of reachable views, the search of N rounds finds them all, and marking them decides acceptance (Turing.MultiTapeATM.boundedAccepts_iff). When the space bound is polynomial in the instance, N lists of at most N + 1 views of polynomial size are processed, so the decision is polynomial-time in the instance and the unary N (Turing.MultiTapeATM.computableInPolyTime_boundedAccepts).

Main definitions

• Turing.MultiTapeATM.markGood, Turing.MultiTapeATM.markStep: a round of marking.
• Turing.MultiTapeATM.markAccepts: whether a view is marked after enough rounds.
• Turing.MultiTapeATM.boundedAccepts: marking the views found by truncated breadth-first search.

Main results

• Turing.MultiTapeATM.mem_markStep_iterate_iff: i + 1 rounds mark the views accepting within i moves.
• Turing.MultiTapeATM.markAccepts_iff: marking decides acceptance on a closed list of views.
• Turing.MultiTapeATM.markAccepts_iff_of_mem_iff: marking the reachable views decides acceptance.
• Turing.MultiTapeATM.boundedAccepts_iff: under a space bound, marking the views found by enough rounds of search decides acceptance.
• Turing.MultiTapeATM.computableInPolyTime_markGood: the marking test is polynomial-time.
• Turing.MultiTapeATM.computableInPolyTime_markAccepts: marking is polynomial-time in the found views and the start view.
• Turing.MultiTapeATM.computableInPolyTime_boundedAccepts: under a polynomial space bound, marking is polynomial-time in the instance and the unary number of views.

References

• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation, Section 3
• M. Sipser, Introduction to the Theory of Computation, Section 10.3

Marking

noncomputable def Turing.MultiTapeATM.markGood {k : ℕ} {State : Type} [Finite State] (atm : MultiTapeATM k Bool State) (marked : List (FiniteCfg k Bool State)) (v : FiniteCfg k Bool State) : Bool

Whether a view accepts within one more move, given the list marked of views accepting within the current number of moves: a halted view with output [true], or a running view one of whose successors (existential state) or all of whose successors (universal state) are marked.

noncomputable def Turing.MultiTapeATM.markStep {k : ℕ} {State : Type} [Finite State] (atm : MultiTapeATM k Bool State) (found marked : List (FiniteCfg k Bool State)) : List (FiniteCfg k Bool State)

One round of marking: the views of found accepting within one more move.

noncomputable def Turing.MultiTapeATM.markAccepts {k : ℕ} {State : Type} [Finite State] (atm : MultiTapeATM k Bool State) (found : List (FiniteCfg k Bool State)) (start : FiniteCfg k Bool State) : Bool

Marking acceptance: whether start is marked after as many rounds of marking as found has entries, plus one.

theorem Turing.MultiTapeATM.markGood_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {found marked : List (FiniteCfg k Bool State)} (hclosed : ∀ v ∈ found, ∀ w ∈ atm.toPTM.toNTM.viewSucc v, w ∈ found) {n : ℕ} (hmarked : ∀ w ∈ found, w ∈ marked ↔ atm.ViewAcceptsWithin n w) {v : FiniteCfg k Bool State} (hv : v ∈ found) : atm.markGood marked v = true ↔ atm.ViewAcceptsWithin (n + 1) v

Marking against the views accepting within n moves gives the views accepting within n + 1.

theorem Turing.MultiTapeATM.markGood_nil_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {v : FiniteCfg k Bool State} : atm.markGood [] v = true ↔ atm.ViewAcceptsWithin 0 v

Marking against no views gives the views accepting within 0 moves: a running view has a successor, which is not marked.

theorem Turing.MultiTapeATM.mem_markStep_iterate_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {found : List (FiniteCfg k Bool State)} (hclosed : ∀ v ∈ found, ∀ w ∈ atm.toPTM.toNTM.viewSucc v, w ∈ found) (i : ℕ) {v : FiniteCfg k Bool State} : v ∈ (atm.markStep found)^[i + 1] [] ↔ v ∈ found ∧ atm.ViewAcceptsWithin i v

Marking rounds. On a list of views closed under successors, after i + 1 rounds of marking the marked views are those of the list accepting within i moves.

theorem Turing.MultiTapeATM.markAccepts_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {found : List (FiniteCfg k Bool State)} (hclosed : ∀ v ∈ found, ∀ w ∈ atm.toPTM.toNTM.viewSucc v, w ∈ found) {start : FiniteCfg k Bool State} (hstart : start ∈ found) : atm.markAccepts found start = true ↔ ∃ (n : ℕ), atm.ViewAcceptsWithin n start

Marking computes the least fixed point on a list of views closed under successors containing the start: the start is marked exactly when it accepts within some number of moves.

Marking the reachable views

theorem Turing.MultiTapeATM.markAccepts_iff_of_mem_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {input : List Bool} {found : List (FiniteCfg k Bool State)} (hfound : ∀ (v : FiniteCfg k Bool State), v ∈ found ↔ Relation.ReflTransGen atm.toPTM.toNTM.ViewStep (atm.toPTM.toNTM.initView input) v) : atm.markAccepts found (atm.toPTM.toNTM.initView input) = true ↔ atm.Accepts input

Marking the reachable views decides acceptance: if found lists exactly the views reachable from the initial view, marking it and testing the initial view decides acceptance.

noncomputable def Turing.MultiTapeATM.boundedAccepts {k : ℕ} {State : Type} [Finite State] (atm : MultiTapeATM k Bool State) (input : List Bool) (N : ℕ) : Bool

Space-bounded acceptance by marking: mark the views found by the truncated breadth-first search of N rounds, and test the initial view.

theorem Turing.MultiTapeATM.boundedAccepts_iff {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {input : List Bool} {s N : ℕ} (hs : atm.toPTM.toNTM.RunsInSpace input s) (hN : 2 ^ (2 * MultiTapeNTM.coreLengthBound k State input.length s + 1) ≤ N) : atm.boundedAccepts input N = true ↔ atm.Accepts input

Marking decides acceptance under a space bound, once N bounds the number of reachable views.

Polynomial time

theorem Turing.MultiTapeATM.computableInPolyTime_markGood {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} : MultiTapeTM.ComputableInPolyTime (fun (p : List (FiniteCfg k Bool State) × FiniteCfg k Bool State) => atm.markGood p.1 p.2) (MultiTapeTM.encPair (MultiTapeTM.encList MultiTapeTM.encFiniteCfg) MultiTapeTM.encFiniteCfg) MultiTapeTM.encBool

The marking test is polynomial-time in the marked views and the view.

theorem Turing.MultiTapeATM.computableInPolyTime_markAccepts {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} : MultiTapeTM.ComputableInPolyTime (fun (p : List (FiniteCfg k Bool State) × FiniteCfg k Bool State) => atm.markAccepts p.1 p.2) (MultiTapeTM.encPair (MultiTapeTM.encList MultiTapeTM.encFiniteCfg) MultiTapeTM.encFiniteCfg) MultiTapeTM.encBool

Marking is polynomial-time in the found views and the start view: the marked views are a sublist of the found views, and there are as many rounds of marking as found views, plus one.

theorem Turing.MultiTapeATM.computableInPolyTime_boundedAccepts {k : ℕ} {State : Type} [Finite State] {atm : MultiTapeATM k Bool State} {α : Type} {enc : α ↪ List Bool} {s : α → ℕ} (hs : ∀ (a : α), atm.toPTM.toNTM.RunsInSpace (enc a) (s a)) (hpoly : MultiTapeTM.PolyBounded (fun (a : α) => (enc a).length) s) : MultiTapeTM.ComputableInPolyTime (fun (x : α × ℕ) => atm.boundedAccepts (enc x.1) x.2) (MultiTapeTM.encPair enc MultiTapeTM.encUnary) MultiTapeTM.encBool

Space-bounded acceptance by marking is polynomial-time in the instance and the unary number N of views, when the space bound is polynomial in the instance: the found and marked views are at most N + 1 views of polynomial size, and there are at most N + 2 rounds of marking.