Determinism is a promise a reduction can enforce: DTMAcceptSpace ≤ᶠᵒ NTMAcceptSpace

The transfer step of the PSPACE machine bridge. Hardness travels forward along reductions, so a single hardness proof – for the deterministic problem, which is the harder one to establish – gives the nondeterministic one as soon as DescriptiveComplexity.DTMAcceptSpace reduces to DescriptiveComplexity.NTMAcceptSpace.

The two problems differ only in that the deterministic one folds DescriptiveComplexity.TMData.Deterministic into its yes-instances. That condition is first-order (DescriptiveComplexity.SpaceTM.detF), so the reduction is 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; 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.DetToNondet.detG (γ : Type) : FirstOrder.Language.turing.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.DetToNondet.detInterp : FOInterpretation FirstOrder.Language.turing FirstOrder.Language.turing Unit 1

The identity interpretation with a guarded accepting predicate. Every symbol is copied; acc 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.DetToNondet.toBase {A : Type} (x : detInterp.Map A) : A

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

Equations

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

@[simp]

theorem DescriptiveComplexity.DetToNondet.detG_realize {A : Type} [FirstOrder.Language.turing.Structure A] {γ : Type} (v : γ → A) : (detG γ).Realize v ↔ (tmData A).Deterministic

@[simp]

theorem DescriptiveComplexity.DetToNondet.posn_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMPosn x ↔ TMPosn (toBase x)

@[simp]

theorem DescriptiveComplexity.DetToNondet.tr_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMTr x ↔ TMTr (toBase x)

@[simp]

theorem DescriptiveComplexity.DetToNondet.start_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMStart x ↔ TMStart (toBase x)

@[simp]

theorem DescriptiveComplexity.DetToNondet.blank_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMBlank x ↔ TMBlank (toBase x)

@[simp]

theorem DescriptiveComplexity.DetToNondet.right_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMRight x ↔ TMRight (toBase x)

@[simp]

theorem DescriptiveComplexity.DetToNondet.le_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMLe x y ↔ TMLe (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.src_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMSrc x y ↔ TMSrc (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.read_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMRead x y ↔ TMRead (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.dst_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMDst x y ↔ TMDst (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.write_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMWrite x y ↔ TMWrite (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.inp_map {A : Type} [FirstOrder.Language.turing.Structure A] (x y : detInterp.Map A) : TMInp x y ↔ TMInp (toBase x) (toBase y)

@[simp]

theorem DescriptiveComplexity.DetToNondet.acc_map {A : Type} [FirstOrder.Language.turing.Structure A] (x : detInterp.Map A) : TMAcc x ↔ (tmData A).Deterministic ∧ TMAcc (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.

theorem DescriptiveComplexity.DetToNondet.agree_of_det {A : Type} [FirstOrder.Language.turing.Structure A] (hdet : (tmData A).Deterministic) : TMData.Agree (detInterp.mapEquivSelf A) (tmData (detInterp.Map A)) (tmData A)

A deterministic instance is copied verbatim.

theorem DescriptiveComplexity.DetToNondet.not_acceptsSpace_of_not_det {A : Type} [FirstOrder.Language.turing.Structure A] (hdet : ¬(tmData A).Deterministic) : ¬(tmData (detInterp.Map A)).AcceptsSpace

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

theorem DescriptiveComplexity.DetToNondet.correct (A : Type) [FirstOrder.Language.turing.Structure A] [Finite A] [Nonempty A] : DTMAcceptSpace.Holds A ↔ NTMAcceptSpace.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.dtmAcceptSpace_fo_reduction_ntmAcceptSpace : FOReduction DTMAcceptSpace NTMAcceptSpace

Deterministic space-bounded acceptance 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.DTMAcceptSpace is enforced by the reduction itself.

Equations

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