The guess-then-verify alternating machine

This file builds the alternating machine that writes a sequence of alternate single-bit moves of two players on a work tape and then runs a deterministic verifier, the guess-then-verify machine (Turing.MultiTapeATM.guessVerify) Chandra, Kozen and Stockmeyer Arora and Barak, Section 5.3.

The machine is assembled from one deterministic machine for each move (Turing.MultiTapeATM.ofTMs). The machine of the move b (Turing.MultiTapeATM.GuessVerify.machine) runs, in sequence (Turing.MultiTapeTM.seq):

1. a deterministic machine prep, which writes on work tape B the frame of L bits true (Turing.MultiTapeTM.frame) followed by the input;
2. the guessing machine (Turing.MultiTapeATM.GuessVerify.guess), which walks along the pairs true, true of the frame and writes the move b over the second cell of each pair; its states record which player is to move, and the states of the universal player's moves are the universal states;
3. a rewind of tape B (Turing.MultiTapeTM.rewindWork), and a deterministic machine verify, started on the frame of the moves followed by the input.

Outside the cells of the moves the two moves agree, so acceptance and halting pass along these steps (Turing.MultiTapeATM.acceptsWithin_add_iff_of_next_eq, Turing.MultiTapeATM.haltsWithin_add_iff_of_next_eq).

Main definitions

• Turing.MultiTapeATM.ofTMs: the alternating machine of a deterministic machine for each move.
• Turing.MultiTapeATM.HaltsWithin: every list of moves reaches a halted configuration.
• Turing.MultiTapeATM.GuessVerify.guess: the guessing machine.
• Turing.MultiTapeATM.guessVerify: the guess-then-verify machine.

Main results

• Turing.MultiTapeATM.acceptsWithin_add_iff_of_next_eq, Turing.MultiTapeATM.haltsWithin_add_iff_of_next_eq: moves that do not matter.
• Turing.MultiTapeATM.GuessVerify.haltsWithin_lift_tag: halting through the guessing phase.
• Turing.MultiTapeATM.GuessVerify.acceptsWithin_lift_none, Turing.MultiTapeATM.GuessVerify.haltsWithin_lift_none: the verifying phase.
• Turing.MultiTapeATM.GuessVerify.prepare_spec: the preparing phase.

References

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

theorem Turing.tapeOfList_set {Symbol : Type u_1} (w : List Symbol) {i : ℕ} (hi : i < w.length) (s : Symbol) : tapeOfList (w.set i s) = Function.update (tapeOfList w) (↑i) (some s)

Setting a cell of a word sets the cell of its tape.

Alternating machines from deterministic machines

noncomputable def Turing.MultiTapeATM.ofTMs {k : ℕ} {Symbol State : Type} (tm : Bool → MultiTapeTM k Symbol State) (universal : State → Bool) : MultiTapeATM k Symbol State

The alternating machine whose move b is a step of the deterministic machine tm b, with universal states universal.

theorem Turing.MultiTapeATM.next_ofTMs {k : ℕ} {Symbol State : Type} {input : List Symbol} (tm : Bool → MultiTapeTM k Symbol State) (universal : State → Bool) (b : Bool) (c : Cfg k Symbol State input) : (ofTMs tm universal).next b c = MultiTapeTM.step c

The move b of ofTMs tm universal is a step of tm b.

theorem Turing.MultiTapeATM.initCfg_ofTMs {k : ℕ} {Symbol State : Type} {input : List Symbol} (tm : Bool → MultiTapeTM k Symbol State) (universal : State → Bool) : (ofTMs tm universal).toPTM.toNTM.initCfg input = Cfg.init (tm false).q₀ input

The initial configuration of ofTMs tm universal is that of tm false.

Halting within a number of moves

def Turing.MultiTapeATM.HaltsWithin {k : ℕ} {Symbol State : Type} {input : List Symbol} (atm : MultiTapeATM k Symbol State) (n : ℕ) (c : Cfg k Symbol State input) : Prop

Every list of n moves from c reaches a halted configuration.

