Documentation

DescriptiveComplexity.Exponential.Reach

An SO(TC) walk is reachability on an exponential expansion #

The construction that connects the exponential classes to the polynomial ones: an DescriptiveComplexity.SOTCSpec is the graph REACH reads on the expansion whose points are its states. Compare the two definitions, which are the same sentence up to the name of the universe:

SOTCSpec.Accepts A = ∃ ρ σ, spec.IsSrc ρ ∧ spec.IsTgt σ ∧ Relation.ReflTransGen spec.Step ρ σ
Reachable       M = ∃ s t, SGSource s   ∧ SGTarget t   ∧ Relation.ReflTransGen SGEdge     s t

So the expansion DescriptiveComplexity.SOTCSpec.toExp takes Tag := Unit, no domain restriction, the block of the specification, and the vocabulary of graphs with marked sources and targets, defining the edge symbol by the transition sentence and the two marks by the endpoint sentences. Its points are the states (DescriptiveComplexity.SOTCSpec.toExpEquiv) and REACH holds of it exactly when the walk accepts (DescriptiveComplexity.SOTCSpec.reachable_toExp_iff).

Since REACH is in every class from NL up, this gives at once

the inclusion that starts the tower above PSPACE. Read on the definitions the second one is SO(TC) ⊆ SO(LFP) – a transitive closure is a least fixed point – which is the second-order shadow of NL ⊆ PTIME.

The expansion of a specification #

source
def DescriptiveComplexity.SOTCSpec.toExp {L : FirstOrder.Language} (spec : SOTCSpec L) :
ExpExpansion L

The expansion whose points are the states of the walk: no tags, no domain restriction, and the three sentences of the specification defining the three symbols of the vocabulary of marked graphs.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Dependency graph
    source
    @[instance_reducible]
    def DescriptiveComplexity.SOTCSpec.toExpStructure {L : FirstOrder.Language} (spec : SOTCSpec L) (A : Type) [L.Structure A] [LinearOrder A] :
    FirstOrder.Language.stGraph.Structure (spec.toExp.Map A)

    The expanded structure of DescriptiveComplexity.SOTCSpec.toExp, at the vocabulary of marked graphs – equal to the expansion's own by definition, but not syntactically, so instance search has to be handed it.

    Equations
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.SOTCSpec.domHolds_toExp {L : FirstOrder.Language} (spec : SOTCSpec L) (A : Type) [L.Structure A] [LinearOrder A] (p : spec.toExp.Point A) :
      ExpExpansion.DomHolds p

      The domain of DescriptiveComplexity.SOTCSpec.toExp is the whole space of tagged assignments: its domain sentence is ⊤.

      Dependency graph
      source
      def DescriptiveComplexity.SOTCSpec.toExpEquiv {L : FirstOrder.Language} (spec : SOTCSpec L) (A : Type) [L.Structure A] [LinearOrder A] :
      spec.toExp.Map A ≃ spec.State A

      The points of the expansion are the states of the walk.

      Equations
      Instances For
        Dependency graph

        The three symbols #

        source
        theorem DescriptiveComplexity.SOTCSpec.sgEdge_toExp {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x y : spec.toExp.Map A) :
        SGEdge x y ↔ spec.Step (↑x).2 (↑y).2

        The edge symbol is the transition sentence.

        Dependency graph
        source
        theorem DescriptiveComplexity.SOTCSpec.sgSource_toExp {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : spec.toExp.Map A) :
        SGSource x ↔ spec.IsSrc (↑x).2

        The marked sources are the starting states.

        Dependency graph
        source
        theorem DescriptiveComplexity.SOTCSpec.sgTarget_toExp {L : FirstOrder.Language} (spec : SOTCSpec L) {A : Type} [L.Structure A] [LinearOrder A] (x : spec.toExp.Map A) :
        SGTarget x ↔ spec.IsTgt (↑x).2

        The marked targets are the accepting states.

        Dependency graph

        Acceptance is reachability #

        source
        theorem DescriptiveComplexity.SOTCSpec.reachable_toExp_iff {L : FirstOrder.Language} (spec : SOTCSpec L) (A : Type) [L.Structure A] [LinearOrder A] :
        Reachable (spec.toExp.Map A) ↔ spec.Accepts A

        The walk accepts exactly when REACH holds of the expansion.

        Dependency graph

        Polynomial space sits inside every exponential class above NL #

        source
        theorem DescriptiveComplexity.SOTCDefinable.expDefinable {L : FirstOrder.Language} [L.IsRelational] {C : ComplexityClass} (hreach : C.Mem REACH) {P : DecisionProblem L} (h : SOTCDefinable P) :
        ExpDefinable C P

        An SO(TC) definable problem is definable over an expanded universe by REACH: the walk is the graph the expansion draws, so any class containing REACH contains the problem one exponential up.

        Dependency graph
        source
        theorem DescriptiveComplexity.PSPACE_subset_NL_exp :
        PSPACE ⊆ NL.exp

        PSPACE ⊆ NL.exp: polynomial space is nondeterministic logarithmic space read one exponential up. This is the inclusion of the succinctness theorem at the level where the library independently knows the answer, and so the check that DescriptiveComplexity.ComplexityClass.exp computes the intended class.

        Dependency graph
        source
        theorem DescriptiveComplexity.PSPACE_subset_PTIME_exp :
        PSPACE ⊆ PTIME.exp

        PSPACE ⊆ PTIME.exp, i.e., PSPACE ⊆ EXPTIME once the class is named (DescriptiveComplexity.PSPACE_subset_EXPTIME). Read on the definitions it is SO(TC) ⊆ SO(LFP), the second-order shadow of NL ⊆ PTIME.

        Dependency graph