Documentation

DescriptiveComplexity.Problems.MachineAltSpace.Membership

Alternating acceptance in bounded space is in EXPTIME #

The third layer, and the theorem: DescriptiveComplexity.ATMAcceptSpace is a DescriptiveComplexity.SOGameSpec, so it is in EXPTIME (DescriptiveComplexity.atmAcceptSpace_mem_EXPTIME) – EXPTIME's first natural problem, and one that needs no succinctness argument.

The correspondence is a bisimulation between two inductive predicates of the same shape: DescriptiveComplexity.SOGameSpec.Wins on assignments of the configuration block and DescriptiveComplexity.ATMData.AltWin on configurations. It needs exactly two lemmas beyond the four realization ones – a move lands on a configuration and a start is a configuration – so junk assignments, which the block has plenty of, are never reached and never have to be reasoned about.

Where the promises go: DescriptiveComplexity.ExpDefinable compares P A with Q (X.Map A), and DescriptiveComplexity.TMData.WellFormed and DescriptiveComplexity.ATMData.BlocksSplit are conditions on A alone, so they ride on the start sentence – a game with no starting state is lost, which is what a failed promise should mean.

source
noncomputable def DescriptiveComplexity.ATMSpace.atmSpec :
SOGameSpec (FirstOrder.Language.turingAlt 2)

The alternating machine, as a second-order game: its states are the assignments of the configuration block, its moves are the machine's steps, the universal player owns the states marked by the second block, an accepting state wins outright, and the starting states are the initial configurations of a well-formed machine whose marks split.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    theorem DescriptiveComplexity.ATMSpace.move_cfgOf {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c c' : Config A) :
    atmSpec.Move (cfgOf c) (cfgOf c') ↔ (atmData 2 A).Step c c'

    A move is a step, between configurations.

    Dependency graph
    source
    theorem DescriptiveComplexity.ATMSpace.move_isCfg {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] {ρ σ : atmSpec.State A} (h : atmSpec.Move ρ σ) :
    ∃ (c' : Config A), σ = cfgOf c'

    A move lands on a configuration: the move sentence says so outright, which is what keeps the walk out of the junk assignments.

    Dependency graph
    source
    theorem DescriptiveComplexity.ATMSpace.isUniv_cfgOf {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (hsplit : (atmData 2 A).BlocksSplit) (c : Config A) :
    atmSpec.IsUniv (cfgOf c) ↔ (atmData 2 A).IsUniv true c.state

    The universal states are the ones the second mark owns.

    Dependency graph
    source
    theorem DescriptiveComplexity.ATMSpace.isWon_cfgOf {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (c : Config A) :
    atmSpec.IsWon (cfgOf c) ↔ (atmData 2 A).Acc c.state

    The states that win outright are the accepting ones.

    Dependency graph
    source
    theorem DescriptiveComplexity.ATMSpace.isStart_iff {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (ρ : atmSpec.State A) :
    atmSpec.IsStart ρ ↔ (atmData 2 A).WellFormed ∧ (atmData 2 A).BlocksSplit ∧ ∃ (c : Config A), ρ = cfgOf c ∧ (atmData 2 A).IsInit c

    The starting states are the initial configurations, of a machine whose two promises hold.

    Dependency graph

    The bisimulation #

    source
    def DescriptiveComplexity.ATMSpace.WinsCfg {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] (ρ : atmSpec.State A) :
    Prop

    What winning says about the configuration an assignment is.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.ATMSpace.altWin_of_wins {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (hsplit : (atmData 2 A).BlocksSplit) {ρ : atmSpec.State A} (h : atmSpec.Wins ρ) :
      WinsCfg ρ

      Winning the game is winning the machine's game.

      Dependency graph
      source
      theorem DescriptiveComplexity.ATMSpace.wins_of_altWin {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] (hsplit : (atmData 2 A).BlocksSplit) {c : Config A} (h : (atmData 2 A).AltWin true c) :
      atmSpec.Wins (cfgOf c)

      Winning the machine's game is winning the game.

      Dependency graph
      source
      theorem DescriptiveComplexity.ATMSpace.accepts_atmSpec {A : Type} [(FirstOrder.Language.turingAlt 2).Structure A] [LinearOrder A] :
      atmSpec.Accepts A ↔ ATMAcceptSpace.Holds A

      The game accepts exactly when the machine does.

      Dependency graph
      source
      theorem DescriptiveComplexity.atmAcceptSpace_soGameDefinable :
      SOGameDefinable ATMAcceptSpace

      Alternating acceptance in bounded space is a second-order game.

      Dependency graph
      source
      theorem DescriptiveComplexity.atmAcceptSpace_mem_EXPTIME :
      EXPTIME.Mem ATMAcceptSpace

      Alternating acceptance in bounded space is in EXPTIME (APSPACE ⊆ EXPTIME, half of Chandra–Kozen–Stockmeyer 1981): the game on the configuration graph is DescriptiveComplexity.GAME read over the expansion whose points are the configurations, and GAME is in DescriptiveComplexity.PTIME.

      This is EXPTIME's first natural problem, and it needs no succinctness argument: the expansion is applied after the problem, which is the composition that exists. The other half – the Chandra–Kozen–Stockmeyer simulation – is DescriptiveComplexity.atmAcceptSpace_EXPTIME_hard, whence DescriptiveComplexity.atmAcceptSpace_EXPTIME_complete.

      Dependency graph