theorem Turing.MultiTapeATM.haltsWithin_zero {k : ℕ} {Symbol State : Type} {input : List Symbol} {atm : MultiTapeATM k Symbol State} {c : Cfg k Symbol State input} : atm.HaltsWithin 0 c ↔ c.state = none

Within no moves, only a halted configuration halts.

theorem Turing.MultiTapeATM.haltsWithin_succ {k : ℕ} {Symbol State : Type} {input : List Symbol} {atm : MultiTapeATM k Symbol State} {n : ℕ} {c : Cfg k Symbol State input} : atm.HaltsWithin (n + 1) c ↔ ∀ (b : Bool), atm.HaltsWithin n (atm.next b c)

Halting within n + 1 moves is halting within n after either move.

theorem Turing.MultiTapeATM.runsInTime_iff_haltsWithin {k : ℕ} {Symbol State : Type} {input : List Symbol} {atm : MultiTapeATM k Symbol State} {t : ℕ} : atm.toPTM.toNTM.RunsInTime input t ↔ atm.HaltsWithin t (atm.toPTM.toNTM.initCfg input)

A time bound is halting within as many moves from the initial configuration.

theorem Turing.MultiTapeATM.haltsWithin_add_iff_of_next_eq {k : ℕ} {Symbol State : Type} {input : List Symbol} {atm : MultiTapeATM k Symbol State} {f : Cfg k Symbol State input → Cfg k Symbol State input} {m n : ℕ} {c : Cfg k Symbol State input} (h : ∀ j < m, ∀ (b : Bool), atm.next b (f^[j] c) = f^[j + 1] c) : atm.HaltsWithin (m + n) c ↔ atm.HaltsWithin n (f^[m] c)

Along steps of f whose two moves agree, halting moves forward.

Moves that do not matter

theorem Turing.MultiTapeATM.acceptsWithin_succ_of_next_eq {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} {n : ℕ} {c c' : Cfg k Bool State input} (h : ∀ (b : Bool), atm.next b c = c') : atm.AcceptsWithin (n + 1) c ↔ atm.AcceptsWithin n c'

A configuration whose two moves agree accepts within n + 1 moves exactly when the common successor accepts within n.

theorem Turing.MultiTapeATM.acceptsWithin_add_iff_of_next_eq {k : ℕ} {State : Type} {atm : MultiTapeATM k Bool State} {input : List Bool} {f : Cfg k Bool State input → Cfg k Bool State input} {m n : ℕ} {c : Cfg k Bool State input} (h : ∀ j < m, ∀ (b : Bool), atm.next b (f^[j] c) = f^[j + 1] c) : atm.AcceptsWithin (m + n) c ↔ atm.AcceptsWithin n (f^[m] c)

Along steps of f whose two moves agree, acceptance moves forward.

The guessing machine

inductive Turing.MultiTapeATM.GuessState : Type

The states of the guessing machine: at a tag cell, or at a cell receiving a move, with the label of the player of the next move (true for universal).

• tag (universal : Bool) : GuessState
• move (universal : Bool) : GuessState

@[instance_reducible]

instance Turing.MultiTapeATM.instDecidableEqGuessState : DecidableEq GuessState

def Turing.MultiTapeATM.instDecidableEqGuessState.decEq (x✝ x✝¹ : GuessState) : Decidable (x✝ = x✝¹)

instance Turing.MultiTapeATM.instFiniteGuessState : Finite GuessState

def Turing.MultiTapeATM.GuessVerify.guess {k : ℕ} (B : Fin k) (b : Bool) : MultiTapeTM k Bool GuessState

The guessing machine with move b on work tape B: at a cell true it moves right to the next cell, which receives the move b, and the player alternates; at any other cell it halts.

def Turing.MultiTapeATM.GuessVerify.cfg {k : ℕ} {input : List Bool} {State : Type} (B : Fin k) (q : Option State) (w : List Bool) (pos : ℕ) : Cfg k Bool State input

A configuration with the word w on tape B and its head at pos, every other work tape blank with its head at 0, the input head at the start and no output.

