Alternating machine acceptance, and the machine bridge for the hierarchy

Umbrella file for DescriptiveComplexity.ATMAccept k start, the problem “does this alternating Turing machine with k quantifier blocks accept its input within as many steps as there are positions?”, with the machine carried by the instance as in DescriptiveComplexity.NTMAccept.

The problem is the polynomial hierarchy's analogue of the machine bridge that DescriptiveComplexity.Problems.Machine provides for NP and PTIME: the levels Σₖᵖ/Πₖᵖ of this library are defined by second-order alternation, and the bridge is to say that they are the levels of the alternating-machine hierarchy of Chandra–Kozen–Stockmeyer 1981.

What is here

• The model – DescriptiveComplexity.ATMData and its acceptance (DescriptiveComplexity.MachinesAlt): a machine of DescriptiveComplexity.TMData whose states carry k block marks, with a budget recursion handing each move to the owner of the current state's block. The alternation bound is DescriptiveComplexity.ATMData.BlocksWellFormed, folded into the yes-instances: exactly one mark per state, and a transition either stays in its block or moves to the next one – a condition on a single transition, hence first-order.

• The collapse lemmas (DescriptiveComplexity.MachinesAltPlay), the mathematical content of the bridge's membership half: because the blocks are entered in order, the moves a player makes form one contiguous play of the block, so an existential block's configuration accepts exactly when some play of the block ends well (DescriptiveComplexity.ATMData.altAcc_iff_exists_play) and a universal one's exactly when every play does (DescriptiveComplexity.ATMData.altAcc_iff_forall_play). That is what lets a single second-order quantifier commit a whole phase of the run.

• The round game (DescriptiveComplexity.Problems.Machine.AltGame), the object the second-order blocks of the membership proof guess: k rounds, each choosing a walk – a configuration per position – legal only as far as its own block and reproducing what the earlier rounds committed (DescriptiveComplexity.ATMData.AltGame).

• The translation between a walk and a play, which is where the unary time bound is cashed in: reading a play off a walk (DescriptiveComplexity.ATMData.exists_play_of_legalBelow) and splicing a play into one (DescriptiveComplexity.ATMData.roundCond_splice), on the rank arithmetic of DescriptiveComplexity.Problems.Machine.AltRank.

• The round induction (DescriptiveComplexity.ATMData.altAccepts_iff_altGame): alternating acceptance is the k-round game. This is the membership half's mathematical content, and all that is left of that half is to write the game down as a Σₖ sentence.

• The membership half at every level (DescriptiveComplexity.Problems.Machine.AltMembership): the game is turned into an implication ladder – a universal round always has a move, so the existence clause of DescriptiveComplexity.guardQ is redundant (DescriptiveComplexity.Problems.Machine.AltLadder) – the ladder is rewritten over the relations a second-order block guesses (DescriptiveComplexity.Problems.Machine.AltRel), its quantifiers become the alternating prefix over one guess per round (DescriptiveComplexity.Problems.Machine.AltMatrix), and what is left is the first-order kernel of DescriptiveComplexity.Problems.Machine.AltKernel. So ATMAccept (k+1) true is in Σₖ₊₁ᵖ and ATMAccept (k+1) false in Πₖ₊₁ᵖ.

• The bridge at one block, below: at k = 1 and an existential prefix no state is universal, so the model is the nondeterministic one and ATMAccept 1 true is NP-complete – by two identity interpretations, one marking every element and one forgetting the mark under a guard.

• The hardness half at every level: the machine M_φ of a quantified Boolean formula, one guessing sweep per quantifier block, built inside an ordered QBF instance. Its tape is the instance's elements bracketed by two markers; sweep i walks it once in each direction, and the only choice it ever makes is whether to set the cell of a variable block i marks – so the moves of round i are exactly the truth assignments of block i (DescriptiveComplexity.Problems.Machine.AltGuess). After the last sweep a deterministic check phase walks the clauses, which is where the matrix is read (DescriptiveComplexity.Problems.Machine.AltVerdict). The rounds compose into the quantifier prefix (DescriptiveComplexity.Problems.Machine.AltRounds), and DescriptiveComplexity.Problems.Machine.AltInterp writes the machine down as a two-dimensional interpretation. So ATMAccept (k+1) true is Σₖ₊₁ᵖ-hard and ATMAccept (k+1) false is Πₖ₊₁ᵖ-hard.

