FO(DTC) reductions: the logarithmic-space reduction of the textbooks

DescriptiveComplexity.TCReduction lets a reduction's formulas consult nondeterministic walks. The classical many-one reduction for the classes at this level is the deterministic logarithmic-space one, and this file is it: DescriptiveComplexity.DTCReduction, notation P ≤ᵈᵗᶜ Q, where every walk is read through its determinization – it may follow a step only when that step is the only one available.

Determinism as a formula

The packaging is the library's own, from DescriptiveComplexity.TransitiveClosureDet: rather than carrying a proof that a walk is functional – which is not first-order data, and would have to be re-established after every pullback – the walk is read through

detStep(x̄, ȳ, z̄) := step(x̄, ȳ, z̄) ∧ ∀ w̄. step(x̄, w̄, z̄) → w̄ = ȳ

(DescriptiveComplexity.ParamTCSpec.det), which is again first-order. Every specification then denotes a legitimate deterministic walk (DescriptiveComplexity.ParamTCSpec.det_functional) and nothing has to be assumed; on a walk that is already functional the two readings agree (DescriptiveComplexity.ParamTCSpec.detStepAt_of_functional), which is how an existing walk – the parity walk, say – is reused at this notion.

Where it sits

≤ᶠᵒ[≤] ⊆ ≤ᵈᵗᶜ ⊆ ≤ᵗᶜ ⊆ ≤ˡᶠᵖ: a determinized walk is a walk, so everything DescriptiveComplexity.TransitiveClosureReduction proves transfers, and PTIME, NP and coNP are closed under ≤ᵈᵗᶜ as well.

DescriptiveComplexity.LOGSPACE is closed under it (DescriptiveComplexity.mem_LOGSPACE_of_dtcReduction, in DescriptiveComplexity.TransitiveClosureReductionClosure), by the same normal form as NL under ≤ᵗᶜ with one difference at the atoms: flattening a walk that consults walks needs non-reachability at the negative occurrences, and a deterministic walk is witnessed not to arrive by a step budget (DescriptiveComplexity.ParamTCSpec.detReachDecider), where a nondeterministic one needs inductive counting. Transitivity is DescriptiveComplexity.DTCReduction.trans, the composite of DescriptiveComplexity.TransitiveClosureReductionTrans read through its determinization.

Determinizing a parameterized walk