theorem Turing.MultiTapeATM.GuessVerify.cfg_zero {k : ℕ} {input : List Bool} {State : Type} (B : Fin k) (q : Option State) (w : List Bool) : cfg B q w 0 = wordsCfg input q (Function.update (fun (x : Fin k) => []) B w) []

With its head at 0, tape B is in the normal form of Turing.wordsCfg.

theorem Turing.MultiTapeATM.GuessVerify.step_guess_tag {k : ℕ} {input : List Bool} (B : Fin k) (b : Bool) {w : List Bool} {pos : ℕ} (u : Bool) (h : w[pos]? = some true) : MultiTapeTM.step (cfg B (some (GuessState.tag u)) w pos) = cfg B (some (GuessState.move u)) w (pos + 1)

At a tag true, the guessing machine moves right to the cell of the move.

theorem Turing.MultiTapeATM.GuessVerify.step_guess_move {k : ℕ} {input : List Bool} (B : Fin k) (b : Bool) {w : List Bool} {pos : ℕ} (u : Bool) (h : pos < w.length) : MultiTapeTM.step (cfg B (some (GuessState.move u)) w pos) = cfg B (some (GuessState.tag !u)) (w.set pos b) (pos + 1)

At the cell of a move, the guessing machine writes its move, moves right, and the other player is to move.

theorem Turing.MultiTapeATM.GuessVerify.step_guess_halt {k : ℕ} {input : List Bool} (B : Fin k) (b : Bool) {w : List Bool} {pos : ℕ} (u : Bool) (h : w[pos]? ≠ some true) : MultiTapeTM.step (cfg B (some (GuessState.tag u)) w pos) = cfg B none w pos

At any other cell, the guessing machine halts.

Guess, then verify

noncomputable def Turing.MultiTapeATM.GuessVerify.rewindVerify {k : ℕ} {S₂ : Type} (B : Fin k) (verify : MultiTapeTM k Bool S₂) : MultiTapeTM k Bool (MultiTapeTM.RewindWorkState ⊕ S₂)

Rewind tape B, then run verify.

noncomputable def Turing.MultiTapeATM.GuessVerify.machine {k : ℕ} {S₁ S₂ : Type} (B : Fin k) (prep : MultiTapeTM k Bool S₁) (verify : MultiTapeTM k Bool S₂) (b : Bool) : MultiTapeTM k Bool (S₁ ⊕ GuessState ⊕ MultiTapeTM.RewindWorkState ⊕ S₂)

The deterministic machine of the move b: run prep, guess with the move b, rewind tape B and run verify.

def Turing.MultiTapeATM.GuessVerify.isUniversal {S₁ S₂ : Type} : S₁ ⊕ GuessState ⊕ MultiTapeTM.RewindWorkState ⊕ S₂ → Bool

The universal states of the guess-then-verify machine: the cells of the moves of the universal player.

noncomputable def Turing.MultiTapeATM.guessVerify {k : ℕ} {S₁ S₂ : Type} (B : Fin k) (prep : MultiTapeTM k Bool S₁) (verify : MultiTapeTM k Bool S₂) : MultiTapeATM k Bool (S₁ ⊕ GuessState ⊕ MultiTapeTM.RewindWorkState ⊕ S₂)

The guess-then-verify machine: it prepares tape B by prep, writes the moves of the two players, alternately, over the second cells of the pairs true, true that follow the tape's initial pairs, rewinds tape B and runs verify.

theorem Turing.MultiTapeATM.GuessVerify.step_machine {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} {c : Cfg k Bool (S₁ ⊕ GuessState ⊕ MultiTapeTM.RewindWorkState ⊕ S₂) input} (h : ∀ (u : Bool), c.state ≠ some (Sum.inr (Sum.inl (GuessState.move u)))) (b : Bool) : MultiTapeTM.step c = MultiTapeTM.step c

Outside the cells of the moves, the two moves agree.

noncomputable def Turing.MultiTapeATM.GuessVerify.lift {k : ℕ} (S₁ : Type) {S₂ : Type} (B : Fin k) (verify : MultiTapeTM k Bool S₂) {input : List Bool} (c : Cfg k Bool GuessState input) : Cfg k Bool (S₁ ⊕ GuessState ⊕ MultiTapeTM.RewindWorkState ⊕ S₂) input

