Documentation

DescriptiveComplexity.Exponential.GamePlay

The machine plays the game #

The forward simulation: a winning state of an SOGameSpec is a winning configuration of the machine. Everything it is made of is already proved – a question holding wins from the entry of its prefix (DescriptiveComplexity.GameProg.altWin_ask), an existential sweep writes what its owner chooses and a universal one is answered for every assignment (DescriptiveComplexity.altWin_sweep_ex, DescriptiveComplexity.altWin_sweep_all) – so what is left is the control graph, one clause of DescriptiveComplexity.SOGameSpec.Wins at a time.

The invariant #

DescriptiveComplexity.PlayCfg says the tape's region r holds the current position and the machine is at play for that region. The candidate region is junk: nothing reads it before it is swept.

That is where the roles swapping pays. play at !r re-enters the same invariant with the regions exchanged, so a move of the game costs one sweep and nothing is ever copied.

The three clauses #

Wins.won  ρ  ⟶  ∃ picks `verify won`
Wins.ex   ρ σ ⟶  ∃ picks splitEx: ∀ { verify ¬univ ; sweep σ ; ∀ { verify move ; play σ } }
Wins.all  ρ   ⟶  ∃ picks splitAll: ∀ { verify univ
                                     ; sweep a witness ; verify move
                                     ; ∀-sweep ; ∃ { verify ¬move ; play } }

The last line is the one that needed the machinery: the universal sweep hands an arbitrary candidate to allStep, where the existential player either refutes the move – no sentence over the base could have filtered it out earlier – or plays on, which is the induction hypothesis.

source
def DescriptiveComplexity.PlayCfg {L : FirstOrder.Language} (spec : SOGameSpec L) {V M : ℕ} {A : Type} [L.Structure A] [LinearOrder A] (a₀ : A) (hdim : blockArityBound spec.B ≤ gameDim spec.B V) (prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M) (ρ : spec.State A) (r par : Bool) (c : Config (GamePt spec.B V M A)) :
Prop

The machine sits at a position of the game: the tape's region r holds that position, and the control is at play for that region.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.not_true_of_eq_false {b : Bool} (h : b = false) :
    ¬b = true
    Dependency graph

    The three clauses of Wins #

    The play #

    source
    theorem DescriptiveComplexity.altWin_play {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) {ρ : spec.State A} (hw : spec.Wins ρ) (r par : Bool) (c : Config (GamePt spec.B V M A)) :
    PlayCfg spec a₀ hdim prog ρ r par c → (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltWin true c

    A winning state of the game is a winning configuration of the machine. By induction on DescriptiveComplexity.SOGameSpec.Wins, one clause per lemma above.

    Dependency graph

    The entry #

    source
    theorem DescriptiveComplexity.altAcceptsSpace_of_accepts {L : FirstOrder.Language} {spec : SOGameSpec L} {V M : ℕ} {prog : GameProg (L.sum FirstOrder.Language.order) spec.B V M} {A : Type} [L.Structure A] [LinearOrder A] [Finite A] {a₀ : A} {hdim : blockArityBound spec.B ≤ gameDim spec.B V} (h₀ : IsBot a₀) (hplays : ∀ (q : GameQuestion), (prog.data q).Plays (spec.question q)) (hacc : spec.Accepts A) :
    (gameMachine prog.vars prog.pol a₀ hdim (gameRule prog.vars prog.natoms prog.concOk prog.isTarget)).AltAcceptsSpace true

    The machine accepts when the game does. The initial tape is empty – Inp is total on the positions, which is what makes it functional – so the starting position is guessed, by the very first sweep; the split that follows checks it starts the game, and plays it.

    Dependency graph