Both halves are complete at every level, so the levels of this library's hierarchy are the levels of the alternating-machine one.

theorem DescriptiveComplexity.atmAccept_one_complete : NP.Complete (ATMAccept 1 true)

The machine bridge at one block: alternating acceptance with a single existential block is NP-complete, so the alternating model agrees with DescriptiveComplexity.NTMAccept where the two overlap.

theorem DescriptiveComplexity.atmAccept_mem_sigmaP' (k : ℕ) : (SigmaP (k + 1)).Mem (ATMAccept (k + 1) true)

Alternating acceptance with an existential first block is in Σₖ₊₁ᵖ, the membership half of the bridge.

theorem DescriptiveComplexity.atmAccept_mem_piP' (k : ℕ) : (PiP (k + 1)).Mem (ATMAccept (k + 1) false)

Alternating acceptance with a universal first block is in Πₖ₊₁ᵖ.

theorem DescriptiveComplexity.ATMData.accepts_iff_game {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) (hk : 0 < k) {p₀ p₁ : A} (hmin : MinPos M.Le M.Posn p₀) (hmax : MaxPos M.Le M.Posn p₁) (start : Bool) : M.AltAccepts start ↔ M.AltGame start k

Alternating acceptance is the k-round game, the semantic content of the membership half at every level: an alternating machine accepts exactly when the owner of block 0 can choose a run of its block, the owner of block 1 cannot avoid one of its own, and so on for k rounds.

The hardness half

theorem DescriptiveComplexity.atmAccept_sigmaP_hard (k : ℕ) : (SigmaP (k + 1)).Hard (ATMAccept (k + 1) true)

Alternating acceptance with an existential first block is Σₖ₊₁ᵖ-hard: DescriptiveComplexity.QBF reduces to it by building the machine M_φ of the formula inside the instance, one guessing sweep per quantifier block.

theorem DescriptiveComplexity.atmAccept_piP_hard (k : ℕ) : (PiP (k + 1)).Hard (ATMAccept (k + 1) false)

Alternating acceptance with a universal first block is Πₖ₊₁ᵖ-hard, by the same reduction at the other starting polarity: the machine is the same, and only the matrix shape and the block that moves first change.

The bridge

theorem DescriptiveComplexity.atmAccept_sigmaP_complete (k : ℕ) : (SigmaP (k + 1)).Complete (ATMAccept (k + 1) true)

The machine bridge for the polynomial hierarchy, existential half: alternating acceptance with k + 1 blocks, the first existential, is Σₖ₊₁ᵖ-complete. The classes of this library are defined by second-order alternation; this theorem says they are the levels of the alternating-machine hierarchy of Chandra–Kozen–Stockmeyer 1981.

theorem DescriptiveComplexity.atmAccept_piP_complete (k : ℕ) : (PiP (k + 1)).Complete (ATMAccept (k + 1) false)

The machine bridge, universal half: with a universal first block, Πₖ₊₁ᵖ-complete.

theorem DescriptiveComplexity.mem_sigmaP_iff_le_atmAccept {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : (SigmaP (k + 1)).Mem P ↔ Nonempty (OrderedFOReduction P (ATMAccept (k + 1) true))

The machine characterization of Σₖ₊₁ᵖ: a problem sits at the k+1-st level exactly when it ordered-FO-reduces to acceptance by an alternating machine with k + 1 blocks starting existentially. Forward through DescriptiveComplexity.QBF, backward because membership travels along reductions.

theorem DescriptiveComplexity.atmAccept_one_coNP_complete : coNP.Complete (ATMAccept 1 false)

The machine bridge at one universal block: alternating acceptance with a single universal block is coNP-complete. The model is the co-nondeterministic one – a universal configuration accepts when it has a successor and every successor accepts, so the machine accepts exactly when every run of it does – and this is the dual of DescriptiveComplexity.atmAccept_one_complete, which reads the same machine at the existential polarity as DescriptiveComplexity.NTMAccept.

theorem DescriptiveComplexity.mem_piP_iff_le_atmAccept {L : FirstOrder.Language} (k : ℕ) (P : DecisionProblem L) : (PiP (k + 1)).Mem P ↔ Nonempty (OrderedFOReduction P (ATMAccept (k + 1) false))

The machine characterization of Πₖ₊₁ᵖ.