A configuration of the guessing machine, as a configuration of the guess-then-verify machine.

theorem Turing.MultiTapeATM.GuessVerify.next_lift {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} {c : Cfg k Bool GuessState input} (h : c.state ≠ none) (b : Bool) : (guessVerify B prep verify).next b (lift S₁ B verify c) = lift S₁ B verify (MultiTapeTM.step c)

In the guessing phase, the move b is a step of the guessing machine with the move b.

theorem Turing.MultiTapeATM.GuessVerify.next_lift_halt {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} (zd : List Bool) (u b : Bool) : (guessVerify B prep verify).next b (lift S₁ B verify (cfg B (some (GuessState.tag u)) (MultiTapeTM.frame zd ++ input) (2 * zd.length))) = lift S₁ B verify (cfg B none (MultiTapeTM.frame zd ++ input) (2 * zd.length))

At the terminator of the frame, the guessing phase ends.

theorem Turing.MultiTapeATM.GuessVerify.next_lift_tag {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} (zd v : List Bool) (c u b : Bool) : (guessVerify B prep verify).next b (lift S₁ B verify (cfg B (some (GuessState.tag u)) (MultiTapeTM.frame (zd ++ c :: v) ++ input) (2 * zd.length))) = lift S₁ B verify (cfg B (some (GuessState.move u)) (MultiTapeTM.frame (zd ++ c :: v) ++ input) (2 * zd.length + 1))

At the tag of a pair, the head moves to its second cell.

theorem Turing.MultiTapeATM.GuessVerify.next_lift_move {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} (zd v : List Bool) (c u b : Bool) : (guessVerify B prep verify).next b (lift S₁ B verify (cfg B (some (GuessState.move u)) (MultiTapeTM.frame (zd ++ c :: v) ++ input) (2 * zd.length + 1))) = lift S₁ B verify (cfg B (some (GuessState.tag !u)) (MultiTapeTM.frame (zd ++ b :: v) ++ input) (2 * (zd.length + 1)))

The second cell of a pair receives the move.

theorem Turing.MultiTapeATM.GuessVerify.haltsWithin_lift_tag {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} (r : ℕ) (zd : List Bool) (u : Bool) (n : ℕ) : (guessVerify B prep verify).HaltsWithin (2 * r + 1 + n) (lift S₁ B verify (cfg B (some (GuessState.tag u)) (MultiTapeTM.frame (zd ++ List.replicate r true) ++ input) (2 * zd.length))) ↔ ∀ (zr : List Bool), zr.length = r → (guessVerify B prep verify).HaltsWithin n (lift S₁ B verify (cfg B none (MultiTapeTM.frame (zd ++ zr) ++ input) (2 * (zd.length + r))))

The guessing phase halts within 2 * r + 1 + n moves from the tag of the first of r pairs true, true exactly when every way of writing the r moves ends the guessing phase in a configuration halting within n moves.

theorem Turing.MultiTapeATM.GuessVerify.state_rightCfg_rightCfg_ne {k : ℕ} {S₁ S₂ : Type} {input : List Bool} (c : Cfg k Bool (MultiTapeTM.RewindWorkState ⊕ S₂) input) (u : Bool) : (MultiTapeTM.Sequential.rightCfg (MultiTapeTM.Sequential.rightCfg c)).state ≠ some (Sum.inr (Sum.inl (GuessState.move u)))

The configurations after the guessing phase are never at the cell of a move.

theorem Turing.MultiTapeATM.GuessVerify.runFrom_rewindWork_cfg {k : ℕ} {B : Fin k} {input w : List Bool} {pos : ℕ} (hpos : pos ≤ w.length) : MultiTapeTM.runFrom (cfg B (some (MultiTapeTM.rewindWork Bool).q₀) w pos) (pos + 2) = cfg B none w 0

Rewinding tape B from pos takes pos + 2 steps.

