Alternating acceptance on views

A view (Turing.FiniteCfg) of a configuration keeps everything except the input and the output (Turing.MultiTapeNTM.ViewRep), and the views a running view steps to (Turing.MultiTapeNTM.viewSucc) are, for the nondeterministic machine of the table of an alternating machine, the views after its two moves (Turing.MultiTapeATM.mem_viewSucc_iff). Acceptance within n moves therefore transfers to views (Turing.MultiTapeATM.ViewAcceptsWithin, Turing.MultiTapeATM.viewAcceptsWithin_iff), so a machine accepts exactly when its initial view accepts within some number of moves (Turing.MultiTapeATM.accepts_iff_exists_viewAcceptsWithin).

Acceptance (Turing.MultiTapeATM.Accepts) is the least fixed point of the labelling: it asks for acceptance within some finite number of moves, so a configuration whose acceptance would rely on an infinite branch does not accept, as for Chandra, Kozen and Stockmeyer Chandra, Kozen and Stockmeyer. On a list of views closed under successors, the views accepting within n moves grow with n and can grow strictly for at most as many steps as the list has entries; once they stop growing they never grow again. So a view of the list that accepts within some number of moves accepts within as many moves as the list has entries (Turing.MultiTapeATM.viewAcceptsWithin_length). This finite stabilization is what lets a bounded number of rounds of marking compute the least fixed point exactly.

Main definitions

• Turing.MultiTapeATM.ViewAcceptsWithin: acceptance of a view within a number of moves.

Main results

• Turing.MultiTapeATM.tr_toNTM_iff_action: the transitions of the nondeterministic machine of the table are the actions of the two moves.
• Turing.MultiTapeATM.mem_viewSucc_iff: the successors of a running view are its views after the two moves.
• Turing.MultiTapeATM.viewAcceptsWithin_iff: views accept within n moves as the configurations they represent do.
• Turing.MultiTapeATM.accepts_iff_exists_viewAcceptsWithin: acceptance through views.
• Turing.MultiTapeATM.viewAcceptsWithin_length: on a closed list of views, acceptance within some number of moves is acceptance within as many moves as the list has entries.

References

• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation

theorem Turing.MultiTapeATM.tr_toNTM_iff_action {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {q : State} {symbol : Option Bool} {work : Fin k → Option Bool} {act : Action k Bool State} : atm.toPTM.toNTM.Tr q symbol work act ↔ ∃ (b : Bool), act = atm.action q symbol work b

The transitions of the nondeterministic machine of the table are the actions of the two moves.

def Turing.MultiTapeATM.ViewAcceptsWithin {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) [Finite State] : ℕ → FiniteCfg k Bool State → Prop

Acceptance of a view within n moves, as for configurations (Turing.MultiTapeATM.AcceptsWithin): within 0 moves a halted view with output [true], and within n + 1 moves a halted view with output [true] or a running view one (existential state) or all (universal state) of whose successors accept within n moves.

theorem Turing.MultiTapeATM.mem_viewSucc_iff {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {v w : FiniteCfg k Bool State} {q : State} (hq : v.state = some q) : w ∈ atm.toPTM.toNTM.viewSucc v ↔ ∃ (b : Bool), w = (v.step (atm.action q v.inputSymbol v.workTapeSymbols b)).summarizeOutput

The successors of a running view are its views after the two moves.

theorem Turing.MultiTapeATM.viewSucc_ne_nil {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {v : FiniteCfg k Bool State} {q : State} (hq : v.state = some q) : atm.toPTM.toNTM.viewSucc v ≠ []

A running view has a successor.

theorem Turing.MultiTapeATM.viewAcceptsWithin_zero_iff {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {v : FiniteCfg k Bool State} : atm.ViewAcceptsWithin 0 v ↔ v.state = none ∧ v.output = [true]

Within 0 moves, only a halted view with output [true] accepts.

theorem Turing.MultiTapeATM.viewAcceptsWithin_of_halted {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {n : ℕ} {v : FiniteCfg k Bool State} (h : v.state = none) : atm.ViewAcceptsWithin n v ↔ v.output = [true]

A halted view accepts exactly when its output is [true].

theorem Turing.MultiTapeATM.viewAcceptsWithin_succ_of_universal {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {n : ℕ} {v : FiniteCfg k Bool State} {q : State} (h : v.state = some q) (hq : atm.universal q = true) : atm.ViewAcceptsWithin (n + 1) v ↔ ∀ w ∈ atm.toPTM.toNTM.viewSucc v, atm.ViewAcceptsWithin n w

A universal view accepts within n + 1 moves when all its successors accept within n.

theorem Turing.MultiTapeATM.viewAcceptsWithin_succ_of_existential {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {n : ℕ} {v : FiniteCfg k Bool State} {q : State} (h : v.state = some q) (hq : atm.universal q = false) : atm.ViewAcceptsWithin (n + 1) v ↔ ∃ w ∈ atm.toPTM.toNTM.viewSucc v, atm.ViewAcceptsWithin n w

An existential view accepts within n + 1 moves when one of its successors accepts within n.

theorem Turing.MultiTapeATM.not_viewAcceptsWithin_zero {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {v : FiniteCfg k Bool State} {q : State} (h : v.state = some q) : ¬atm.ViewAcceptsWithin 0 v

A running view does not accept within 0 moves.

theorem Turing.MultiTapeATM.viewAcceptsWithin_iff {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {input : List Bool} {n : ℕ} {v : FiniteCfg k Bool State} {c : Cfg k Bool State input} (h : MultiTapeNTM.ViewRep v c) : atm.ViewAcceptsWithin n v ↔ atm.AcceptsWithin n c

Views accept as the configurations they represent do.

theorem Turing.MultiTapeATM.accepts_iff_exists_viewAcceptsWithin {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {input : List Bool} : atm.Accepts input ↔ ∃ (n : ℕ), atm.ViewAcceptsWithin n (atm.toPTM.toNTM.initView input)

Acceptance through views: the machine accepts exactly when its initial view accepts within some number of moves.

theorem Turing.MultiTapeATM.ViewAcceptsWithin.mono {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {n n' : ℕ} {v : FiniteCfg k Bool State} (h : atm.ViewAcceptsWithin n v) (hn : n ≤ n') : atm.ViewAcceptsWithin n' v

Acceptance within n moves is acceptance within more.

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

On a list of views closed under successors, acceptance within n + 1 moves depends only on acceptance within n moves on the list.

theorem Turing.MultiTapeATM.viewAcceptsWithin_length {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} [Finite State] {found : List (FiniteCfg k Bool State)} (hclosed : ∀ v ∈ found, ∀ w ∈ atm.toPTM.toNTM.viewSucc v, w ∈ found) {v : FiniteCfg k Bool State} (hv : v ∈ found) {n : ℕ} (h : atm.ViewAcceptsWithin n v) : atm.ViewAcceptsWithin found.length v

Stabilization. On a list of views closed under successors, a view of the list accepting within some number of moves accepts within as many moves as the list has entries.