Documentation

DescriptiveComplexity.Problems.Game.Membership

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.

source
@[reducible, inline]
abbrev DescriptiveComplexity.Game.agOrd :
FirstOrder.Language

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

Equations
Instances For
    Dependency graph

    The block #

    source
    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.

    Instances For
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.Game.instDecidableEqGIx :
      DecidableEq GIx
      Equations
      Dependency graph
      source
      @[instance_reducible]
      instance DescriptiveComplexity.Game.instFintypeGIx :
      Fintype GIx
      Equations
      • One or more equations did not get rendered due to their size.
      Dependency graph
      source
      @[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.
      Instances For
        Dependency graph

        The guards #

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

        The node x wins outright, as a guard.

        Equations
        Instances For
          Dependency graph
          source
          noncomputable def DescriptiveComplexity.Game.univG {α : Type} (x : α) :
          agOrd.Formula α

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

          Equations
          Instances For
            Dependency graph
            source
            noncomputable def DescriptiveComplexity.Game.startG {α : Type} (x : α) :
            agOrd.Formula α

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

            Equations
            Instances For
              Dependency graph
              source
              noncomputable def DescriptiveComplexity.Game.moveG {α : Type} (x y : α) :
              agOrd.Formula α

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

              Equations
              Instances For
                Dependency graph
                source
                @[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)
                Dependency graph
                source
                @[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)
                Dependency graph
                source
                @[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)
                Dependency graph
                source
                @[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)
                Dependency graph

                The rules #

                The output #

                The intended fixed point #

                Completeness: every winning node is derived #

                source
                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.

                Dependency graph
                source
                theorem DescriptiveComplexity.game_mem_PTIME :
                PTIME.Mem GAME

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

                Dependency graph