Documentation

DescriptiveComplexity.Exponential.GameState

The states of the graph game #

The game that carries DescriptiveComplexity.EXPTIME to SO-GAME has one block for everything: n rounds of the point block (DescriptiveComplexity.repMerged) extended by tag bits naming a phase. This file fixes the phases and says what a state is.

The phases #

DescriptiveComplexity.Ph has six families, and the whole design of the game is in the table:

phaseownerwhat its moves are
startPick tx∀prove AGStart x; and play from x
main tx∃claim AGWon x; or claim x is existential; or claim it is universal
exStep tx ty∀prove ¬AGUniv x; prove AGMove x y; and win from y
allCert tx ty∀prove AGUniv x; prove AGMove x y; and answer every y'
allStep tx ty∃refute AGMove x y; or win from y
pre s tx ty j polpolfill round n - j, or – at j = 0 – be decided by the kernel

Two of the six families are there for reasons that are easy to get wrong and expensive to discover late.

The claim phases (exStep, allCert) are universal with the proof and the play as sibling moves: claiming falsely loses on the proof branch, so the existential player is forced to tell the truth about AGUniv x.

The states #

A state is DescriptiveComplexity.ExpExpansion.stateAssign: a phase and one assignment per round. Rounds are not guarded to be points in general – the play rounds of a prefix range over all assignments, the guards living inside the kernel (DescriptiveComplexity.ExpExpansion.stepF) – but the rounds of every node-carrying phase are, which is what DescriptiveComplexity.ExpExpansion.allRoundsPointF asserts at the start and every node move preserves.

The phases #

source
inductive DescriptiveComplexity.Ph (T : Type) (Dm : ℕ) :
Type

The phases of the graph game: tx, ty are the tags of the two nodes the state carries, j the number of play rounds a prefix has left and pol the player whose turn it is there.

  • startPick {T : Type} {Dm : ℕ} (tx : T) : Ph T Dm

    A candidate start node has been chosen.

  • main {T : Type} {Dm : ℕ} (tx : T) : Ph T Dm

    The game is at the node x.

  • exStep {T : Type} {Dm : ℕ} (tx ty : T) : Ph T Dm

    The existential player claims x is his and moves to y.

  • allCert {T : Type} {Dm : ℕ} (tx ty : T) : Ph T Dm

    The existential player claims x is universal, with y as witness.

  • allStep {T : Type} {Dm : ℕ} (tx ty : T) : Ph T Dm

    The universal player has proposed the move to y.

  • pre {T : Type} {Dm : ℕ} (s : Sub) (tx ty : T) (j : Fin (Dm + 1)) (pol : Bool) : Ph T Dm

    A question is being decided, j play rounds left.

Instances For
    Dependency graph
    source
    def DescriptiveComplexity.instDecidableEqPh.decEq {T✝ : Type} {Dm✝ : ℕ} [DecidableEq T✝] (x✝ x✝¹ : Ph T✝ Dm✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.instDecidableEqPh {T✝ : Type} {Dm✝ : ℕ} [DecidableEq T✝] :
      DecidableEq (Ph T✝ Dm✝)
      Equations
      Dependency graph
      source
      instance DescriptiveComplexity.Ph.instFinite {T : Type} {Dm : ℕ} [Finite T] :
      Finite (Ph T Dm)
      Dependency graph
      source
      def DescriptiveComplexity.Ph.IsUniv {T : Type} {Dm : ℕ} :
      Ph T Dm → Prop

      Who owns a phase. The two claim phases and the start phase are universal, a prefix position is universal exactly when its polarity says so and it still has a round to fill, and everything else is existential.

      Equations
      Instances For
        Dependency graph
        source
        @[instance_reducible]
        instance DescriptiveComplexity.Ph.instDecidablePredIsUniv {T : Type} {Dm : ℕ} :
        DecidablePred IsUniv
        Equations
        • One or more equations did not get rendered due to their size.
        Dependency graph
        source
        @[reducible, inline]
        abbrev DescriptiveComplexity.ExpExpansion.gameBlock {L : FirstOrder.Language} (X : ExpExpansion L) (n : ℕ) (T : Type) [Finite T] (Dm : ℕ) :
        SOBlock

        The one block of the graph game: n rounds of the point block, extended by tag bits naming a phase.

        Equations
        Instances For
          Dependency graph
          source
          def DescriptiveComplexity.ExpExpansion.stateAssign {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {T : Type} [Finite T] {Dm : ℕ} {A : Type} (p : Ph T Dm) (ρs : Fin n → X.pointBlock.Assignment A) :
          (X.gameBlock n T Dm).Assignment A

          A state of the graph game: a phase, and one assignment per round.

          Equations
          Instances For
            Dependency graph
            source
            @[simp]
            theorem DescriptiveComplexity.ExpExpansion.dropTag_stateAssign {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {T : Type} [Finite T] {Dm : ℕ} {A : Type} (p : Ph T Dm) (ρs : Fin n → X.pointBlock.Assignment A) :
            SOBlock.dropTag (stateAssign p ρs) = repBlockAssign X.pointBlock A n ρs
            Dependency graph

            Every round holds a point #

            source
            noncomputable def DescriptiveComplexity.ExpExpansion.allRoundsPointF {L : FirstOrder.Language} (X : ExpExpansion L) (n : ℕ) :
            ((L.sum FirstOrder.Language.order).sum (repMerged X.pointBlock n).lang).Sentence

            Every round of the state holds a point of the expanded universe. True of a starting state and preserved by every move between node phases; the play rounds of a prefix are where it stops holding, and they are never read as parameters.

            Equations
            Instances For
              Dependency graph
              source
              theorem DescriptiveComplexity.ExpExpansion.realize_allRoundsPointF {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (ρs : Fin n → X.pointBlock.Assignment A) :
              A ⊨ X.allRoundsPointF n ↔ ∀ (i : Fin n), IsPointAssign (ρs i)
              Dependency graph
              source
              theorem DescriptiveComplexity.ExpExpansion.exists_points_of_allRoundsPoint {L : FirstOrder.Language} {X : ExpExpansion L} {n : ℕ} {A : Type} [L.Structure A] [LinearOrder A] {ρs : Fin n → X.pointBlock.Assignment A} (h : ∀ (i : Fin n), IsPointAssign (ρs i)) :
              ∃ (pts : Fin n → X.Map A), ρs = fun (i : Fin n) => pointAssign (pts i)

              A state all of whose rounds are points carries a tuple of points.

              Dependency graph