NL is closed under FO(TC) reductions, and LOGSPACE under FO(DTC) reductions

The two closure theorems the reductions with a logic inside were missing:

• DescriptiveComplexity.mem_NL_of_tcReduction – NL is closed under ≤ᵗᶜ, so ≤ᵗᶜ is the reduction notion of NL as ≤ˡᶠᵖ is that of PTIME;
• DescriptiveComplexity.mem_LOGSPACE_of_dtcReduction – LOGSPACE is closed under ≤ᵈᵗᶜ, the many-one logarithmic-space reduction of the textbooks.

Both are Immerman's normal form, in the walk-algebra form of DescriptiveComplexity.TransitiveClosureDecide. Given P ≤ᵗᶜ Q and a walk deciding Q, the walk is pulled back through the reduction's interpretation (DescriptiveComplexity.TCSpec.pullSpec, the sentence-level reading of DescriptiveComplexity.ParamTCSpec.comapRel): a walk over the base structure expanded by the reachability relations of the reduction's own walks. Its step, source and target formulas read those relations, and every such formula has a decider (DescriptiveComplexity.Decider.exists_of_formula, the atoms being DescriptiveComplexity.ParamTCSpec.reachDecider); the walk is flattened (DescriptiveComplexity.ParamTCSpec.flat) and the sentence “some source reaches some target” is one decider (DescriptiveComplexity.ParamTCSpec.sentenceDecider), hence one DescriptiveComplexity.TCSpec – FO(TC) definability of P, which is membership in NL (DescriptiveComplexity.tcDefinable_iff_mem_NL).

The deterministic case runs the same assembly with the deterministic atoms (DescriptiveComplexity.ParamTCSpec.detReachDecider), the searching flat walk, and the deterministic reading of everything: each construction is functional, so the resulting specification is unchanged by determinization (DescriptiveComplexity.Decider.det_accepts_toSpec), which is FO(DTC) definability. The searching flat walk simulates the outer walk only when that one is functional – which the pullback of a determinized walk is (DescriptiveComplexity.TCSpec.pullSpec_functional).

Transport along an isomorphism, with explicit structures

theorem DescriptiveComplexity.ParamTCSpec.stepAt_of_equiv {L'' : FirstOrder.Language} {M N : Type} {instM : L''.Structure M} {instN : L''.Structure N} (e : L''.Equiv M N) (s : ParamTCSpec L'') (z : Fin s.par → M) (a b : s.Node M) : s.StepAt (⇑e ∘ z) (a.1, ⇑e ∘ a.2) (b.1, ⇑e ∘ b.2) ↔ s.StepAt z a b

A step of a parameterized walk transports along an isomorphism.

theorem DescriptiveComplexity.ParamTCSpec.reachAt_of_equiv {L'' : FirstOrder.Language} {M N : Type} {instM : L''.Structure M} {instN : L''.Structure N} (e : L''.Equiv M N) (s : ParamTCSpec L'') (z : Fin s.par → M) (a b : s.Node M) : s.ReachAt (⇑e ∘ z) (a.1, ⇑e ∘ a.2) (b.1, ⇑e ∘ b.2) ↔ s.ReachAt z a b

Reachability in a parameterized walk transports along an isomorphism.

The pullback of a sentence through a relativized ordered interpretation

@[reducible]

noncomputable def DescriptiveComplexity.TCSpec.pullSpec {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) : ParamTCSpec L₁

The pullback of a specification's walk through a relativized ordered interpretation.

Equations

• spec.pullSpec J = spec.toParam.comapRel J Fin.elim0

noncomputable def DescriptiveComplexity.TCSpec.pullSrc {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) (m : (spec.pullSpec J).Mode) : L₁.Formula (Fin (spec.pullSpec J).k)

The pulled source formula: the tuple is in the domain and encodes a source.

Equations

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

noncomputable def DescriptiveComplexity.TCSpec.pullTgt {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) (m : (spec.pullSpec J).Mode) : L₁.Formula (Fin (spec.pullSpec J).k)

The pulled target formula.

Equations

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

@[reducible, inline]

abbrev DescriptiveComplexity.TCSpec.pullPar {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) (A : Type) : Fin (spec.pullSpec J).par → A

The valuation of the (absent) parameters of the pulled walk.

Equations

• spec.pullPar J A i = (Fin.cast ⋯ i).elim0

theorem DescriptiveComplexity.TCSpec.realize_pullSrc {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) {A : Type} [L₁.Structure A] (a : (spec.pullSpec J).Node A) : (spec.pullSrc J a.1).Realize a.2 ↔ ∃ (ha : ParamTCSpec.InDom a), (spec.src a.1.1).Realize (ParamTCSpec.decode a ha).2

