One block at a time: collapsing the moves of a player into a single play

The mathematical content of the machine bridge for the polynomial hierarchy. DescriptiveComplexity.ATMData.AltAcc recurses one step at a time, handing each move to the owner of the current state's block; a Σₖ definition, and the k-round game it describes, hands each player all of its moves at once. That the two agree is the content of this file, and it is where the alternation bound is spent: because a transition never decreases the block index and never raises it by more than one (DescriptiveComplexity.ATMData.BlocksWellFormed), the times at which a given player moves form one contiguous stretch of the run – a play of the block – and the whole stretch may be committed in a single quantifier.

The two collapses

A play of block i from c (DescriptiveComplexity.ATMData.BlockPlay) is a sequence of genuine steps whose configurations are, up to the last one, in block i and not accepting: it stops exactly when the machine accepts or hands over to block i + 1.

• Existential (DescriptiveComplexity.ATMData.altAcc_iff_exists_play): a configuration of an existential block accepts exactly when some play of the block ends accepting, or hands a configuration over to block i + 1 which itself accepts with the remaining budget.
• Universal (DescriptiveComplexity.ATMData.altAcc_iff_forall_play): a configuration of a universal block accepts exactly when every play of the block is all right – it hands over only accepting configurations, and it can never stall inside the block, neither by getting stuck nor by exhausting the budget. The second clause is the “a stuck universal state rejects” convention of DescriptiveComplexity.MachinesAlt in the form the proofs use.

Both statements are equivalences, and both are proved by induction on the budget with the play generalized, so no strategy tree is ever built.

Reading the block structure

theorem DescriptiveComplexity.ATMData.blk_unique {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {q : A} {j j' : ℕ} (h : M.Blk j q) (h' : M.Blk j' q) : j = j'

A state has only one block.

theorem DescriptiveComplexity.ATMData.not_isUniv_of_blk {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {start : Bool} {i : ℕ} {q : A} (h : M.Blk i q) (hpol : blockPol start i = true) : ¬M.IsUniv start q

A state of an existential block belongs to the existential player.

theorem DescriptiveComplexity.ATMData.isUniv_of_blk {A : Type} {M : ATMData A} {start : Bool} {i : ℕ} {q : A} (h : M.Blk i q) (hpol : blockPol start i = false) : M.IsUniv start q

A state of a universal block belongs to the universal player.

theorem DescriptiveComplexity.ATMData.blk_step {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {i : ℕ} {c d : Config A} (hstep : M.Step c d) (hi : M.Blk i c.state) : M.Blk i d.state ∨ M.Blk (i + 1) d.state

A step stays in its block or moves to the next one: the alternation bound, read on a single step.

Plays of a block

def DescriptiveComplexity.ATMData.BlockPlay {A : Type} (M : ATMData A) (i : ℕ) (c : Config A) (ℓ : ℕ) (f : ℕ → Config A) : Prop

A play of block i from c: ℓ genuine steps, whose configurations before the last one are in block i and not accepting. A play therefore stops as soon as the machine accepts or hands over to the next block, and its last configuration is the one the next round of the game starts from.

Equations

• M.BlockPlay i c ℓ f = (f 0 = c ∧ (∀ j < ℓ, M.Step (f j) (f (j + 1))) ∧ ∀ j < ℓ, M.Blk i (f j).state ∧ ¬M.Acc (f j).state)

def DescriptiveComplexity.ATMData.PlayEnds {A : Type} (M : ATMData A) (start : Bool) (i n ℓ : ℕ) (f : ℕ → Config A) : Prop

A play of an existential block ends well: accepting, or handing an accepting configuration over to block i + 1.

Equations

• M.PlayEnds start i n ℓ f = (M.Acc (f ℓ).state ∨ M.Blk (i + 1) (f ℓ).state ∧ M.AltAcc start (n - ℓ) (f ℓ))

def DescriptiveComplexity.ATMData.UnivPlayOk {A : Type} (M : ATMData A) (start : Bool) (i n ℓ : ℕ) (f : ℕ → Config A) : Prop

A play of a universal block is all right: what it hands over to block i + 1 accepts, and if it is still inside the block without having accepted then it can – and must – go on, so the universal player can neither get stuck nor run the budget out inside the block.

Equations

• One or more equations did not get rendered due to their size.

Prepending and shifting a play

def DescriptiveComplexity.ATMData.consPlay {A : Type} (c : Config A) (f : ℕ → Config A) : ℕ → Config A

The play f with c prepended.

Equations

• DescriptiveComplexity.ATMData.consPlay c f 0 = c
• DescriptiveComplexity.ATMData.consPlay c f j.succ = f j

@[simp]

theorem DescriptiveComplexity.ATMData.consPlay_zero {A : Type} (c : Config A) (f : ℕ → Config A) : consPlay c f 0 = c

@[simp]

theorem DescriptiveComplexity.ATMData.consPlay_succ {A : Type} (c : Config A) (f : ℕ → Config A) (j : ℕ) : consPlay c f (j + 1) = f j

theorem DescriptiveComplexity.ATMData.BlockPlay.cons {A : Type} {M : ATMData A} {i : ℕ} {c d : Config A} {ℓ : ℕ} {f : ℕ → Config A} (h : M.BlockPlay i d ℓ f) (hstep : M.Step c d) (hblk : M.Blk i c.state) (hacc : ¬M.Acc c.state) : M.BlockPlay i c (ℓ + 1) (consPlay c f)

Prepending a step to a play of the same block.

theorem DescriptiveComplexity.ATMData.BlockPlay.tail {A : Type} {M : ATMData A} {i : ℕ} {c : Config A} {ℓ : ℕ} {f : ℕ → Config A} (h : M.BlockPlay i c (ℓ + 1) f) : M.BlockPlay i (f 1) ℓ fun (j : ℕ) => f (j + 1)

The play f with its first configuration dropped.

Running an existential play

theorem DescriptiveComplexity.ATMData.altAcc_of_steps {A : Type} {M : ATMData A} {start : Bool} (ℓ n : ℕ) (f : ℕ → Config A) : ℓ ≤ n → (∀ j < ℓ, M.Step (f j) (f (j + 1))) → (∀ j < ℓ, ¬M.IsUniv start (f j).state) → M.AltAcc start (n - ℓ) (f ℓ) → M.AltAcc start n (f 0)

A run of moves that all belong to the existential player accepts as soon as its end does. This is the “easy” half of both collapses: the budget is spent one step at a time, and each step is a legitimate existential choice.

The existential collapse

theorem DescriptiveComplexity.ATMData.altAcc_iff_exists_play {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {start : Bool} {i : ℕ} {c : Config A} (hpol : blockPol start i = true) (hi : M.Blk i c.state) (n : ℕ) : M.AltAcc start n c ↔ ∃ ℓ ≤ n, ∃ (f : ℕ → Config A), M.BlockPlay i c ℓ f ∧ M.PlayEnds start i n ℓ f

The moves of an existential block collapse into one play.

The universal collapse

theorem DescriptiveComplexity.ATMData.altAcc_iff_forall_play {A : Type} {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) {start : Bool} {i : ℕ} {c : Config A} (hpol : blockPol start i = false) (hi : M.Blk i c.state) (n : ℕ) : M.AltAcc start n c ↔ ∀ ℓ ≤ n, ∀ (f : ℕ → Config A), M.BlockPlay i c ℓ f → M.UnivPlayOk start i n ℓ f

The moves of a universal block collapse into one play.