Documentation

DescriptiveComplexity.Problems.Wide.Membership

The wide machines are members of the exponential classes #

The payoff of DescriptiveComplexity.Problems.Wide.Expansion: the expansion's points are the universe of the wide machine (DescriptiveComplexity.Wide.wideEquiv), so the machine an instance describes and the machine the expanded structure describes agree fieldwise (DescriptiveComplexity.Wide.wideAgree) and the three wide problems are exactly the three ordinary machine problems read over the expansion. With DescriptiveComplexity.ntmAccept_mem_NP and DescriptiveComplexity.ntmAcceptSpace_mem_PSPACE that gives

No resource argument appears anywhere: the exponent is in the universe the machine runs over, and everything else is the composition that DescriptiveComplexity.ExpDefinable is made of – an expansion applied after the problem, which is the composition that exists.

source
noncomputable def DescriptiveComplexity.Wide.wideEmbed {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
WPoint A → wideExp.Map A

The universe of the wide machine sits inside the expansion: an address becomes the point tagged addr carrying it, a control element the point tagged ctrl carrying its singleton. It is the address expansion's own embedding (DescriptiveComplexity.AddrExp.addrEmbed), at this expansion.

Equations
Instances For
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.Wide.wideEquiv {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
    WPoint A ≃ wideExp.Map A

    The points of the expansion are the universe of the wide machine.

    Equations
    Instances For
      Dependency graph
      source
      @[simp]
      theorem DescriptiveComplexity.Wide.wideEquiv_apply {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (p : WPoint A) :
      wideEquiv p = wideEmbed p
      Dependency graph
      source
      @[simp]
      theorem DescriptiveComplexity.Wide.wideEmbed_addr_tag {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (s : A → Prop) :
      (↑(wideEmbed (Sum.inl s))).1 = AddrExp.WTag.addr
      Dependency graph
      source
      @[simp]
      theorem DescriptiveComplexity.Wide.wideEmbed_ctrl_tag {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (x : A) :
      (↑(wideEmbed (Sum.inr x))).1 = AddrExp.WTag.ctrl
      Dependency graph

      The twelve symbols #

      Each defining sentence is read at the points the embedding produces, and turns out to be the corresponding field of DescriptiveComplexity.wideData. The two generic lemmas do the bookkeeping – the tag match and the passage from the replicated block to one or two stacked copies – once for all.

      The two machines agree #

      source
      theorem DescriptiveComplexity.Wide.wideAgree (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
      TMData.Agree wideEquiv (wideData A) (tmData (wideExp.Map A))

      The wide machine of the instance is the ordinary machine of the expansion, fieldwise along DescriptiveComplexity.Wide.wideEquiv.

      Dependency graph

      The memberships #

      source
      theorem DescriptiveComplexity.wideAccept_mem_NEXPTIME :
      NEXPTIME.Mem WideAccept

      The wide machine is in NEXPTIME, which is NP.exp: the expansion turns it into DescriptiveComplexity.NTMAccept, and that problem is in NP. This is the first natural member the class has. Registered in the Lax archive as Lax822549.WideMachinesComplete.wideAccept_mem_NEXPTIME.

      Dependency graph
      source
      theorem DescriptiveComplexity.wideAcceptSpace_mem_EXPSPACE :
      EXPSPACE.Mem WideAcceptSpace

      The space-bounded wide machine is in EXPSPACE: the expansion turns it into DescriptiveComplexity.NTMAcceptSpace, and that problem is in PSPACE.

      Dependency graph
      source
      theorem DescriptiveComplexity.dwideAcceptSpace_mem_EXPSPACE :
      EXPSPACE.Mem DWideAcceptSpace

      The deterministic space-bounded wide machine is in EXPSPACE, through DescriptiveComplexity.DTMAcceptSpace.

      Dependency graph