Alternating machines

An alternating machine Chandra, Kozen and Stockmeyer Arora and Barak, Section 5.3 is a nondeterministic machine whose states are labelled existential or universal. Here it is a closed fair-coin table (Turing.MultiTapePTM, the parametric machine with one action for each of two choices) together with such a labelling (Turing.MultiTapeATM): at a running configuration the two transitions of the table are the two moves (Turing.MultiTapeATM.next), as for the two transition functions of Arora and Barak. A step of the machine is a step of the nondeterministic machine Turing.MultiTapePTM.toNTM of the table, so no configuration is stuck, and time bounds are those of that nondeterministic machine (Turing.MultiTapeNTM.RunsInTime).

Acceptance is the least fixed point of the labelling: a halted configuration accepts when its output is exactly [true], an existential configuration when one of its two moves leads to an accepting configuration, and a universal configuration when both do. It is defined through the number of moves allowed (Turing.MultiTapeATM.AcceptsWithin): within 0 moves only a halted configuration with output [true] accepts, and a running configuration accepts within n + 1 moves when one (existential) or both (universal) of its moves accept within n. The machine accepts an input when its initial configuration accepts within some number of moves (Turing.MultiTapeATM.Accepts). Infinite branches never accept, and running configurations reached when the moves are exhausted do not accept.

A machine decides A within time t (Turing.MultiTapeATM.DecidesInTime) when on every encoded instance enc a every computation path of at least t a steps ends halted, and a ∈ A exactly when the machine accepts enc a. Under such a bound, acceptance is acceptance within t a moves (Turing.MultiTapeATM.accepts_iff_acceptsWithin). Turing.MultiTapeATM.DecidableInPolyTime asks for one machine with a binary alphabet and finitely many states, and one polynomially bounded time bound, for all instances; like Turing.MultiTapeNTM.DecidableInPolyTime, it is relative to the encoding of instances.

Main definitions

• Turing.MultiTapeATM: an alternating machine, a fair-coin table with universal states.
• Turing.MultiTapeATM.next, Turing.MultiTapeATM.action: the configuration after a move, and the action of a move.
• Turing.MultiTapeATM.AcceptsWithin, Turing.MultiTapeATM.Accepts: acceptance.
• Turing.MultiTapeATM.DecidesInTime, Turing.MultiTapeATM.DecidableInTime, Turing.MultiTapeATM.DecidableInPolyTime: deciding a problem within a time bound.

Main results

• Turing.MultiTapeATM.AcceptsWithin.mono: acceptance within n moves is acceptance within more.
• Turing.MultiTapeATM.runsInTime_iff_stepCoins: time bounds through lists of moves.
• Turing.MultiTapeATM.accepts_iff_acceptsWithin: under a time bound t, acceptance is acceptance within t moves.
• Turing.MultiTapeATM.accepts_iff_toNTM_accepts: without universal states, acceptance is acceptance by the nondeterministic machine of the table.

References

• A. K. Chandra, D. C. Kozen, L. J. Stockmeyer, Alternation
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• M. Sipser, Introduction to the Theory of Computation

structure Turing.MultiTapeATM (k : ℕ) (Symbol State : Type) : Type

An alternating machine Chandra, Kozen and Stockmeyer: a closed fair-coin table, whose two transitions at a running configuration are the two moves, together with a labelling of its states as universal or existential.

• toPTM : MultiTapePTM k Symbol State

  The transition table, with one action for each of the two moves.

• universal : State → Bool

  Whether a state is universal; the other states are existential.

noncomputable def Turing.MultiTapeATM.next {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) (b : Bool) (c : Cfg k Symbol State input) : Cfg k Symbol State input

The configuration after the move b: one step of the table with the coin b. A halted configuration stays unchanged.

def Turing.MultiTapeATM.action {k : ℕ} {Symbol State : Type} (atm : MultiTapeATM k Symbol State) (state : State) (symbol : Option Symbol) (work : Fin k → Option Symbol) (b : Bool) : Action k Symbol State