def DescriptiveComplexity.ParamTCSpec.detVar {L : FirstOrder.Language} (s : ParamTCSpec L) : (Fin s.k ⊕ Fin s.k) ⊕ Fin s.par → ((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par) ⊕ Fin s.k

The renaming used by the uniqueness clause: the step formula is re-read with its first tuple still the current one, its second tuple the freshly quantified w̄, and its parameters unchanged.

Equations

• s.detVar (Sum.inl (Sum.inl i)) = Sum.inl (Sum.inl (Sum.inl i))
• s.detVar (Sum.inl (Sum.inr i)) = Sum.inr i
• s.detVar (Sum.inr j) = Sum.inl (Sum.inr j)

noncomputable def DescriptiveComplexity.ParamTCSpec.detStep {L : FirstOrder.Language} (s : ParamTCSpec L) (m n : s.Mode) : L.Formula ((Fin s.k ⊕ Fin s.k) ⊕ Fin s.par)

The determinized step formula at a pair of modes: this step, and no other step out of the current node. As in DescriptiveComplexity.TCSpec.detStep, the competing successor's mode is compared statically, so the uniqueness clause has one conjunct per mode.

Equations

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

@[reducible]

noncomputable def DescriptiveComplexity.ParamTCSpec.det {L : FirstOrder.Language} (s : ParamTCSpec L) : ParamTCSpec L

The deterministic reading of a walk: the same modes, arity and parameters, with the step formula replaced by its determinization.

Reducible, so that the modes, the arity and the parameter count of s.det are those of s transparently – a node of the deterministic reading is a node, and the block of a determinized family is the block of the family.

Equations

• s.det = { Mode := s.Mode, modeFinite := ⋯, k := s.k, par := s.par, step := s.detStep }

theorem DescriptiveComplexity.ParamTCSpec.realize_detStep {L : FirstOrder.Language} (s : ParamTCSpec L) {A : Type} [L.Structure A] (m n : s.Mode) (x y : Fin s.k → A) (z : Fin s.par → A) : (s.detStep m n).Realize (Sum.elim (Sum.elim x y) z) ↔ (s.step m n).Realize (Sum.elim (Sum.elim x y) z) ∧ ∀ (m' : s.Mode) (w : Fin s.k → A), (s.step m m').Realize (Sum.elim (Sum.elim x w) z) → m' = n ∧ w = y

theorem DescriptiveComplexity.ParamTCSpec.detStepAt_iff {L : FirstOrder.Language} (s : ParamTCSpec L) {A : Type} [L.Structure A] (z : Fin s.par → A) (a b : s.Node A) : s.det.StepAt z a b ↔ s.StepAt z a b ∧ ∀ (c : s.Node A), s.StepAt z a c → c = b

A determinized step is a step with no competitor.

def DescriptiveComplexity.ParamTCSpec.Functional {L : FirstOrder.Language} (s : ParamTCSpec L) (A : Type) [L.Structure A] : Prop

A walk is functional at a structure when no node has two successors.

Equations

• s.Functional A = ∀ (z : Fin s.par → A) (a b c : s.Node A), s.StepAt z a b → s.StepAt z a c → b = c

theorem DescriptiveComplexity.ParamTCSpec.det_functional {L : FirstOrder.Language} {s : ParamTCSpec L} {A : Type} [L.Structure A] : s.det.Functional A

The deterministic reading is functional, whatever walk it comes from: this is what makes determinization the right packaging, there being nothing left to assume.

theorem DescriptiveComplexity.ParamTCSpec.detStepAt_of_functional {L : FirstOrder.Language} {s : ParamTCSpec L} {A : Type} [L.Structure A] (h : s.Functional A) (z : Fin s.par → A) (a b : s.Node A) : s.det.StepAt z a b ↔ s.StepAt z a b

On a walk that is already functional, the deterministic reading is the original one.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_det_of_functional {L : FirstOrder.Language} {s : ParamTCSpec L} {A : Type} [L.Structure A] (h : s.Functional A) (z : Fin s.par → A) (a b : s.Node A) : s.det.ReachAt z a b ↔ s.ReachAt z a b

Reachability is unchanged by determinizing a functional walk.

Determinizing a family

@[reducible]

noncomputable def DescriptiveComplexity.TCFamily.det {L : FirstOrder.Language} (F : TCFamily L) : TCFamily L

The deterministic reading of a family: every walk read through its determinization. Reducible, so that F.det.block is F.block.

Equations

• F.det = { Ix := F.Ix, ixFinite := ⋯, spec := fun (i : F.Ix) => (F.spec i).det }

def DescriptiveComplexity.TCFamily.Functional {L : FirstOrder.Language} (F : TCFamily L) (A : Type) [L.Structure A] : Prop

A family is functional when each of its walks is.

Equations

• F.Functional A = ∀ (i : F.Ix), (F.spec i).Functional A

theorem DescriptiveComplexity.TCFamily.reachAssign_det_of_functional {L : FirstOrder.Language} {F : TCFamily L} {A : Type} [L.Structure A] (h : F.Functional A) : F.det.reachAssign A = F.reachAssign A

A functional family is unchanged by determinization: its relation variables hold the same relations either way.

An FO(TC) sentence read deterministically

theorem DescriptiveComplexity.TCSpec.realize_acceptsF_det {L₀ : FirstOrder.Language} (spec : TCSpec L₀) {A : Type} [L₀.Structure A] [LinearOrder A] (h : spec.toFamily.Functional A) : A ⊨ spec.acceptsF ↔ spec.Accepts A

A functional walk may be read deterministically at no cost: its walk-as-an-atom formula (DescriptiveComplexity.TCSpec.acceptsF) still says acceptance when the relation variables hold the determinized reachability relations. This is what lets an existing walk of the catalog be reused at the deterministic notion.

FO(DTC) reductions

structure DescriptiveComplexity.DTCReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] (P : DecisionProblem L) (Q : DecisionProblem L') : Type 1

An FO(DTC) reduction from P to Q – a deterministic logarithmic-space reduction, in the logical form of Immerman 1987: an interpretation over the ordered expansion whose formulas may read the reachability relations of a family of walks, each read through its determinization.

• Tag : Type

  The tags used by the underlying interpretation.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures map to finite structures.

• dim : ℕ

  The dimension of the underlying interpretation.

• fam : TCFamily (L.sum FirstOrder.Language.order)

  The walks the formulas may read – before determinization, which is how they are read.

• toRel : RelFOInterpretation ((L.sum FirstOrder.Language.order).sum self.fam.block.lang) L' self.Tag self.dim

  The interpretation, over the base expanded by the walks' relation variables.

• map_nonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty ({ fam := self.fam.det, toRel := self.toRel }.Map A)

  The interpreted structure is nonempty on nonempty finite ordered inputs.

• correct (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : P.Holds A ↔ Q.Holds ({ fam := self.fam.det, toRel := self.toRel }.Map A)

  Yes-instances map exactly to yes-instances, whatever the linear order.

def DescriptiveComplexity.«term_≤ᵈᵗᶜ_» : Lean.TrailingParserDescr

An FO(DTC) reduction from P to Q – a deterministic logarithmic-space reduction, in the logical form of Immerman 1987: an interpretation over the ordered expansion whose formulas may read the reachability relations of a family of walks, each read through its determinization.

Equations

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

noncomputable def DescriptiveComplexity.DTCReduction.toTC {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : DTCReduction P Q) : TCReduction P Q

An FO(DTC) reduction is an FO(TC) reduction: a determinized walk is a walk. Every closure property of ≤ᵗᶜ – hence of ≤ˡᶠᵖ – transfers along this.

Equations

• f.toTC = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toInterpretation := { fam := f.fam.det, toRel := f.toRel }, map_nonempty := ⋯, correct := ⋯ }

noncomputable def DescriptiveComplexity.RelOrderedFOReduction.toDTC {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : RelOrderedFOReduction P Q) : DTCReduction P Q

A relativized ordered FO reduction is an FO(DTC) reduction, consulting no walk.

Equations

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

noncomputable def DescriptiveComplexity.OrderedFOReduction.toDTC {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) : DTCReduction P Q

An ordered FO reduction is an FO(DTC) reduction.

Equations

• f.toDTC = f.toRel.toDTC

noncomputable def DescriptiveComplexity.FOReduction.toDTC {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) : DTCReduction P Q

An FO reduction is an FO(DTC) reduction.

Equations

• f.toDTC = f.toOrdered.toRel.toDTC

theorem DescriptiveComplexity.mem_PTIME_of_dtcReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : DTCReduction P Q) (h : PTIME.Mem Q) : PTIME.Mem P

PTIME is closed under FO(DTC) reductions.

theorem DescriptiveComplexity.mem_NP_of_dtcReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : DTCReduction P Q) (h : NP.Mem Q) : NP.Mem P

NP is closed under FO(DTC) reductions.

theorem DescriptiveComplexity.mem_coNP_of_dtcReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} (f : DTCReduction P Q) (h : coNP.Mem Q) : coNP.Mem P

coNP is closed under FO(DTC) reductions.