GAME is in PTIME

The membership half: DescriptiveComplexity.GAME is FO(LFP) definable (DescriptiveComplexity.game_lfpDefinable), hence in DescriptiveComplexity.PTIME by the Immerman–Vardi capture theorem the library already carries.

Why a second relation variable is needed

The winning set is a least fixed point, and two of its three clauses are Horn rules already. The third is not:

a universal node wins when it has a successor and every successor wins

has a universally quantified body, and a DescriptiveComplexity.HornClause carries a list of atoms, not a quantified one. The standard repair is to walk the order: a second variable allge x y – “every successor of x that is ≥ y wins” – is computed by a downward induction along the linear order, from the greatest element to the least, one immediate predecessor at a time (DescriptiveComplexity.order_induction_down). At the least element it says “every successor of x wins”, which is the body the third clause wanted.

That this stays a least fixed point is the point of doing it this way: allge is derivable exactly when the winners it quantifies over are already derived, so nothing is derived early and the two variables grow together.

@[reducible, inline]

abbrev DescriptiveComplexity.Game.agOrd : FirstOrder.Language

The ordered expansion of the vocabulary of AND/OR graphs.

Equations

• DescriptiveComplexity.Game.agOrd = FirstOrder.Language.andOrGraph.sum FirstOrder.Language.order

The block

inductive DescriptiveComplexity.Game.GIx : Type

The relation variables the fixed point computes.

• win : GIx

  win x: the node x is winning.

• allge : GIx

  allge x y: every successor of x that is at least y is winning.

@[instance_reducible]

instance DescriptiveComplexity.Game.instDecidableEqGIx : DecidableEq GIx

Equations

• DescriptiveComplexity.Game.instDecidableEqGIx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DescriptiveComplexity.Game.instFintypeGIx : Fintype GIx

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.Game.gameBlock : SOBlock

The block of the fixed point: the winning set, and the scan that collects a universal node's successors from the greatest element downwards.

Equations

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

def DescriptiveComplexity.Game.winAt (x : Fin 3) : SOAtom gameBlock 3

The atom win x.

Equations

• DescriptiveComplexity.Game.winAt x = { idx := DescriptiveComplexity.Game.GIx.win, args := fun (x_1 : Fin (DescriptiveComplexity.Game.gameBlock.arity DescriptiveComplexity.Game.GIx.win)) => x }

def DescriptiveComplexity.Game.allgeAt (x y : Fin 3) : SOAtom gameBlock 3

The atom allge x y.

Equations

• DescriptiveComplexity.Game.allgeAt x y = { idx := DescriptiveComplexity.Game.GIx.allge, args := ![x, y] }

The guards

noncomputable def DescriptiveComplexity.Game.wonG {α : Type} (x : α) : agOrd.Formula α

The node x wins outright, as a guard.

Equations

• DescriptiveComplexity.Game.wonG x = FirstOrder.Language.agWonO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Game.univG {α : Type} (x : α) : agOrd.Formula α

The node x belongs to the universal player, as a guard.

Equations

• DescriptiveComplexity.Game.univG x = FirstOrder.Language.agUnivO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Game.startG {α : Type} (x : α) : agOrd.Formula α

The node x is a marked start, as a guard.

Equations

• DescriptiveComplexity.Game.startG x = FirstOrder.Language.agStartO.formula₁ (FirstOrder.Language.var x)

noncomputable def DescriptiveComplexity.Game.moveG {α : Type} (x y : α) : agOrd.Formula α

There is a move from x to y, as a guard.

Equations

• DescriptiveComplexity.Game.moveG x y = FirstOrder.Language.agMoveO.formula₂ (FirstOrder.Language.var x) (FirstOrder.Language.var y)

@[simp]

theorem DescriptiveComplexity.Game.realize_wonG {α A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] {v : α → A} (x : α) : (wonG x).Realize v ↔ AGWon (v x)

@[simp]

theorem DescriptiveComplexity.Game.realize_univG {α A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] {v : α → A} (x : α) : (univG x).Realize v ↔ AGUniv (v x)

@[simp]

theorem DescriptiveComplexity.Game.realize_startG {α A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] {v : α → A} (x : α) : (startG x).Realize v ↔ AGStart (v x)

@[simp]

theorem DescriptiveComplexity.Game.realize_moveG {α A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] {v : α → A} (x y : α) : (moveG x y).Realize v ↔ AGMove (v x) (v y)

The rules

noncomputable def DescriptiveComplexity.Game.rWon : HornClause agOrd gameBlock 3

A node that wins outright is winning.

Equations

• DescriptiveComplexity.Game.rWon = { guard := DescriptiveComplexity.Game.wonG 0, body := [], head := some (DescriptiveComplexity.Game.winAt 0) }

noncomputable def DescriptiveComplexity.Game.rEx : HornClause agOrd gameBlock 3

An existential node with a winning successor is winning.

Equations

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