theorem DescriptiveComplexity.TCSpec.realize_pullTgt {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) {A : Type} [L₁.Structure A] (a : (spec.pullSpec J).Node A) : (spec.pullTgt J a.1).Realize a.2 ↔ ∃ (ha : ParamTCSpec.InDom a), (spec.tgt a.1.1).Realize (ParamTCSpec.decode a ha).2

theorem DescriptiveComplexity.TCSpec.encode_decode {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) {A : Type} [L₁.Structure A] (a : (spec.pullSpec J).Node A) (ha : ParamTCSpec.InDom a) : ParamTCSpec.encode Fin.elim0 (ParamTCSpec.decode a ha) = a

Decoding then encoding is the identity on in-domain nodes.

def DescriptiveComplexity.TCSpec.PulledAccepts {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) (A : Type) [L₁.Structure A] : Prop

The pulled sentence: some pulled source reaches some pulled target.

Equations

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

theorem DescriptiveComplexity.TCSpec.pulledAccepts_iff {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) {A : Type} [L₁.Structure A] : spec.PulledAccepts J A ↔ ∃ (u : spec.Node (J.MapRel A)) (v : spec.Node (J.MapRel A)), (spec.src u.1).Realize u.2 ∧ (spec.tgt v.1).Realize v.2 ∧ spec.toParam.ReachAt (fun (i : Fin spec.toParam.par) => i.elim0) u v

The pulled sentence says what the original says on the interpreted structure, read with the interpretation's own structure.

theorem DescriptiveComplexity.TCSpec.pullSpec_functional {L₁ L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] {dim : ℕ} (spec : TCSpec L') (J : RelFOInterpretation L₁ (L'.sum FirstOrder.Language.order) Tag dim) {A : Type} [L₁.Structure A] (h : ∀ (u v w : spec.Node (J.MapRel A)), spec.toParam.StepAt (fun (i : Fin spec.toParam.par) => i.elim0) u v → spec.toParam.StepAt (fun (i : Fin spec.toParam.par) => i.elim0) u w → v = w) (z : Fin (spec.pullSpec J).par → A) (a b c : (spec.pullSpec J).Node A) (hb : (spec.pullSpec J).StepAt z a b) (hc : (spec.pullSpec J).StepAt z a c) : b = c

The pullback of a functional walk is functional: steps correspond between in-domain nodes, and out-of-domain nodes have none.

The sentence on the interpreted structure, pulled back

@[reducible, inline]

noncomputable abbrev DescriptiveComplexity.TCInterpretation.ordInterp {L L' : FirstOrder.Language} {Tag : Type} [LinearOrder Tag] {dim : ℕ} (I : TCInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) : RelFOInterpretation ((L.sum FirstOrder.Language.order).sum I.fam.block.lang) (L'.sum FirstOrder.Language.order) Tag dim

The reduction's interpretation, extended by the lexicographic order.

Equations

• I.ordInterp = DescriptiveComplexity.RelFOInterpretation.ordExtendSrc FirstOrder.Language.LHom.sumInl I.toRel

theorem DescriptiveComplexity.TCInterpretation.accepts_iff_pulled {L L' : FirstOrder.Language} [L'.IsRelational] {Tag : Type} [Finite Tag] [LinearOrder Tag] {dim : ℕ} (I : TCInterpretation (L.sum FirstOrder.Language.order) L' Tag dim) (spec : TCSpec L') (A : Type) [L.Structure A] [LinearOrder A] : spec.Accepts (I.Map A) ↔ spec.PulledAccepts I.ordInterp A

Acceptance on the interpreted structure is the pulled sentence on the base structure expanded by the reduction's walks.

Closure of FO(TC) definability

theorem DescriptiveComplexity.exists_bot (A : Type) [LinearOrder A] [Finite A] [Nonempty A] : ∃ (a₀ : A), ∀ (a : A), a₀ ≤ a

A bottom element of a finite nonempty linear order.

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

FO(TC) definability is closed under FO(TC) reductions: the normal form.

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

FO(DTC) definability is closed under FO(DTC) reductions: the normal form, deterministically.

The classes

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

NL is closed under FO(TC) reductions.

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

NL is closed under FO(DTC) reductions.

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

LOGSPACE is closed under FO(DTC) reductions.

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

An FO(TC) reduction complements: the same interpretation reduces the complements.

Equations

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

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

An FO(DTC) reduction complements.

Equations

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

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

coNL is closed under FO(TC) reductions.

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

coLOGSPACE is closed under FO(DTC) reductions (the complement class LOGSPACE.compl is DescriptiveComplexity.coLOGSPACE, which is defined with its complete problem in DescriptiveComplexity.Problems.ReachabilityDet.Complement).