GAME: alternating reachability

The natural PTIME-complete problem the catalog was missing. An AND/OR graph is a directed graph whose nodes are split between two players, together with a set of nodes that win outright; a node is winning when

• it wins outright, or
• it belongs to the existential player and some successor is winning, or
• it belongs to the universal player, it has a successor, and every successor is winning.

DescriptiveComplexity.GAME asks whether some marked source is winning. Reading the three clauses with the universal player removed gives DescriptiveComplexity.REACH back, so this is alternating reachability in the same sense that DescriptiveComplexity.PSPACE is DescriptiveComplexity.NL with alternation: one operator more, one class up.

The stuck-universal convention

A universal node with no successor loses. The other convention – vacuous universal quantification, so that a stuck universal node wins – is equally standard; this one is chosen because it is the convention DescriptiveComplexity.ATMData.AltWin already uses, and matching them is what lets the alternating machine's configuration graph be read as an instance of this problem with nothing to adjust. A node that should win vacuously is marked as winning outright instead, which is what the reduction from HORN-SAT does with a clause that has no body.

Winning as an inductive predicate

DescriptiveComplexity.WinsOn is an inductive predicate, i.e., the least fixed point of the game operator, so an infinite play is a loss for the existential player. That is also the presentation the FO(LFP) membership proof mirrors clause by clause – with one twist, since a Horn rule cannot carry a universally quantified body atom; see DescriptiveComplexity.Problems.Game.Membership.

@[instance_reducible]

instance FirstOrder.Language.instDecidableEqAndOrGraphRel {a✝ : ℕ} : DecidableEq (andOrGraphRel a✝)

Equations

• FirstOrder.Language.instDecidableEqAndOrGraphRel = FirstOrder.Language.instDecidableEqAndOrGraphRel.decEq

@[reducible, inline]

abbrev FirstOrder.Language.agStart : Language.andOrGraph.Relations 1

start a: the node a is a marked starting position.

Equations

• FirstOrder.Language.agStart = FirstOrder.Language.andOrGraphRel.start

@[reducible, inline]

abbrev FirstOrder.Language.agUniv : Language.andOrGraph.Relations 1

univ a: the node a belongs to the universal player.

Equations

• FirstOrder.Language.agUniv = FirstOrder.Language.andOrGraphRel.univ

@[reducible, inline]

abbrev FirstOrder.Language.agWon : Language.andOrGraph.Relations 1

won a: the node a wins outright.

Equations

• FirstOrder.Language.agWon = FirstOrder.Language.andOrGraphRel.won

def FirstOrder.Language.instDecidableEqAndOrGraphRel.decEq {a✝ : ℕ} (x✝ x✝¹ : andOrGraphRel a✝) : Decidable (x✝ = x✝¹)

Equations

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

inductive FirstOrder.Language.andOrGraphRel : ℕ → Type

The relation symbols of the language.

• move : andOrGraphRel 2

  move a b: the player to move at a may move to b.

• univ : andOrGraphRel 1

  univ a: the node a belongs to the universal player.

• start : andOrGraphRel 1

  start a: the node a is a marked starting position.

• won : andOrGraphRel 1

  won a: the node a wins outright.

instance FirstOrder.Language.instIsRelationalAndOrGraph : Language.andOrGraph.IsRelational

@[reducible, inline]

abbrev FirstOrder.Language.agMove : Language.andOrGraph.Relations 2

move a b: the player to move at a may move to b.

Equations

• FirstOrder.Language.agMove = FirstOrder.Language.andOrGraphRel.move

def FirstOrder.Language.andOrGraph : Language

The relational vocabulary of AND/OR graphs: a move relation, a mark for the nodes of the universal player, a mark for the starting positions and a mark for the positions that win outright.

Equations

• FirstOrder.Language.andOrGraph = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.andOrGraphRel }

@[reducible, inline]

abbrev FirstOrder.Language.agMoveO : (Language.andOrGraph.sum Language.order).Relations 2

The move symbol in the ordered expansion.

Equations

• FirstOrder.Language.agMoveO = Sum.inl FirstOrder.Language.agMove

@[reducible, inline]

abbrev FirstOrder.Language.agUnivO : (Language.andOrGraph.sum Language.order).Relations 1

