FO(TC) reductions: the logarithmic-space reductions

The reduction notion of DescriptiveComplexity.NL: an interpretation whose defining formulas may consult, besides the input structure, the reachability relations of first-order walks (DescriptiveComplexity.TCFamily). It sits between the two notions already built,

≤ᶠᵒ[≤] ⊆ ≤ᵗᶜ ⊆ ≤ˡᶠᵖ,

the first inclusion strict (DescriptiveComplexity.TransitiveClosureReductionStrict), and it is what “logarithmic-space reduction” means in a machine-free development, exactly as ≤ˡᶠᵖ is what “polynomial-time reduction” means.

What comes for free, and what does not

A walk is an inflationary induction of a very restricted shape (DescriptiveComplexity.TCFamily.inflLimit_toStepDef), so an FO(TC) interpretation is an FO(LFP) interpretation (DescriptiveComplexity.TCInterpretation.toLFP) and an FO(TC) reduction is an FO(LFP) reduction (DescriptiveComplexity.TCReduction.toLFP). Every closure theorem of DescriptiveComplexity.FixedPointReductionClosure therefore transfers: PTIME, NP and coNP are closed under ≤ᵗᶜ, and hardness under first-order reductions implies hardness under these.

What does not transfer is the closure of NL itself: the membership walk pulled back through the reduction is a walk whose steps consult walks, and the route the other classes took is unavailable here – there the induction was absorbed by a smaller class already known to sit inside (PTIME inside NP), and NL has no smaller class to lean on. What it needs is its own normal form, a TC of a formula containing TCs being a single TC, and that is proved as an algebra of walks with two exits (DescriptiveComplexity.Decider, DescriptiveComplexity.TransitiveClosureDecide through DescriptiveComplexity.TransitiveClosureSentenceDecide): NL is closed under ≤ᵗᶜ (DescriptiveComplexity.mem_NL_of_tcReduction, in DescriptiveComplexity.TransitiveClosureReductionClosure).

Transitivity of ≤ᵗᶜ (DescriptiveComplexity.TCReduction.trans, in DescriptiveComplexity.TransitiveClosureReductionTrans) composes two FO(TC) interpretations by pulling the outer walks back through the inner interpretation, flattening them with the same deciders, and extending the inner interpretation to the outer walks' vocabulary. So ≤ᵗᶜ is a reduction order, with the closure properties of NL and of the classes above it.

Interpretations that read walks

