Documentation

DescriptiveComplexity.Problems.Wide.RegChannelExpansion

The register channel, as an expansion #

DescriptiveComplexity.WideAccept is in NEXPTIME because the wide machine of an instance is the ordinary machine of an exponential expansion of it (DescriptiveComplexity.Problems.Wide.Membership): twelve relation symbols, each defined by a sentence over one or two copies of the address block. The register channel changes exactly one of the twelve – the input – so this file adds the sentence it needs, the expansion it names, and the membership that follows.

The sentence is the segment channel's with one conjunct added: the segment channel says «the address holds z exactly when z ≤ x», the register channel says «exactly when z ≤ x and z carries an input symbol». Carrying one is itself first-order (hasInpG), so the expansion stays what it was, and the two expansions have the same tags, the same block and the same domain, hence the same universe.

The sentence the register channel needs #

source
noncomputable def DescriptiveComplexity.Wide.hasInpG {γ : Type} (x : γ) :
wOrd.Formula γ

An element the channel writes for, as a guard: it carries an input symbol.

Equations
Instances For
    Dependency graph
    source
    @[simp]
    theorem DescriptiveComplexity.Wide.realize_hasInpG {γ A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] {v : γ → A} (x : γ) :
    (hasInpG x).Realize v ↔ WMHasInp (v x)
    Dependency graph
    source
    noncomputable def DescriptiveComplexity.Wide.inpRegS :
    wide2.Sentence

    The initial tape at the register channel: the first address is the segment some element x cuts among the elements that carry input, the second point is a symbol y, and y is the input at x.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Dependency graph
      source
      theorem DescriptiveComplexity.Wide.realize_inpRegS {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (ρ σ : addrBlock.Assignment A) :
      A ⊨ inpRegS ↔ ∃ (x : A) (y : A), WMRegSeg (wbits ρ) x ∧ wbits σ y ∧ WMInp x y
      Dependency graph

      The expansion, and the structure it puts on the same universe #

      source
      noncomputable def DescriptiveComplexity.Wide.inpRegT :
      WTag → WTag → wide2.Sentence

      The initial tape of the register channel, at a pair of tags.

      Equations
      Instances For
        Dependency graph
        source
        noncomputable def DescriptiveComplexity.Wide.wideRegExp :
        ExpExpansion FirstOrder.Language.wide

        The expansion of a wide-machine instance at the register channel: the tags, the block, the domain and eleven of the twelve symbols are DescriptiveComplexity.wideExp's; the input is the register channel's.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          Dependency graph
          source
          @[instance_reducible]
          noncomputable def DescriptiveComplexity.Wide.wideRegStructure (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
          FirstOrder.Language.turing.Structure (wideExp.Map A)

          The expanded structure at the register channel. Its universe is wideExp's – the two expansions differ in one defining sentence and in nothing that decides the points.

          Equations
          Instances For
            Dependency graph
            source
            theorem DescriptiveComplexity.Wide.realize_twoReg {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (rt : FirstOrder.Language.turing.Relations 2) (φ : WTag → WTag → wide2.Sentence) (h : ∀ (τ : Fin 2 → wideRegExp.Tag), wideRegExp.relSentence rt τ = onS2 (φ (τ 0) (τ 1))) (x y : wideExp.Map A) :
            FirstOrder.Language.Structure.RelMap rt ![x, y] ↔ A ⊨ φ (↑x).1 (↑y).1

            Reading a binary symbol of the register-channel expansion at two points.

            Dependency graph
            source
            theorem DescriptiveComplexity.Wide.relMap_inpReg {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (p q : WPoint A) :
            FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmInp ![wideEmbed p, wideEmbed q] ↔ (wideRegData A).Inp p q

            The initial tape of the expanded machine at the register channel: the segment an element cuts among the elements that carry input holds that element's input symbol.

            Dependency graph
            source
            theorem DescriptiveComplexity.Wide.wideRegAgree (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
            TMData.Agree wideEquiv (wideRegData A) (tmData (wideExp.Map A))

            The wide machine at the register channel is the ordinary machine of the register-channel expansion, fieldwise: eleven of the twelve symbols are defined by the same sentences as wideExp's, so their readings are the same readings, and the twelfth is relMap_inpReg.

            Dependency graph

            The membership #

            source
            theorem DescriptiveComplexity.wideRegAccept_iff_expansion (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] :
            WideRegAccept.Holds A ↔ NTMAccept.Holds (Wide.wideExp.Map A)

            The register-channel machine is the ordinary machine of its expansion: acceptance of the one is acceptance of the other.

            Dependency graph
            source
            theorem DescriptiveComplexity.wideRegAccept_mem_NEXPTIME :
            NEXPTIME.Mem WideRegAccept

            The register-channel machine is in NEXPTIME, for the reason DescriptiveComplexity.wideAccept_mem_NEXPTIME gives: its expansion is an ordinary machine, and DescriptiveComplexity.NTMAccept is in NP. The two problems are therefore in the same class, and a reduction may choose whichever channel puts its input where it can reach it.

            Dependency graph