The round game as an implication ladder

The last semantic step before the Σₖ sentence of the membership half. The game of DescriptiveComplexity.Problems.Machine.AltGame quantifies its rounds with DescriptiveComplexity.guardQ, whose universal case carries an existence clause: a universal player with no legal move loses rather than winning vacuously. Over configurations that clause is harmless, but over walks it is an existential second-order quantifier sitting inside a universal block, and a sentence built on it would not be Σₖ at all.

The clause is however redundant. A round always has a move available: follow the previous round's walk as far as it is committed, and from the entry into the round's own block run greedily – step while a step is available, stand still once stuck – which is DescriptiveComplexity.ATMData.greedyFrom. So the game can be restated with the unguarded DescriptiveComplexity.bareQ, and DescriptiveComplexity.ATMData.AltLadder is that restatement: an alternating chain of conjunctions and implications, which is exactly the shape a first-order kernel can have.

The one clause that is not redundant is at the top: round 0 has no previous walk to extend, so a legal walk exists only if an initial configuration does. That is first-order – it is ∃ q, Start q, the rest being supplied by DescriptiveComplexity.TMData.exists_isInit – and it is carried into the sentence as a plain conjunct rather than as a quantifier.

Unguarded alternation

def DescriptiveComplexity.bareQ (pol : Bool) {α : Type} (C P : α → Prop) : Prop

Quantification with a polarity, unguarded: existentially the guard is conjoined, universally it is assumed. Unlike DescriptiveComplexity.guardQ nothing here asks the guard to be satisfiable, which is what makes this shape expressible by a first-order kernel under a second-order prefix.

Equations

• DescriptiveComplexity.bareQ true C P = ∃ (a : α), C a ∧ P a
• DescriptiveComplexity.bareQ false C P = ∀ (a : α), C a → P a

theorem DescriptiveComplexity.bareQ_true {α : Type} (C P : α → Prop) : bareQ true C P ↔ ∃ (a : α), C a ∧ P a

theorem DescriptiveComplexity.bareQ_false {α : Type} (C P : α → Prop) : bareQ false C P ↔ ∀ (a : α), C a → P a

theorem DescriptiveComplexity.bareQ_congr (pol : Bool) {α : Type} {C C' P P' : α → Prop} (hC : ∀ (a : α), C a ↔ C' a) (hP : ∀ (a : α), C a → (P a ↔ P' a)) : bareQ pol C P ↔ bareQ pol C' P'

Unguarded quantification only depends on its two predicates up to pointwise equivalence.

theorem DescriptiveComplexity.guardQ_iff_bareQ (pol : Bool) {α : Type} {C P : α → Prop} (hne : ∃ (a : α), C a) : guardQ pol C P ↔ bareQ pol C P

A satisfiable guard makes the two quantifications agree: the existence clause of DescriptiveComplexity.guardQ is the only difference between them.

The greedy continuation of a round

noncomputable def DescriptiveComplexity.ATMData.greedyFrom {A : Type} (M : ATMData A) (prev : A → Config A) (t : A) : A → Config A

The walk following prev up to t and running greedily after it: the move a round can always make. It is DescriptiveComplexity.ATMData.splice of the greedy sequence, with no bound on its length – a walk never has to stand still, since DescriptiveComplexity.ATMData.greedy already does when it must.

Equations

• M.greedyFrom prev t x = if M.Posn x ∧ ¬M.Le x t then M.greedy (prev t) (DescriptiveComplexity.bitRank M.Le M.Posn x - DescriptiveComplexity.bitRank M.Le M.Posn t) else prev x

theorem DescriptiveComplexity.ATMData.greedyFrom_of_le {A : Type} {M : ATMData A} {prev : A → Config A} {t x : A} (h : ¬(M.Posn x ∧ ¬M.Le x t)) : M.greedyFrom prev t x = prev x

Below the entry time the continuation is the previous walk.