The universal-player symbol in the ordered expansion.

Equations

• FirstOrder.Language.agUnivO = Sum.inl FirstOrder.Language.agUniv

@[reducible, inline]

abbrev FirstOrder.Language.agStartO : (Language.andOrGraph.sum Language.order).Relations 1

The marked-start symbol in the ordered expansion.

Equations

• FirstOrder.Language.agStartO = Sum.inl FirstOrder.Language.agStart

@[reducible, inline]

abbrev FirstOrder.Language.agWonO : (Language.andOrGraph.sum Language.order).Relations 1

The won-outright symbol in the ordered expansion.

Equations

• FirstOrder.Language.agWonO = Sum.inl FirstOrder.Language.agWon

The semantics

def DescriptiveComplexity.AGWon {A : Type} [FirstOrder.Language.andOrGraph.Structure A] (a0 : A) : Prop

won a: the node a wins outright.

Equations

• DescriptiveComplexity.AGWon a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.agWon ![a0]

def DescriptiveComplexity.AGStart {A : Type} [FirstOrder.Language.andOrGraph.Structure A] (a0 : A) : Prop

start a: the node a is a marked starting position.

Equations

• DescriptiveComplexity.AGStart a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.agStart ![a0]

def DescriptiveComplexity.AGUniv {A : Type} [FirstOrder.Language.andOrGraph.Structure A] (a0 : A) : Prop

univ a: the node a belongs to the universal player.

Equations

• DescriptiveComplexity.AGUniv a0 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.agUniv ![a0]

def DescriptiveComplexity.AGMove {A : Type} [FirstOrder.Language.andOrGraph.Structure A] (a0 a1 : A) : Prop

move a b: the player to move at a may move to b.

Equations

• DescriptiveComplexity.AGMove a0 a1 = FirstOrder.Language.Structure.RelMap FirstOrder.Language.agMove ![a0, a1]

inductive DescriptiveComplexity.WinsOn (A : Type) [FirstOrder.Language.andOrGraph.Structure A] : A → Prop

The winning positions of an AND/OR graph, as a least fixed point: a position that wins outright, an existential position with a winning successor, or a universal position that has a successor and all of whose successors win.

• won {A : Type} [FirstOrder.Language.andOrGraph.Structure A] {a : A} : AGWon a → WinsOn A a

  A position that wins outright.

• ex {A : Type} [FirstOrder.Language.andOrGraph.Structure A] {a b : A} : ¬AGUniv a → AGMove a b → WinsOn A b → WinsOn A a

  An existential position with a winning successor.

• all {A : Type} [FirstOrder.Language.andOrGraph.Structure A] {a : A} : AGUniv a → (∃ (b : A), AGMove a b) → (∀ (b : A), AGMove a b → WinsOn A b) → WinsOn A a

  A universal position with a successor, all of whose successors win.

def DescriptiveComplexity.GameWon (A : Type) [FirstOrder.Language.andOrGraph.Structure A] : Prop

Some marked starting position is winning.

Equations

• DescriptiveComplexity.GameWon A = ∃ (s : A), DescriptiveComplexity.AGStart s ∧ DescriptiveComplexity.WinsOn A s

Without the universal player, the game is reachability

Isomorphism-invariance

theorem DescriptiveComplexity.gameWon_iso {A B : Type} [FirstOrder.Language.andOrGraph.Structure A] [FirstOrder.Language.andOrGraph.Structure B] (e : FirstOrder.Language.andOrGraph.Equiv A B) : GameWon A ↔ GameWon B

Being won is isomorphism-invariant.

def DescriptiveComplexity.GAME : DecisionProblem FirstOrder.Language.andOrGraph

GAME, alternating reachability: is some marked starting position of the AND/OR graph winning?

Equations

• DescriptiveComplexity.GAME = { Holds := fun (A : Type) (inst : FirstOrder.Language.andOrGraph.Structure A) => DescriptiveComplexity.GameWon A, iso_invariant := ⋯ }

@[simp]

theorem DescriptiveComplexity.game_holds_iff (A : Type) [FirstOrder.Language.andOrGraph.Structure A] : GAME.Holds A ↔ GameWon A