The action of the move b at a state and read symbols.

theorem Turing.MultiTapeATM.next_of_state {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) (b : Bool) : atm.next b c = (atm.action q c.inputSymbol c.workTapeSymbols b).apply c

A move from a running configuration applies its action.

theorem Turing.MultiTapeATM.next_of_halted {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) {c : Cfg k Symbol State input} (h : c.state = none) (b : Bool) : atm.next b c = c

A halted configuration has no other move.

theorem Turing.MultiTapeATM.stepCoins_cons {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) (b : Bool) (coins : List Bool) (c : Cfg k Symbol State input) : atm.toPTM.stepCoins (b :: coins) c = atm.toPTM.stepCoins coins (atm.next b c)

Replaying moves one at a time.

theorem Turing.MultiTapeATM.stepCoins_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.toPTM.stepCoins coins c = c

A halted configuration ignores every list of moves.

Acceptance

def Turing.MultiTapeATM.AcceptsWithin {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {input : List Bool} : ℕ → Cfg k Bool State input → Prop

Acceptance within n moves: within 0 moves a configuration accepts when it has halted with output [true]; within n + 1 moves a halted configuration accepts when its output is [true], and a running configuration when one of its two moves (existential state) or both of them (universal state) lead to configurations accepting within n moves.

def Turing.MultiTapeATM.Accepts {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) (input : List Bool) : Prop

The machine accepts input when its initial configuration accepts within some number of moves: the least fixed point of the labelling.

theorem Turing.MultiTapeATM.acceptsWithin_of_halted {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {input : List Bool} {n : ℕ} {c : Cfg k Bool State input} (h : c.state = none) : atm.AcceptsWithin n c ↔ c.output = [true]

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

theorem Turing.MultiTapeATM.not_acceptsWithin_zero {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {input : List Bool} {c : Cfg k Bool State input} {q : State} (h : c.state = some q) : ¬atm.AcceptsWithin 0 c

A running configuration does not accept without moves.

theorem Turing.MultiTapeATM.acceptsWithin_succ_of_universal {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {input : List Bool} {n : ℕ} {c : Cfg k Bool State input} {q : State} (h : c.state = some q) (hq : atm.universal q = true) : atm.AcceptsWithin (n + 1) c ↔ ∀ (b : Bool), atm.AcceptsWithin n (atm.next b c)

A universal configuration accepts within n + 1 moves when both of its moves accept within n.

theorem Turing.MultiTapeATM.acceptsWithin_succ_of_existential {k : ℕ} {State : Type} (atm : MultiTapeATM k Bool State) {input : List Bool} {n : ℕ} {c : Cfg k Bool State input} {q : State} (h : c.state = some q) (hq : atm.universal q = false) : atm.AcceptsWithin (n + 1) c ↔ ∃ (b : Bool), atm.AcceptsWithin n (atm.next b c)

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

theorem Turing.MultiTapeATM.AcceptsWithin.mono {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} {n : ℕ} {c : Cfg k Bool State input} {n' : ℕ} (h : atm.AcceptsWithin n c) (hn : n ≤ n') : atm.AcceptsWithin n' c

Acceptance within n moves is acceptance within more.

theorem Turing.MultiTapeATM.AcceptsWithin.of_halted_stepCoins {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} {n : ℕ} {c : Cfg k Bool State input} {t : ℕ} (ht : ∀ (coins : List Bool), coins.length = t → (atm.toPTM.stepCoins coins c).state = none) (h : atm.AcceptsWithin n c) : atm.AcceptsWithin t c

If every list of t moves from c reaches a halted configuration, acceptance within any number of moves is acceptance within t.

Time bounds

theorem Turing.MultiTapeATM.state_stepCoins_eq_none {k : ℕ} {Symbol State : Type} {atm : MultiTapeATM k Symbol State} {input : List Symbol} {t : ℕ} (h : atm.toPTM.toNTM.RunsInTime input t) {coins : List Bool} (hlen : coins.length = t) : (atm.toPTM.stepCoins coins (atm.toPTM.toNTM.initCfg input)).state = none

Under a time bound t, every list of t moves from the initial configuration reaches a halted configuration.

theorem Turing.MultiTapeATM.runsInTime_iff_stepCoins {k : ℕ} {Symbol State : Type} {atm : MultiTapeATM k Symbol State} {input : List Symbol} {t : ℕ} : atm.toPTM.toNTM.RunsInTime input t ↔ ∀ (coins : List Bool), coins.length = t → (atm.toPTM.stepCoins coins (atm.toPTM.toNTM.initCfg input)).state = none

Time bounds through moves. Every computation path of at least t steps ends halted exactly when every list of t moves from the initial configuration reaches a halted configuration.

theorem Turing.MultiTapeATM.accepts_iff_acceptsWithin {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} {t : ℕ} (h : atm.toPTM.toNTM.RunsInTime input t) : atm.Accepts input ↔ atm.AcceptsWithin t (atm.toPTM.toNTM.initCfg input)

Acceptance under a time bound. If every computation path of at least t steps ends halted, the machine accepts exactly when its initial configuration accepts within t moves.

Machines without universal states

theorem Turing.MultiTapeATM.acceptsWithin_iff_exists_stepCoins {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} (h : ∀ (q : State), atm.universal q = false) {n : ℕ} {c : Cfg k Bool State input} : atm.AcceptsWithin n c ↔ ∃ (coins : List Bool), coins.length = n ∧ (atm.toPTM.stepCoins coins c).state = none ∧ (atm.toPTM.stepCoins coins c).output = [true]

Without universal states, a configuration accepts within n moves exactly when some list of n moves reaches a halted configuration with output [true].

theorem Turing.MultiTapeATM.accepts_iff_toNTM_accepts {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} (h : ∀ (q : State), atm.universal q = false) {t : ℕ} (ht : atm.toPTM.toNTM.RunsInTime input t) : atm.Accepts input ↔ atm.toPTM.toNTM.Accepts input

Without universal states an alternating machine is nondeterministic: under a time bound, it accepts exactly when the nondeterministic machine of its table accepts.

Deciding problems

def Turing.MultiTapeATM.DecidesInTime {k : ℕ} {State α : Type} (atm : MultiTapeATM k Bool State) (enc : α ↪ List Bool) (A : Set α) (t : α → ℕ) : Prop

atm decides A within t relative to the encoding enc: on every encoded instance enc a, every computation path of at least t a steps ends halted, and a ∈ A exactly when atm accepts enc a.

def Turing.MultiTapeATM.DecidableInTime {α : Type} (A : Set α) (enc : α ↪ List Bool) (t : α → ℕ) : Prop

Some alternating machine with a binary alphabet and finitely many states decides A within t.

def Turing.MultiTapeATM.DecidableInPolyTime {α : Type} (A : Set α) (enc : α ↪ List Bool) : Prop

Some alternating machine with a binary alphabet and finitely many states decides A within a time bound polynomial in the length of the encoded instance.

theorem Turing.MultiTapeATM.DecidesInTime.mono {k : ℕ} {State α : Type} {atm : MultiTapeATM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t t' : α → ℕ} (h : atm.DecidesInTime enc A t) (ht : ∀ (a : α), t a ≤ t' a) : atm.DecidesInTime enc A t'

Time bounds can be increased.

theorem Turing.MultiTapeATM.DecidesInTime.mem_iff {k : ℕ} {State α : Type} {atm : MultiTapeATM k Bool State} {enc : α ↪ List Bool} {A : Set α} {t : α → ℕ} (h : atm.DecidesInTime enc A t) (a : α) : a ∈ A ↔ atm.AcceptsWithin (t a) (atm.toPTM.toNTM.initCfg (enc a))

Under its time bound, a deciding machine decides by acceptance within t a moves.