The graph game, as a second-order alternating game

The four sentences of DescriptiveComplexity.ExpExpansion.graphGame, and what each of them says. Every one is a static disjunction over the phase type, which is finite: the phases carry the tags of the two nodes a state holds, so naming a tag costs a disjunct rather than a quantifier.

• univ – the phases DescriptiveComplexity.Ph.IsUniv selects, and nothing else;
• won – a leaf pre s tx ty 0 pol, conjoined with that question's kernel. The leaf is existential and has no move, so a false kernel loses: a player who asked for a proof he cannot give is stuck there;
• start – a startPick phase whose rounds all hold points (DescriptiveComplexity.ExpExpansion.allRoundsPointF), which is the invariant every node move preserves and every prefix consumes;
• move – one disjunct per pair of a phase and one of the moves DescriptiveComplexity.ExpExpansion.movesFrom allows out of it. A move names its target phase exactly (DescriptiveComplexity.atTagTwoF, so no junk state is reachable), lists the rounds it carries over – kept, shifted, or neither – and lists the rounds of the state it enters that it guards to be points.

The one asymmetry worth naming: the move that fills a play round guards nothing. DescriptiveComplexity.altBlockQuant ranges over all assignments and the point guards of a prefix live inside its kernel (DescriptiveComplexity.ExpExpansion.stepF), so guarding there would count them twice and break the correspondence with DescriptiveComplexity.ExpExpansion.exists_paramKernel.

The rounds a move carries over

def DescriptiveComplexity.keepAll (n : ℕ) : List (Fin n × Fin n)

Carry over every round: the move freezes the state.

Equations

• DescriptiveComplexity.keepAll n = List.map (fun (i : Fin n) => (i, i)) (List.finRange n)

def DescriptiveComplexity.keepOff (n : ℕ) (S : Fin n → Bool) : List (Fin n × Fin n)

Carry over every round outside S, in place.

Equations

• DescriptiveComplexity.keepOff n S = List.map (fun (i : Fin n) => (i, i)) (List.filter (fun (i : Fin n) => !S i) (List.finRange n))

def DescriptiveComplexity.isMid (d n : ℕ) : Fin n → Bool

The rounds holding the second node's points.

Equations

• DescriptiveComplexity.isMid d n i = decide (d ≤ ↑i ∧ ↑i < 2 * d)

def DescriptiveComplexity.midRounds (d n : ℕ) : List (Fin n)

The rounds holding the second node's points, as a list.

Equations

• DescriptiveComplexity.midRounds d n = List.filter (DescriptiveComplexity.isMid d n) (List.finRange n)

def DescriptiveComplexity.shiftIx (d n : ℕ) (h : 2 * d ≤ n) (i : Fin n) : Fin n

Where round i of the state a shifting move enters reads from: the second node's points become the first node's.

Equations

• DescriptiveComplexity.shiftIx d n h i = if hi : ↑i < d then ⟨↑i + d, ⋯⟩ else i

def DescriptiveComplexity.keepShift (d n : ℕ) (h : 2 * d ≤ n) : List (Fin n × Fin n)

Carry the second node's points onto the first node's slots.

Equations

• DescriptiveComplexity.keepShift d n h = List.map (fun (i : Fin n) => (DescriptiveComplexity.shiftIx d n h i, i)) (List.finRange n)

The moves out of a phase

structure DescriptiveComplexity.MoveTo (T : Type) (Dm n : ℕ) : Type

A move of the graph game, seen from the phase it leaves: where it goes, which rounds it carries over – as pairs (round of the state left, round of the state entered) – and which rounds of the state entered it guards to hold a point.

• tgt : Ph T Dm

  The phase the move enters.

• keep : List (Fin n × Fin n)

  The rounds it carries over.

• guard : List (Fin n)

  The rounds of the state it enters that it guards to hold a point.

def DescriptiveComplexity.ExpExpansion.preEntry {T : Type} {n Dm : ℕ} (D : Sub → T → T → ℕ) (hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm) (s : Sub) (tx ty : T) : MoveTo T Dm n

Entering the prefix that decides the question s about the nodes tagged tx, ty: nothing moves, and all D s tx ty play rounds are still to fill.

Equations

• DescriptiveComplexity.ExpExpansion.preEntry D hD s tx ty = { tgt := DescriptiveComplexity.Ph.pre s tx ty ⟨D s tx ty, ⋯⟩ true, keep := DescriptiveComplexity.keepAll n, guard := [] }

noncomputable def DescriptiveComplexity.ExpExpansion.movesFrom {T : Type} [Finite T] {d n Dm : ℕ} (hn : n = 2 * d + Dm) (D : Sub → T → T → ℕ) (hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm) : Ph T Dm → List (MoveTo T Dm n)

The moves out of each phase. This is the game.

Equations

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

The four sentences

noncomputable def DescriptiveComplexity.ExpExpansion.moveOf {L : FirstOrder.Language} (X : ExpExpansion L) {T : Type} [Finite T] {n Dm : ℕ} (p : Ph T Dm) (m : MoveTo T Dm n) : (((L.sum FirstOrder.Language.order).sum (X.gameBlock n T Dm).lang).sum (X.gameBlock n T Dm).lang).Sentence

The sentence of one move: it names the phase it leaves and the phase it enters, carries its rounds over, and guards the rounds it says are points.

Equations

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

noncomputable def DescriptiveComplexity.ExpExpansion.graphGame {L : FirstOrder.Language} (X : ExpExpansion L) {T : Type} [Finite T] {d n Dm : ℕ} (hn : n = 2 * d + Dm) (D : Sub → T → T → ℕ) (hD : ∀ (s : Sub) (tx ty : T), D s tx ty ≤ Dm) (K : Sub → T → T → ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence) : SOGameSpec L

The graph game: the game whose positions are the nodes of the AND/OR graph an interpretation draws on the expanded universe, together with the prefix positions that decide the six questions about them.

Equations

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

What the four sentences say

@[instance_reducible]

noncomputable def DescriptiveComplexity.ExpExpansion.stateStructure {L : FirstOrder.Language} {X : ExpExpansion L} {T : Type} [Finite T] {n Dm : ℕ} {A : Type} [instL : L.Structure A] [LinearOrder A] (σ : (X.gameBlock n T Dm).Assignment A) : ((L.sum FirstOrder.Language.order).sum (X.gameBlock n T Dm).lang).Structure A

The one-copy structure a state of the graph game is read against.

Equations

• DescriptiveComplexity.ExpExpansion.stateStructure σ = (X.gameBlock n T Dm).structure₁ σ