structure DescriptiveComplexity.TCInterpretation (L L' : FirstOrder.Language) (Tag : Type) (dim : ℕ) : Type 1

An FO(TC) interpretation: a relativized first-order interpretation whose formulas may read the reachability relations of a finite family of first-order walks over the base structure.

Over an ordered base (L := L₀.sum Language.order) this is Immerman's FO(TC) reduction, the logical form of a logarithmic-space reduction.

• fam : TCFamily L

  The walks whose reachability relations the formulas may read.

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

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

@[instance_reducible]

def DescriptiveComplexity.TCInterpretation.expStructure {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : TCInterpretation L L' Tag dim) (A : Type) [L.Structure A] : (L.sum I.fam.block.lang).Structure A

The base structure expanded by the reachability relations of the walks – the structure the interpretation is read over.

Equations

• I.expStructure A = I.fam.block.structure₁ (I.fam.reachAssign A)

def DescriptiveComplexity.TCInterpretation.Map {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : TCInterpretation L L' Tag dim) (A : Type) [L.Structure A] : Type

The universe of the interpreted structure.

Equations

• I.Map A = I.toRel.MapRel A

@[instance_reducible]

instance DescriptiveComplexity.TCInterpretation.mapStructure {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : TCInterpretation L L' Tag dim) (A : Type) [L.Structure A] [L'.IsRelational] : L'.Structure (I.Map A)

The L'-structure interpreted in A.

Equations

• I.mapStructure A = I.toRel.mapRelStructure A

theorem DescriptiveComplexity.TCInterpretation.map_finite {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : TCInterpretation L L' Tag dim) (A : Type) [L.Structure A] [Finite Tag] [Finite A] : Finite (I.Map A)

A walk is an induction, so an FO(TC) interpretation is an FO(LFP) one

noncomputable def DescriptiveComplexity.TCInterpretation.toLFP {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : TCInterpretation L L' Tag dim) : LFPInterpretation L L' Tag dim

An FO(TC) interpretation, read as an FO(LFP) interpretation: the family's walks become the one induction that computes their reachability relations (DescriptiveComplexity.TCFamily.toStepDef), and the interpretation is unchanged.

Equations

• I.toLFP = { ind := I.fam.toStepDef, toRel := I.toRel }

theorem DescriptiveComplexity.TCInterpretation.expStructure_toLFP {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} {I : TCInterpretation L L' Tag dim} {A : Type} [L.Structure A] [Finite A] : I.toLFP.expStructure A = I.expStructure A

The two readings expand the base structure by the same relations: the value of the induction is the reachability relations.

def DescriptiveComplexity.TCInterpretation.mapEquivOfEq {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} {I : TCInterpretation L L' Tag dim} {A : Type} [L'.IsRelational] {inst₁ inst₂ : (L.sum I.fam.block.lang).Structure A} (h : inst₁ = inst₂) : L'.Equiv (I.toRel.MapRel A) (I.toRel.MapRel A)

Equal expansions give the same interpreted structure.

Equations

• DescriptiveComplexity.TCInterpretation.mapEquivOfEq h = h ▸ let __Equiv := Equiv.refl (I.toRel.MapRel A); { toEquiv := __Equiv, map_fun' := ⋯, map_rel' := ⋯ }

noncomputable def DescriptiveComplexity.TCInterpretation.toLFPLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} {I : TCInterpretation L L' Tag dim} {A : Type} [L.Structure A] [L'.IsRelational] [Finite A] : L'.Equiv (I.toLFP.Map A) (I.Map A)

The FO(LFP) reading interprets the same structure: the identity map on tagged tuples is an isomorphism.

Equations

• DescriptiveComplexity.TCInterpretation.toLFPLEquiv = DescriptiveComplexity.TCInterpretation.mapEquivOfEq ⋯

FO(TC) reductions

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

An FO(TC) reduction from P to Q – a logarithmic-space reduction, in the logical form of Immerman 1999: an FO(TC) interpretation over the ordered expansion of the source vocabulary, mapping yes-instances exactly to yes-instances, for every finite linear order on the input.

• 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.

• toInterpretation : TCInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim

  The underlying FO(TC) interpretation, over the ordered expansion.

• map_nonempty (A : Type) [L.Structure A] [LinearOrder A] [Finite A] [Nonempty A] : Nonempty (self.toInterpretation.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 (self.toInterpretation.Map A)

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

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

An FO(TC) reduction from P to Q – a logarithmic-space reduction, in the logical form of Immerman 1999: an FO(TC) interpretation over the ordered expansion of the source vocabulary, mapping yes-instances exactly to yes-instances, for every finite linear order on the input.

Equations

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

Every FO(TC) reduction is an FO(LFP) reduction

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

An FO(TC) reduction is an FO(LFP) reduction: reachability is an inflationary induction. Every closure property of ≤ˡᶠᵖ transfers along this.

Equations

• f.toLFP = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toInterpretation := f.toInterpretation.toLFP, map_nonempty := ⋯, correct := ⋯ }

Every first-order reduction is an FO(TC) reduction

def DescriptiveComplexity.TCFamily.empty (L : FirstOrder.Language) : TCFamily L

The empty family of walks: no relation variables, so the expansion is the structure itself.

Equations

• DescriptiveComplexity.TCFamily.empty L = { Ix := Empty, ixFinite := ⋯, spec := fun (i : Empty) => i.elim }

def DescriptiveComplexity.RelFOInterpretation.toTCFam {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (J : RelFOInterpretation L L' Tag dim) (F : TCFamily L) : TCInterpretation L L' Tag dim

A relativized interpretation, read as an FO(TC) interpretation whose formulas ignore the walks it is given.

Equations

• J.toTCFam F = { fam := F, toRel := DescriptiveComplexity.RelFOInterpretation.liftSource FirstOrder.Language.LHom.sumInl J }

def DescriptiveComplexity.RelFOInterpretation.toTCFamLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} [L'.IsRelational] (J : RelFOInterpretation L L' Tag dim) (F : TCFamily L) (A : Type) [instA : L.Structure A] : L'.Equiv ((J.toTCFam F).Map A) (J.MapRel A)

An interpretation that ignores its walks produces exactly the structure of the relativized interpretation it lifts, whatever the walks are: the expansion interprets the base symbols as the base structure does.

Equations

• J.toTCFamLEquiv F A = DescriptiveComplexity.RelFOInterpretation.liftSourceLEquiv FirstOrder.Language.LHom.sumInl J ⋯

def DescriptiveComplexity.RelFOInterpretation.toTC {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (J : RelFOInterpretation L L' Tag dim) : TCInterpretation L L' Tag dim

A relativized interpretation, read as an FO(TC) interpretation that consults no walk.

Equations

• J.toTC = J.toTCFam (DescriptiveComplexity.TCFamily.empty L)

def DescriptiveComplexity.RelFOInterpretation.toTCLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} [L'.IsRelational] (J : RelFOInterpretation L L' Tag dim) (A : Type) [L.Structure A] : L'.Equiv (J.toTC.Map A) (J.MapRel A)

The FO(TC) interpretation with no walks produces exactly the structure of the relativized interpretation it lifts.

Equations

• J.toTCLEquiv A = J.toTCFamLEquiv (DescriptiveComplexity.TCFamily.empty L) A

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

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

Equations

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

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

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

Equations

• f.toTC = f.toRel.toTC

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

An FO reduction is an FO(TC) reduction.

Equations

• f.toTC = f.toOrdered.toRel.toTC

The classes above NL are closed under FO(TC) reductions

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

PTIME is closed under FO(TC) reductions.

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

NP is closed under FO(TC) reductions.

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

coNP is closed under FO(TC) reductions.