A second-order alternating game is GAME on an exponential expansion

The alternating counterpart of DescriptiveComplexity.Exponential.Reach, and the way into EXPTIME that needs no succinctness argument. Compare the two definitions, which are the same sentence up to the name of the universe:

SOGameSpec.Accepts A = ∃ ρ, spec.IsStart ρ ∧ spec.Wins ρ
GameWon            M = ∃ s, AGStart s   ∧ WinsOn M s

A DescriptiveComplexity.SOGameSpec is the game DescriptiveComplexity.GAME reads on assignments of a second-order block: four first-order sentences say which assignments the existential player owns, which win outright, which start the game, and which moves are legal – the transition seeing two copies of the block, as an DescriptiveComplexity.SOTCSpec does. Its expansion (DescriptiveComplexity.SOGameSpec.toExp) therefore takes Tag := Unit, no domain restriction, the block of the specification, and the vocabulary of AND/OR graphs, and its points are the states (DescriptiveComplexity.SOGameSpec.toExpEquiv).

Since DescriptiveComplexity.GAME is in DescriptiveComplexity.PTIME, this gives at once

• DescriptiveComplexity.SOGameDefinable.mem_EXPTIME: a second-order alternating game is in EXPTIME,

which read on the definitions is SO-GAME ⊆ SO(LFP) – the second-order shadow of GAME ∈ PTIME, exactly as DescriptiveComplexity.PSPACE_subset_EXPTIME is the second-order shadow of REACH ∈ PTIME.

What this is for

Writing a machine's configuration graph as an expansion by hand means writing its transition relation as a sentence over the base plus two copies of a block, and nothing else: this file takes care of everything that is not those four sentences. It is what an alternating space-bounded machine (DescriptiveComplexity.ATMAcceptSpace) consumes, its configurations being the assignments of a block with one variable for the state, one for the head and one for the tape.

The specification

structure DescriptiveComplexity.SOGameSpec (L : FirstOrder.Language) : Type 1

A second-order alternating game: the states of the game are the assignments of a block B, and four first-order sentences over the base vocabulary expanded by the order and by copies of the block say which states are universal, which win outright, which start the game, and which moves are legal. The move sentence sees two copies of the block – the current state and the next one – exactly as DescriptiveComplexity.SOTCSpec.step does.

The order is visible to all four sentences, as the ordered setting of the capture theorems allows; the problem itself does not see it.

• B : SOBlock

  The block whose assignments are the states of the game.

• move : (((L.sum FirstOrder.Language.order).sum self.B.lang).sum self.B.lang).Sentence

  The move sentence, over two copies of the block: the current state reads the first copy, the next state the second.

• univ : ((L.sum FirstOrder.Language.order).sum self.B.lang).Sentence

  The sentence defining the states of the universal player.

• won : ((L.sum FirstOrder.Language.order).sum self.B.lang).Sentence

  The sentence defining the states that win outright.

• start : ((L.sum FirstOrder.Language.order).sum self.B.lang).Sentence

  The sentence defining the starting states.

@[reducible, inline]

abbrev DescriptiveComplexity.SOGameSpec.State {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) : Type

A state of the game: an assignment of the block.

Equations

• spec.State A = spec.B.Assignment A

def DescriptiveComplexity.SOGameSpec.Move {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ σ : spec.State A) : Prop

A legal move: the move sentence, read with the current state in the first copy of the block and the next state in the second.

Equations

• spec.Move ρ σ = A ⊨ spec.move

def DescriptiveComplexity.SOGameSpec.IsUniv {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.State A) : Prop

A state belongs to the universal player.

Equations

• spec.IsUniv ρ = A ⊨ spec.univ

def DescriptiveComplexity.SOGameSpec.IsWon {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.State A) : Prop

A state wins outright.

Equations

• spec.IsWon ρ = A ⊨ spec.won

