Determinism is a promise a reduction can enforce: DWideAcceptSpace ≤ᶠᵒ WideAcceptSpace

The transfer step of the EXPSPACE machine bridge, and the exact analogue of DescriptiveComplexity.Problems.Machine.SpaceDet one exponent up. Hardness travels forward along reductions, so the deterministic problem – the one a program is naturally proved hard for, its run being unique – hands the nondeterministic one its hardness as soon as DescriptiveComplexity.DWideAcceptSpace reduces to DescriptiveComplexity.WideAcceptSpace.

The two problems differ only in that the deterministic one folds DescriptiveComplexity.WideDet into its yes-instances, and that condition is first-order – DescriptiveComplexity.SpaceTM.detF is stated at an arbitrary vocabulary and arbitrary symbols, so the sentence is the same one the polynomial-level bridge uses, read at FirstOrder.Language.wide's symbols. The reduction is therefore the identity interpretation – one dimension, one tag – with a single change: the accepting states of the image are the accepting states of the source guarded by the determinism sentence. A source whose table is deterministic is copied verbatim, so the two are isomorphic; a source whose table is not has no accepting state at all in the image, hence no accepting run, and both sides are no-instances.

Nothing here needs an order, so this is a plain ≤ᶠᵒ reduction; the ordered and relativized readings follow.

The interpretation

noncomputable def DescriptiveComplexity.WideDetToNondet.detG (γ : Type) : FirstOrder.Language.wide.Formula γ

The determinism of the instance, as a first-order formula whose free variables are unused: the guard the image puts on its accepting states.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def DescriptiveComplexity.WideDetToNondet.detInterp : FOInterpretation FirstOrder.Language.wide FirstOrder.Language.wide Unit 1

The identity interpretation with a guarded accepting predicate. Every symbol is copied; wmAcc is copied only when the transition table is deterministic.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.WideDetToNondet.toBase {A : Type} (x : detInterp.Map A) : A

The universe of the image is the universe of the source.

Equations

• DescriptiveComplexity.WideDetToNondet.toBase x = (DescriptiveComplexity.WideDetToNondet.detInterp.mapEquivSelf A) x

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.detG_realize {A : Type} [FirstOrder.Language.wide.Structure A] {γ : Type} (v : γ → A) : (detG γ).Realize v ↔ WideDet A

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.tr_map {A : Type} [FirstOrder.Language.wide.Structure A] (x : detInterp.Map A) : WMTr x ↔ WMTr (toBase x)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.start_map {A : Type} [FirstOrder.Language.wide.Structure A] (x : detInterp.Map A) : WMStart x ↔ WMStart (toBase x)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.blank_map {A : Type} [FirstOrder.Language.wide.Structure A] (x : detInterp.Map A) : WMBlank x ↔ WMBlank (toBase x)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.right_map {A : Type} [FirstOrder.Language.wide.Structure A] (x : detInterp.Map A) : WMRight x ↔ WMRight (toBase x)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.le_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMLe x y ↔ WMLe (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.src_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMSrc x y ↔ WMSrc (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.read_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMRead x y ↔ WMRead (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.dst_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMDst x y ↔ WMDst (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.write_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMWrite x y ↔ WMWrite (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.inp_map {A : Type} [FirstOrder.Language.wide.Structure A] (x y : detInterp.Map A) : WMInp x y ↔ WMInp (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.WideDetToNondet.acc_map {A : Type} [FirstOrder.Language.wide.Structure A] (x : detInterp.Map A) : WMAcc x ↔ WideDet A ∧ WMAcc (toBase x)

The accepting states of the image are guarded: an element is accepting there exactly when the source table is deterministic and it is accepting in the source.

noncomputable def DescriptiveComplexity.WideDetToNondet.detEquiv {A : Type} [FirstOrder.Language.wide.Structure A] (hdet : WideDet A) : FirstOrder.Language.wide.Equiv A (detInterp.Map A)

A deterministic instance is copied verbatim, so the image is the source up to the identification of the two universes.

Equations

• DescriptiveComplexity.WideDetToNondet.detEquiv hdet = { toEquiv := (DescriptiveComplexity.WideDetToNondet.detInterp.mapEquivSelf A).symm, map_fun' := ⋯, map_rel' := ⋯ }

theorem DescriptiveComplexity.WideDetToNondet.not_acceptsSpace_of_not_det {A : Type} [FirstOrder.Language.wide.Structure A] (hdet : ¬WideDet A) : ¬(wideData (detInterp.Map A)).AcceptsSpace

A nondeterministic instance has no accepting state in the image, so its image cannot accept.

theorem DescriptiveComplexity.WideDetToNondet.correct (A : Type) [FirstOrder.Language.wide.Structure A] [Finite A] [Nonempty A] : DWideAcceptSpace.Holds A ↔ WideAcceptSpace.Holds (detInterp.Map A)

The reduction is correct: the image accepts in bounded space exactly when the source is a well-formed deterministic machine accepting in bounded space.

noncomputable def DescriptiveComplexity.dwideAcceptSpace_fo_reduction_wideAcceptSpace : FOReduction DWideAcceptSpace WideAcceptSpace

Deterministic wide acceptance in bounded space reduces to the nondeterministic problem. The interpretation is the identity, save that the image only keeps its accepting states when the source table is deterministic – a first-order condition, so the promise folded into the yes-instances of DescriptiveComplexity.DWideAcceptSpace is enforced by the reduction itself. This is what lets the EXPSPACE-hardness of the deterministic problem be proved once and inherited by DescriptiveComplexity.WideAcceptSpace.

Equations

• One or more equations did not get rendered due to their size.