Composing an FO(TC) reduction with a first-order one

An FO(TC) reduction followed by a first-order reduction is an FO(TC) reduction (DescriptiveComplexity.TCReduction.trans_rel and its variants). This is the half of transitivity that needs no normal form: the outer reduction contributes no walks, so the composite consults exactly the walks the inner one did.

Why this half is free and the other is not

Composing P ≤ᵗᶜ Q with Q ≤ʳᶠᵒ[≤] R pulls the outer interpretation's formulas back through the inner one. Those formulas are first-order over Q's vocabulary; what the pullback substitutes for their atoms are the inner interpretation's formulas, which read the inner walks. So the composite's formulas read the same walks, at the same nesting depth, and the family is carried over unchanged – the composition is DescriptiveComplexity.RelFOInterpretation.compRel under the walks, with the lexicographic order supplied to the outer reduction by DescriptiveComplexity.RelFOInterpretation.ordExtendSrc.

The other half – P ≤ᵗᶜ Q followed by Q ≤ᵗᶜ R – is where the nesting appears: the outer walks run on the interpreted structure, and pulling them back gives walks whose step formulas read the inner walks' reachability atoms. Those flatten (DescriptiveComplexity.ParamTCSpec.flat), and the inner interpretation extended to their vocabulary substitutes the flattened atoms for the outer ones: that is DescriptiveComplexity.TCReduction.trans, in DescriptiveComplexity.TransitiveClosureReductionTrans.

The composite interpretation

noncomputable def DescriptiveComplexity.RelFOInterpretation.compTC {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ d₂ : ℕ} (J : RelFOInterpretation (L₂.sum FirstOrder.Language.order) L₃ Tag₂ d₂) (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) : TCInterpretation (L₁.sum FirstOrder.Language.order) L₃ (Tag₂ × (Fin d₂ → Tag₁)) (d₂ * d₁)

An FO(TC) interpretation followed by a relativized first-order one. The walks are those of the inner interpretation, unchanged; the interpretations compose with the guarded pullback, the intermediate structure carrying the lexicographic order.

Equations

• J.compTC I = { fam := I.fam, toRel := J.compRel (DescriptiveComplexity.RelFOInterpretation.ordExtendSrc FirstOrder.Language.LHom.sumInl I.toRel) }

@[instance_reducible]

noncomputable def DescriptiveComplexity.TCInterpretation.mapLinearOrder {L₁ L₂ : FirstOrder.Language} {Tag₁ : Type} [LinearOrder Tag₁] {d₁ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (A : Type) [L₁.Structure A] [LinearOrder A] : LinearOrder (I.Map A)

The lexicographic order on the structure an FO(TC) interpretation produces.

Equations

• I.mapLinearOrder A = I.toRel.mapRelLinearOrderSrc (I.expStructure A)

noncomputable def DescriptiveComplexity.RelFOInterpretation.compTCLEquiv {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] [L₃.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] [LinearOrder Tag₁] {d₁ d₂ : ℕ} (I : TCInterpretation (L₁.sum FirstOrder.Language.order) L₂ Tag₁ d₁) (A : Type) [L₁.Structure A] [LinearOrder A] (J : RelFOInterpretation (L₂.sum FirstOrder.Language.order) L₃ Tag₂ d₂) : L₃.Equiv ((J.compTC I).Map A) (J.MapRel (I.Map A))

The composite interprets the twice-interpreted structure: the outer interpretation read on the inner one's output, ordered lexicographically.

Equations

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

Composition of reductions

noncomputable def DescriptiveComplexity.TCReduction.trans_rel {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : TCReduction P Q) (f : RelOrderedFOReduction Q R) : TCReduction P R

An FO(TC) reduction followed by a relativized first-order reduction. The composite consults exactly the walks the inner reduction did.

Equations

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

noncomputable def DescriptiveComplexity.TCReduction.trans_fo {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : TCReduction P Q) (f : OrderedFOReduction Q R) : TCReduction P R

An FO(TC) reduction followed by an ordered first-order reduction.

Equations

• g.trans_fo f = g.trans_rel f.toRel

noncomputable def DescriptiveComplexity.DTCReduction.trans_rel {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] {P : DecisionProblem L₁} {Q : DecisionProblem L₂} {R : DecisionProblem L₃} (g : DTCReduction P Q) (f : RelOrderedFOReduction Q R) : TCReduction P R

An FO(DTC) reduction followed by a relativized first-order reduction.

Equations

• g.trans_rel f = g.toTC.trans_rel f

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemTCReductionOrderedFOReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans TCReduction OrderedFOReduction TCReduction

Trans instance: an FO(TC) reduction composes with an ordered first-order one.

Equations

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