Generalized geography

DefinitionWinning positions in Geography#✓fully proved

Let \(E\) be a list of pairs of natural numbers, read as directed edges, let \(v\) be a natural number (the current vertex) and let \(V\) be a list of natural numbers (the visited vertices). For a natural number \(k\) (the fuel), the predicate \(\mathrm{GeoWins}(k, E, v, V)\) is defined by recursion on \(k\): \(\mathrm{GeoWins}(0, E, v, V)\) is false, and \(\mathrm{GeoWins}(k + 1, E, v, V)\) holds exactly when there is a natural number \(w\) with \((v, w) \in E\) and \(w \notin V\) such that \(\mathrm{GeoWins}(k, E, w, V')\) is false, where \(V'\) is the list \(V\) with \(w\) added at the front.

Read as a game, the player to move wins when they can move the token along an edge of \(E\) to a vertex not in \(V\) from which the opponent does not win; a player with no such move, or with no fuel left, loses.

def GeoWins : ℕ → List (ℕ × ℕ) → ℕ → List ℕ → Prop
  | 0, _, _, _ => False
  | fuel + 1, edges, pos, visited =>
    ∃ nxt, (pos, nxt) ∈ edges ∧ nxt ∉ visited ∧ ¬ GeoWins fuel edges nxt (nxt :: visited)

Used by 1

Used byGeography as a decision problem

DefinitionGeography as a decision problem#✓fully proved

The Geography decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding of triples \((n, E, s)\) of a natural number, a list of pairs of natural numbers and a natural number, to a triple with \(s < n\), with both entries of every pair in \(E\) less than \(n\), and with \(\mathrm{GeoWins}(n + 1, E, s, [s])\), where \([s]\) is the list whose only entry is \(s\). Bitstrings that do not decode are rejected.

A play never revisits one of the \(n\) vertices, so the fuel \(n + 1\) never runs out: the condition says that the player who moves first wins Geography on the directed graph with vertices \(0, \ldots, n - 1\) and edge list \(E\), with the token starting on \(s\) and \(s\) marked visited.

noncomputable def geographyDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × List (ℕ × ℕ) × ℕ) x with
  | some i => decide (i.2.2 < i.1 ∧
      (∀ e ∈ i.2.1, e.1 < i.1 ∧ e.2 < i.1) ∧
      GeoWins (i.1 + 1) i.2.1 i.2.2 [i.2.2])
  | none => false

Uses 10 · Used by 1

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Winning positions in Geography · Decision problems

Used byGeography is PSPACE-complete

TheoremGeography is PSPACE-complete#●ready to prove

The Geography decision problem belongs to PSPACE, and every decision problem in PSPACE has a polynomial-time many-one reduction to it.

public theorem_wanted geography_pspace_complete :
    geographyDec ∈ PSPACE ∧ ∀ L : MetaMathlibExt.ComplexityTheory.DecisionProblem,
      L ∈ PSPACE → Cslib.CookLevin.PolyManyOneRed L geographyDec

Sources

• T. J. Schaefer, "On the complexity of some two- person perfect-information games", Journal of Computer and System Sciences 16 (1978), 185-225.

Uses 5

Statement usesPolynomial space for decision problems · Polynomial-time many-one reduction · Geography as a decision problem · Complexity classes · Decision problems

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.