theorem Turing.MultiTapeATM.GuessVerify.runFrom_lift_none {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input w : List Bool} {pos t : ℕ} (hpos : pos ≤ w.length) (hfin : (MultiTapeTM.runFrom (wordsCfg input (some verify.q₀) (Function.update (fun (x : Fin k) => []) B w) []) t).state = none) (b : Bool) : MultiTapeTM.runFrom (lift S₁ B verify (cfg B none w pos)) (pos + 2 + t) = MultiTapeTM.Sequential.rightCfg (MultiTapeTM.Sequential.rightCfg (MultiTapeTM.Sequential.rightCfg (MultiTapeTM.runFrom (wordsCfg input (some verify.q₀) (Function.update (fun (x : Fin k) => []) B w) []) t)))

After the guessing phase, the machine rewinds tape B and runs verify.

theorem Turing.MultiTapeATM.GuessVerify.next_iterate_rightCfg {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input : List Bool} (c : Cfg k Bool (MultiTapeTM.RewindWorkState ⊕ S₂) input) (j : ℕ) (b : Bool) : (guessVerify B prep verify).next b (MultiTapeTM.step^[j] (MultiTapeTM.Sequential.rightCfg (MultiTapeTM.Sequential.rightCfg c))) = MultiTapeTM.step^[j + 1] (MultiTapeTM.Sequential.rightCfg (MultiTapeTM.Sequential.rightCfg c))

The configurations reached by the deterministic machine of the move false agree with those of every move, outside the moves.

theorem Turing.MultiTapeATM.GuessVerify.acceptsWithin_lift_none {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input w : List Bool} {pos t : ℕ} (hpos : pos ≤ w.length) (hfin : (MultiTapeTM.runFrom (wordsCfg input (some verify.q₀) (Function.update (fun (x : Fin k) => []) B w) []) t).state = none) : (guessVerify B prep verify).AcceptsWithin (pos + 2 + t) (lift S₁ B verify (cfg B none w pos)) ↔ (MultiTapeTM.runFrom (wordsCfg input (some verify.q₀) (Function.update (fun (x : Fin k) => []) B w) []) t).output = [true]

The verifying phase. After the guessing phase, with the word w on tape B, if verify halts within t steps on w, the machine accepts within pos + 2 + t moves exactly when the output of verify is [true].

theorem Turing.MultiTapeATM.GuessVerify.haltsWithin_lift_none {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input w : List Bool} {pos t : ℕ} (hpos : pos ≤ w.length) (hfin : (MultiTapeTM.runFrom (wordsCfg input (some verify.q₀) (Function.update (fun (x : Fin k) => []) B w) []) t).state = none) : (guessVerify B prep verify).HaltsWithin (pos + 2 + t) (lift S₁ B verify (cfg B none w pos))

The verifying phase halts. After the guessing phase, with the word w on tape B, if verify halts within t steps on w, every list of pos + 2 + t moves reaches a halted configuration.

theorem Turing.MultiTapeATM.GuessVerify.prepare_spec {k : ℕ} {S₁ S₂ : Type} {B : Fin k} {prep : MultiTapeTM k Bool S₁} {verify : MultiTapeTM k Bool S₂} {input w : List Bool} {u : ℕ} (hu : prep.HaltsAt (Cfg.init prep.q₀ input) u) (hprep : MultiTapeTM.runFrom (Cfg.init prep.q₀ input) u = wordsCfg input none (Function.update (fun (x : Fin k) => []) B w) []) : (∀ j < u, ∀ (b : Bool), (guessVerify B prep verify).next b (MultiTapeTM.step^[j] ((guessVerify B prep verify).toPTM.toNTM.initCfg input)) = MultiTapeTM.step^[j + 1] ((guessVerify B prep verify).toPTM.toNTM.initCfg input)) ∧ MultiTapeTM.step^[u] ((guessVerify B prep verify).toPTM.toNTM.initCfg input) = lift S₁ B verify (cfg B (some (GuessState.tag false)) w 0)

The preparing phase. If prep halts at step u with the word w on tape B and every other work tape blank, then from the initial configuration the machine reaches the start of the guessing phase in u moves that do not matter.