The strict table of an alternating machine

An alternating machine running within t steps plays a game of t moves, each chosen by the player that the state labels. This file makes the order of the players fixed: an existential and a universal move per step. The strict table of a machine (Turing.MultiTapeATM.strict) spends two coins on each step of the machine: it stores the first coin, and on the second takes the step of the machine with the second coin in a universal state and with the first in an existential state. The coin that is not used is a vacuous move.

Replaying a fixed finite fair-coin table is polynomial-time (Turing.MultiTapePTM.computableInPolyTime_runClosedCoins), so the game verifier on the strict table (Turing.MultiTapeATM.gameVerifier) is computable in polynomial time (Turing.MultiTapeATM.computableInPolyTime_gameVerifier).

Main definitions

• Turing.MultiTapeATM.strict: the strict table, two coins per step.
• Turing.MultiTapeATM.gameVerifier: the verifier replaying the strict table on an encoded instance and a move list.

Main results

• Turing.MultiTapeATM.Strict.stepCoins_cfg, Turing.MultiTapeATM.Strict.stepCoins_cfg_of_halted: two coins per step on running configurations, and halted configurations stay unchanged.
• Turing.MultiTapeATM.computableInPolyTime_gameVerifier: replaying the strict table of a finite alternating machine is polynomial-time.

References

• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation
• S. Arora, B. Barak, Computational Complexity: A Modern Approach

The strict table

def Turing.MultiTapeATM.Strict.action {k : ℕ} {Symbol State : Type} (atm : MultiTapeATM k Symbol State) : State × Option Bool → Option Symbol → (Fin k → Option Symbol) → Bool → Action k Symbol (State × Option Bool)

The action of the strict table: in a state (q, none) store the coin; in a state (q, some x) take the step of the machine with the coin y if q is universal and with x otherwise.

def Turing.MultiTapeATM.Strict.cfg {k : ℕ} {Symbol State : Type} {input : List Symbol} (c : Cfg k Symbol State input) (p : Option Bool) : Cfg k Symbol (State × Option Bool) input

A configuration of the machine as one of the strict table, with the stored coin.

def Turing.MultiTapeATM.strict {k : ℕ} {Symbol State : Type} (atm : MultiTapeATM k Symbol State) : MultiTapePTM k Symbol (State × Option Bool)

The strict table of an alternating machine: it spends two coins on each step, storing the first, and takes the step of the machine with the second coin in a universal state and with the first in an existential state.

theorem Turing.MultiTapeATM.Strict.step_strict {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol (State × Option Bool) input} {s : State × Option Bool} (h : c.state = some s) (bit : Bool) : MultiTapeTM.step c = (action atm s c.inputSymbol c.workTapeSymbols bit).apply c

A running instruction of the strict table applies Strict.action.

theorem Turing.MultiTapeATM.Strict.step_cfg_none {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol State input} {q : State} (h : c.state = some q) (x : Bool) : MultiTapeTM.step (cfg c none) = cfg c (some x)

The strict table stores the existential coin.

theorem Turing.MultiTapeATM.Strict.step_cfg_some {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol State input} {q : State} (h : c.state = some q) (x y : Bool) : MultiTapeTM.step (cfg c (some x)) = cfg (atm.next (if atm.universal q = true then y else x) c) none

With a stored coin, the strict table takes the step of the machine with the coin of the player of its state.

theorem Turing.MultiTapeATM.Strict.stepCoins_cfg {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol State input} {q : State} (h : c.state = some q) (x y : Bool) (coins : List Bool) : atm.strict.stepCoins (x :: y :: coins) (cfg c none) = atm.strict.stepCoins coins (cfg (atm.next (if atm.universal q = true then y else x) c) none)

One step of the machine costs two coins of the strict table.

theorem Turing.MultiTapeATM.Strict.stepCoins_cfg_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol State input} (h : c.state = none) (coins : List Bool) : atm.strict.stepCoins coins (cfg c none) = cfg c none

A halted configuration of the machine is a halted configuration of the strict table.

theorem Turing.MultiTapeATM.Strict.initialConfig_strict {k : ℕ} {Symbol State : Type} (atm : MultiTapeATM k Symbol State) (input : List Symbol) : (MultiTapeMachine.initialConfig atm.strict input).tapes = cfg (atm.toPTM.toNTM.initCfg input) none

The strict table starts with the initial configuration of the machine.

Replaying the strict table

def Turing.MultiTapeATM.gameVerifier {k : ℕ} {State α : Type} (atm : MultiTapeATM k Bool State) (enc : α ↪ List Bool) (x : α × List Bool) : Bool

The verifier of a game on the strict table: it accepts when the strict table, replayed from the moves on the encoded instance, emits [true].

theorem Turing.MultiTapeATM.computableInPolyTime_gameVerifier {k : ℕ} {State : Type} [Finite State] {α : Type} {enc : α ↪ List Bool} (atm : MultiTapeATM k Bool State) : MultiTapeTM.ComputableInPolyTime (atm.gameVerifier enc) (MultiTapeTM.encPair enc MultiTapeTM.encBits) MultiTapeTM.encBool

The verifier of a game on the strict table is polynomial-time: it replays a fixed finite fair-coin table.