The matrix of the ladder

The ladder of DescriptiveComplexity.Problems.Machine.AltLadder alternates its own quantifiers; a Σₖ sentence puts the alternation in the prefix and leaves a quantifier-free chain behind. This file is that reshuffling, at the level of the semantics: DescriptiveComplexity.ATMData.runMatrix is the ladder with its quantifiers stripped – a conjunction where the round is existential, an implication where it is universal (DescriptiveComplexity.polConn) – read at a family of assignments, one per round, and DescriptiveComplexity.ATMData.altBlockQuant_runMatrix puts the quantifiers back as the alternating prefix DescriptiveComplexity.altBlockQuant.

The two lemmas that make it work pull a condition on the round already chosen out of the quantifiers over the rounds still to come (DescriptiveComplexity.altBlockQuant_and_left and DescriptiveComplexity.altBlockQuant_imp_left); both need the assignments to form a nonempty type, which they do – the empty relation is one.

Pulling a condition out of the prefix

def DescriptiveComplexity.polConn (pol : Bool) (X Y : Prop) : Prop

The connective a round of the ladder uses: a conjunction where the round is existential, an implication where it is universal.

Equations

• DescriptiveComplexity.polConn true X Y = (X ∧ Y)
• DescriptiveComplexity.polConn false X Y = (X → Y)

theorem DescriptiveComplexity.altBlockQuant_and_left {A : Type} {B : SOBlock} (ρ₀ : B.Assignment A) (m : ℕ) (F : Prop) (P : (Fin m → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B m (fun (ρs : Fin m → B.Assignment A) => F ∧ P ρs) pol ↔ F ∧ altBlockQuant A B m P pol

A conjunct that does not mention the quantified rounds comes out of the prefix.

theorem DescriptiveComplexity.altBlockQuant_imp_left {A : Type} {B : SOBlock} (ρ₀ : B.Assignment A) (m : ℕ) (F : Prop) (P : (Fin m → B.Assignment A) → Prop) (pol : Bool) : altBlockQuant A B m (fun (ρs : Fin m → B.Assignment A) => F → P ρs) pol ↔ F → altBlockQuant A B m P pol

A hypothesis that does not mention the quantified rounds comes out of the prefix.

theorem DescriptiveComplexity.altBlockQuant_step {A : Type} {B : SOBlock} (ρ₀ : B.Assignment A) (m : ℕ) (pol : Bool) (C : B.Assignment A → Prop) (Q : B.Assignment A → (Fin m → B.Assignment A) → Prop) (R : B.Assignment A → Prop) (h : ∀ (ρ : B.Assignment A), altBlockQuant A B m (Q ρ) !pol ↔ R ρ) : altBlockQuant A B (m + 1) (fun (ρs : Fin (m + 1) → B.Assignment A) => polConn pol (C (ρs 0)) (Q (ρs 0) fun (j : Fin m) => ρs j.succ)) pol ↔ bareQ pol C R

One round of the prefix. The outermost block of the prefix is the round DescriptiveComplexity.bareQ quantifies, once the condition on it is pulled out of the blocks that follow.

The matrix

def DescriptiveComplexity.ATMData.RunGuard {A : Type} (M : ATMData A) (i : ℕ) (prev : Option (tmGuessBlock.Assignment A)) (ρ : tmGuessBlock.Assignment A) : Prop

The condition round i puts on its guess, with the round before it – or nothing at all, at the first round, which only has to be legal.

Equations

• M.RunGuard i none ρ = M.RunLegalBelow ρ 1
• M.RunGuard i (some ρp) ρ = M.RunRoundCond ρp ρ i

def DescriptiveComplexity.ATMData.runMatrix {A : Type} (M : ATMData A) (start : Bool) (m _i : ℕ) : Option (tmGuessBlock.Assignment A) → (Fin m → tmGuessBlock.Assignment A) → Prop

The ladder with its quantifiers stripped. runMatrix M start m i prev ρs is the chain of the m rounds still to play, starting at round i with prev the round before it – none at the very first round, which has nothing to inherit. When no round is left the last guess must accept.

Equations

• One or more equations did not get rendered due to their size.
• M.runMatrix start 0 x✝ none x_5 = False
• M.runMatrix start 0 x✝ (some ρp) x_5 = M.RunAccAt ρp

theorem DescriptiveComplexity.ATMData.altBlockQuant_runMatrix_some {A : Type} {M : ATMData A} {start : Bool} (m i : ℕ) (ρp : tmGuessBlock.Assignment A) : altBlockQuant A tmGuessBlock m (M.runMatrix start m i (some ρp)) (blockPol start i) ↔ M.runLadder start i m ρp

The prefix puts the rounds back, from a round that has a predecessor on.

theorem DescriptiveComplexity.ATMData.altBlockQuant_runMatrix {A : Type} {M : ATMData A} {start : Bool} (n : ℕ) : altBlockQuant A tmGuessBlock n (M.runMatrix start n 0 none) start ↔ M.RunAltLadder start n

The prefix puts the rounds back, at the first round: the alternating second-order prefix over one guess per round says exactly what the ladder does.