def DescriptiveComplexity.SOGameSpec.IsStart {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (ρ : spec.State A) : Prop

A state starts the game.

Equations

• spec.IsStart ρ = A ⊨ spec.start

inductive DescriptiveComplexity.SOGameSpec.Wins {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] : spec.State A → Prop

The winning states, as a least fixed point: a state that wins outright, an existential state with a winning move, or a universal state that has a move and all of whose moves are winning.

• won {L : FirstOrder.Language} {spec : SOGameSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ρ : spec.State A} : spec.IsWon ρ → spec.Wins ρ

  A state that wins outright.

• ex {L : FirstOrder.Language} {spec : SOGameSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ρ σ : spec.State A} : ¬spec.IsUniv ρ → spec.Move ρ σ → spec.Wins σ → spec.Wins ρ

  An existential state with a winning move.

• all {L : FirstOrder.Language} {spec : SOGameSpec L} {A : Type} [L.Structure A] [LinearOrder A] {ρ : spec.State A} : spec.IsUniv ρ → (∃ (σ : spec.State A), spec.Move ρ σ) → (∀ (σ : spec.State A), spec.Move ρ σ → spec.Wins σ) → spec.Wins ρ

  A universal state with a move, all of whose moves are winning.

def DescriptiveComplexity.SOGameSpec.Accepts {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) [L.Structure A] [LinearOrder A] : Prop

The structure is accepted: some starting state is winning.

Equations

• spec.Accepts A = ∃ (ρ : spec.State A), spec.IsStart ρ ∧ spec.Wins ρ

The expansion of a specification

def DescriptiveComplexity.SOGameSpec.toExp {L : FirstOrder.Language} (spec : SOGameSpec L) : ExpExpansion L

The expansion whose points are the states of the game: no tags, no domain restriction, and the four sentences of the specification defining the four symbols of the vocabulary of AND/OR graphs.

Equations

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

@[instance_reducible]

def DescriptiveComplexity.SOGameSpec.toExpStructure {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) [L.Structure A] [LinearOrder A] : FirstOrder.Language.andOrGraph.Structure (spec.toExp.Map A)

The expanded structure of DescriptiveComplexity.SOGameSpec.toExp, at the vocabulary of AND/OR graphs – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

Equations

• spec.toExpStructure A = spec.toExp.mapStructure A

theorem DescriptiveComplexity.SOGameSpec.domHolds_toExp {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) [L.Structure A] [LinearOrder A] (p : spec.toExp.Point A) : ExpExpansion.DomHolds p

The domain of DescriptiveComplexity.SOGameSpec.toExp is the whole space of tagged assignments: its domain sentence is ⊤.

def DescriptiveComplexity.SOGameSpec.toExpEquiv {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) [L.Structure A] [LinearOrder A] : spec.toExp.Map A ≃ spec.State A

The points of the expansion are the states of the game.

Equations

• spec.toExpEquiv A = { toFun := fun (x : spec.toExp.Map A) => (↑x).2, invFun := fun (ρ : spec.State A) => ⟨((), ρ), ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

The four symbols

theorem DescriptiveComplexity.SOGameSpec.agMove_toExp {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x y : spec.toExp.Map A) : AGMove x y ↔ spec.Move (↑x).2 (↑y).2

The move symbol is the move sentence.

theorem DescriptiveComplexity.SOGameSpec.agUniv_toExp {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : spec.toExp.Map A) : AGUniv x ↔ spec.IsUniv (↑x).2

The universal nodes are the universal states.

theorem DescriptiveComplexity.SOGameSpec.agWon_toExp {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : spec.toExp.Map A) : AGWon x ↔ spec.IsWon (↑x).2

The nodes that win outright are the states that do.

theorem DescriptiveComplexity.SOGameSpec.agStart_toExp {L : FirstOrder.Language} (spec : SOGameSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : spec.toExp.Map A) : AGStart x ↔ spec.IsStart (↑x).2

The marked starts are the starting states.

Winning is winning

theorem DescriptiveComplexity.SOGameSpec.gameWon_toExp_iff {L : FirstOrder.Language} (spec : SOGameSpec L) (A : Type) [L.Structure A] [LinearOrder A] : GameWon (spec.toExp.Map A) ↔ spec.Accepts A

The game accepts exactly when GAME holds of the expansion.

Definability, and the class

def DescriptiveComplexity.SOGameDefinable {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : Prop

SO-GAME definability: the problem is the value of a second-order alternating game, on nonempty finite ordered structures.

Equations

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

theorem DescriptiveComplexity.SOGameDefinable.expDefinable {L : FirstOrder.Language} [L.IsRelational] {C : ComplexityClass} (hgame : C.Mem GAME) {P : DecisionProblem L} (h : SOGameDefinable P) : ExpDefinable C P

A second-order alternating game is GAME over an expanded universe: the game is the AND/OR graph the expansion draws, so any class containing GAME contains the problem one exponential up.

theorem DescriptiveComplexity.SOGameDefinable.mem_EXPTIME {L : FirstOrder.Language} [L.IsRelational] {P : DecisionProblem L} (h : SOGameDefinable P) : EXPTIME.Mem P

A second-order alternating game is in EXPTIME. Read on the definitions this is SO-GAME ⊆ SO(LFP) – the second-order shadow of GAME ∈ PTIME, and the way into EXPTIME that needs no succinctness argument.