theorem DescriptiveComplexity.ATMData.greedyFrom_of_lt {A : Type} {M : ATMData A} (hlin : IsLinOrd M.Le) {prev : A → Config A} {t x : A} (hx : M.Posn x) (hle : M.Le t x) : M.greedyFrom prev t x = M.greedy (prev t) (bitRank M.Le M.Posn x - bitRank M.Le M.Posn t)

From the entry time on, the continuation is the greedy sequence.

theorem DescriptiveComplexity.ATMData.roundCond_greedyFrom {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {i : ℕ} {prev : A → Config A} (hprev : M.LegalBelow i prev) {t : A} (ht : M.Posn t) (hti : M.Blk i (prev t).state) (hpast : ∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (prev s).state) : M.RoundCond i prev (M.greedyFrom prev t)

The greedy continuation is an admissible move for round i, given the entry t into block i: it reproduces everything the earlier rounds committed – they committed exactly the times strictly below t – and it is legal below block i + 1 because the greedy sequence is.

Every round has a move

theorem DescriptiveComplexity.ATMData.exists_entry {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {i : ℕ} (hi : 0 < i) {prev : A → Config A} (hprev : M.LegalBelow i prev) : (∀ (x : A), M.Posn x → M.BlkLt i (prev x).state) ∨ ∃ (t : A), M.Posn t ∧ M.Blk i (prev t).state ∧ ∀ (s : A), M.Posn s → M.Le s t → s ≠ t → M.BlkLt i (prev s).state

Either the previous walk never reaches block i, or it enters it at a definite time. The entry is the lowest time whose block is not below i, and it is in block i exactly because the step into it is legal.

theorem DescriptiveComplexity.ATMData.exists_roundCond {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {i : ℕ} (hi : 0 < i) {prev : A → Config A} (hprev : M.LegalBelow i prev) : ∃ (w : A → Config A), M.RoundCond i prev w

A round always has an admissible move, which is what makes the existence clause of DescriptiveComplexity.guardQ redundant from round 1 on. If the previous walk never reaches block i it is itself admissible – it has nothing left to answer for – and otherwise the greedy continuation of its entry into the block is.

The ladder

def DescriptiveComplexity.ATMData.gameLadder {A : Type} (M : ATMData A) (start : Bool) (i : ℕ) : ℕ → (A → Config A) → Prop

The game from round i on, unguarded: the shape a first-order kernel can express, an alternating chain of conjunctions and implications.

Equations

• One or more equations did not get rendered due to their size.
• M.gameLadder start i 0 x✝ = M.AccAt x✝

def DescriptiveComplexity.ATMData.AltLadder {A : Type} (M : ATMData A) (start : Bool) : ℕ → Prop

The whole k-round ladder, with the first round peeled off as in DescriptiveComplexity.ATMData.AltGame.

Equations

• One or more equations did not get rendered due to their size.
• M.AltLadder start 0 = False

theorem DescriptiveComplexity.ATMData.gameFrom_iff_gameLadder {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) (start : Bool) (m i : ℕ) : 0 < i → ∀ (prev : A → Config A), M.LegalBelow i prev → (M.gameFrom start i m prev ↔ M.gameLadder start i m prev)

The game is the ladder, from round 1 on.

theorem DescriptiveComplexity.ATMData.altGame_iff_altLadder {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) (hinit : ∃ (c₀ : Config A), M.IsInit c₀) (start : Bool) : M.AltGame start k ↔ M.AltLadder start k

The whole game is the whole ladder. The hypothesis is the one existence clause that is not redundant: round 0 extends no previous walk, so it needs an initial configuration to exist.

theorem DescriptiveComplexity.ATMData.altAccepts_iff_altLadder {A : Type} [Finite A] {M : ATMData A} {k : ℕ} (hbwf : M.BlocksWellFormed k) (hlin : IsLinOrd M.Le) {p₀ p₁ : A} (hmin : MinPos M.Le M.Posn p₀) (hmax : MaxPos M.Le M.Posn p₁) (hk : 0 < k) (hinit : ∃ (c₀ : Config A), M.IsInit c₀) (start : Bool) : M.AltAccepts start ↔ M.AltLadder start k

Alternating acceptance is the ladder, the statement the Σₖ sentence of the membership half expresses.