noncomputable def DescriptiveComplexity.Game.rAll : HornClause agOrd gameBlock 3

A universal node with a successor, all of whose successors are winning, is winning: the scan has reached the least element.

Equations

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

noncomputable def DescriptiveComplexity.Game.rTopNo : HornClause agOrd gameBlock 3

The scan starts at the greatest element, which is not a successor.

Equations

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

noncomputable def DescriptiveComplexity.Game.rTopYes : HornClause agOrd gameBlock 3

The scan starts at the greatest element, which is a winning successor.

Equations

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

noncomputable def DescriptiveComplexity.Game.rStepNo : HornClause agOrd gameBlock 3

The scan steps down past an element that is not a successor.

Equations

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

noncomputable def DescriptiveComplexity.Game.rStepYes : HornClause agOrd gameBlock 3

The scan steps down past a winning successor.

Equations

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

noncomputable def DescriptiveComplexity.Game.gameRules : List (HornClause agOrd gameBlock 3)

The rules of the definition.

Equations

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

theorem DescriptiveComplexity.Game.rWon_mem : rWon ∈ gameRules

theorem DescriptiveComplexity.Game.rEx_mem : rEx ∈ gameRules

theorem DescriptiveComplexity.Game.rAll_mem : rAll ∈ gameRules

theorem DescriptiveComplexity.Game.rTopNo_mem : rTopNo ∈ gameRules

theorem DescriptiveComplexity.Game.rTopYes_mem : rTopYes ∈ gameRules

theorem DescriptiveComplexity.Game.rStepNo_mem : rStepNo ∈ gameRules

theorem DescriptiveComplexity.Game.rStepYes_mem : rStepYes ∈ gameRules

The output

noncomputable def DescriptiveComplexity.Game.gameOut : (agOrd.sum gameBlock.lang).Sentence

The output: some marked start is winning.

Equations

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

The intended fixed point

def DescriptiveComplexity.Game.gameAssign (A : Type) [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] : gameBlock.Assignment A

The assignment the rules are meant to compute.

Equations

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

theorem DescriptiveComplexity.Game.gameAssign_closed {A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] (c : HornClause agOrd gameBlock 3) : c ∈ gameRules → ∀ (a : SOAtom gameBlock 3), c.head = some a → ∀ (v : Fin 3 → A), c.guard.Realize v → (∀ b ∈ c.body, b.Holds (gameAssign A) v) → a.Holds (gameAssign A) v

The intended assignment is closed under the rules, so the least fixed point is contained in it.

theorem DescriptiveComplexity.Game.winsOn_of_derives {A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] {t : Fin (gameBlock.arity GIx.win) → A} (h : Derives gameRules ⟨GIx.win, t⟩) : WinsOn A (t 0)

Soundness: everything the rules derive about win is winning.

Completeness: every winning node is derived

theorem DescriptiveComplexity.Game.allgeArgs₁ {A : Type} (x y w : A) : (fun (j : Fin (gameBlock.arity (allgeAt 0 1).idx)) => ![x, y, w] ((allgeAt 0 1).args j)) = ![x, y]

The arguments of allge x y read out of the three variables.

theorem DescriptiveComplexity.Game.allgeArgs₂ {A : Type} (x y w : A) : (fun (j : Fin (gameBlock.arity (allgeAt 0 2).idx)) => ![x, y, w] ((allgeAt 0 2).args j)) = ![x, w]

The arguments of allge x z read out of the three variables.

theorem DescriptiveComplexity.Game.derives_allge {A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] [Finite A] {x : A} (hw : ∀ (b : A), AGMove x b → Derives gameRules ⟨GIx.win, fun (x : Fin (gameBlock.arity GIx.win)) => b⟩) (y : A) : Derives gameRules ⟨GIx.allge, ![x, y]⟩

The scan is derivable at every element, by a downward induction along the order: this is the universal body the third rule needs.

theorem DescriptiveComplexity.Game.derives_of_winsOn {A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] [Finite A] [Nonempty A] {x : A} (h : WinsOn A x) : Derives gameRules ⟨GIx.win, fun (x_1 : Fin (gameBlock.arity GIx.win)) => x⟩

Completeness: every winning node is derived.

theorem DescriptiveComplexity.Game.realize_gameOut {A : Type} [FirstOrder.Language.andOrGraph.Structure A] [LinearOrder A] (ρ : gameBlock.Assignment A) : A ⊨ gameOut ↔ ∃ (s : A), (ρ GIx.win fun (x : Fin (gameBlock.arity GIx.win)) => s) ∧ AGStart s

Reading the output: some marked start is in the fixed point.

theorem DescriptiveComplexity.game_lfpDefinable : LFPDefinable GAME

GAME is FO(LFP) definable: the winning set is the least fixed point of the three clauses, the universal one carried by a scan of the order.

theorem DescriptiveComplexity.game_mem_PTIME : PTIME.Mem GAME

GAME is in PTIME, through the formalized translation of FO(LFP) into the Horn fragment.