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

• DescriptiveComplexity.wideAccept_mem_NEXPTIME – NEXPTIME := NP.exp, so this is the definition being exercised;
• DescriptiveComplexity.wideAcceptSpace_mem_EXPSPACE and its deterministic variant, through DescriptiveComplexity.EXPSPACE_eq_PSPACE_exp.

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.

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

• DescriptiveComplexity.Wide.wideEmbed = DescriptiveComplexity.AddrExp.addrEmbed

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

• DescriptiveComplexity.Wide.wideEquiv = DescriptiveComplexity.AddrExp.addrEquiv

@[simp]

theorem DescriptiveComplexity.Wide.wideEquiv_apply {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (p : WPoint A) : wideEquiv p = wideEmbed p

@[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

@[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

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.

theorem DescriptiveComplexity.Wide.realize_one {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (rt : FirstOrder.Language.turing.Relations 1) (φ : WTag → wide1.Sentence) (h : ∀ (τ : Fin 1 → wideExp.Tag), wideExp.relSentence rt τ = onS1 (φ (τ 0))) (x : wideExp.Map A) : FirstOrder.Language.Structure.RelMap rt ![x] ↔ A ⊨ φ (↑x).1

Reading a unary symbol of the expanded vocabulary at one point: the address expansion's own reading (DescriptiveComplexity.AddrExp.realize_one), at this expansion.

theorem DescriptiveComplexity.Wide.realize_two {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (rt : FirstOrder.Language.turing.Relations 2) (φ : WTag → WTag → wide2.Sentence) (h : ∀ (τ : Fin 2 → wideExp.Tag), wideExp.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 expanded vocabulary at two points.

theorem DescriptiveComplexity.Wide.relMap_posn {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (p : WPoint A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmPosn ![wideEmbed p] ↔ (wideData A).Posn p

The positions of the expanded machine are the addresses.

theorem DescriptiveComplexity.Wide.relMap_mark {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (rt : FirstOrder.Language.turing.Relations 1) (r : FirstOrder.Language.wide.Relations 1) (h : ∀ (τ : Fin 1 → wideExp.Tag), wideExp.relSentence rt τ = onS1 (markT r (τ 0))) (p : WPoint A) : FirstOrder.Language.Structure.RelMap rt ![wideEmbed p] ↔ wpMark (fun (x : A) => FirstOrder.Language.Structure.RelMap r ![x]) p

A mark of the expanded machine is the corresponding mark of the instance, carried by the control elements alone.

theorem DescriptiveComplexity.Wide.relMap_attr {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (rt : FirstOrder.Language.turing.Relations 2) (r : FirstOrder.Language.wide.Relations 2) (h : ∀ (τ : Fin 2 → wideExp.Tag), wideExp.relSentence rt τ = onS2 (binT r (τ 0) (τ 1))) (p q : WPoint A) : FirstOrder.Language.Structure.RelMap rt ![wideEmbed p, wideEmbed q] ↔ wpAttr (fun (x y : A) => FirstOrder.Language.Structure.RelMap r ![x, y]) p q

A binary attribute of the expanded machine is the corresponding attribute of the instance, holding of control elements alone.

theorem DescriptiveComplexity.Wide.relMap_le {A : Type} [FirstOrder.Language.wide.Structure A] [LinearOrder A] (p q : WPoint A) : FirstOrder.Language.Structure.RelMap FirstOrder.Language.tmLe ![wideEmbed p, wideEmbed q] ↔ (wideData A).Le p q

The order of the expanded machine: addresses in the binary-number order the instance's own order induces, then the control elements in that order.

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

The initial tape of the expanded machine: the address cutting the initial segment of an element holds that element's input symbol.

The two machines agree

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.

The memberships

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

The wide machine is the ordinary machine of the expansion: acceptance of the one is acceptance of the other.

theorem DescriptiveComplexity.wideAcceptSpace_iff_expansion (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] : WideAcceptSpace.Holds A ↔ NTMAcceptSpace.Holds (Wide.wideExp.Map A)

The space-bounded version of DescriptiveComplexity.wideAccept_iff_expansion.

theorem DescriptiveComplexity.dwideAcceptSpace_iff_expansion (A : Type) [FirstOrder.Language.wide.Structure A] [LinearOrder A] : DWideAcceptSpace.Holds A ↔ DTMAcceptSpace.Holds (Wide.wideExp.Map A)

The deterministic space-bounded version of DescriptiveComplexity.wideAccept_iff_expansion.

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.

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.

theorem DescriptiveComplexity.dwideAcceptSpace_mem_EXPSPACE : EXPSPACE.Mem DWideAcceptSpace

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