Composition of FO(LFP) reductions

Transitivity of P ≤ˡᶠᵖ Q (DescriptiveComplexity.LFPReduction.trans), the FO(LFP) analogue of DescriptiveComplexity.RelOrderedFOReduction.trans. It is what makes ≤ˡᶠᵖ a reduction order, and what the hardness notion of DescriptiveComplexity.FixedPointReductionClosure consumes.

Why this is a theorem and not bookkeeping

Composing two first-order interpretations pulls the outer formulas back through the inner one. Here the outer formulas may also read the outer induction, run over the interpreted structure, so composition has to say that a fixed point computed on the interpreted structure is computed by an induction on the base – after the inner induction, whose value the inner interpretation reads. Nothing about that is formal: it is the substitution property of the logic, and the statement classically known as “FO(LFP) reductions compose”.

Three constructions already in the library supply the three halves:

• the outer induction pulls back through the inner (relativized) interpretation, DescriptiveComplexity.StepDef.pullRel, giving an induction over the base expanded by the inner induction's block;
• two inductions run one after the other are one induction, DescriptiveComplexity.StepDef.stratify – whose gate fires exactly when the first has converged, so the composite's limit has the inner limit and the pulled outer limit as its two parts (DescriptiveComplexity.StepDef.strat1Assign_inflLimit, DescriptiveComplexity.StepDef.strat2Assign_inflLimit);
• the interpretations compose, with the guarded pullback that a definable domain requires, DescriptiveComplexity.RelFOInterpretation.compRel.

DescriptiveComplexity.LFPInterpretation.compLEquiv assembles them: the composite interpretation produces the twice-interpreted structure.

The order of the intermediate structure

As for DescriptiveComplexity.OrderedFOReduction.trans, the outer reduction's formulas mention the order of the intermediate structure, which the inner interpretation does not produce. The fix is the same – the lexicographic order on tagged tuples – with one twist: the inner interpretation's source is the base expanded by its own induction's block, so the lexicographic formula has to be read there. DescriptiveComplexity.RelFOInterpretation.ordExtendSrc is the order extension along an arbitrary vocabulary map of the source, of which DescriptiveComplexity.RelFOInterpretation.ordExtendRel is the identity case.

The order extension, over a larger source vocabulary

noncomputable def DescriptiveComplexity.RelFOInterpretation.ordExtendSrc {L₁ Lsrc L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (φ : L₁.sum FirstOrder.Language.order →ᴸ Lsrc) (I : RelFOInterpretation Lsrc L₂ T d) : RelFOInterpretation Lsrc (L₂.sum FirstOrder.Language.order) T d

Extension of a relativized interpretation with the lexicographic order on tagged tuples, the comparison formula being read through a vocabulary map of the source: this is DescriptiveComplexity.RelFOInterpretation.ordExtendRel where the source is not the ordered expansion itself but an expansion of it, as happens when the interpretation reads an induction over the ordered base.

Equations

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

@[instance_reducible]

noncomputable def DescriptiveComplexity.RelFOInterpretation.mapRelLinearOrderSrc {Lsrc L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : RelFOInterpretation Lsrc L₂ T d) {A : Type} [LinearOrder A] (instS : Lsrc.Structure A) : LinearOrder (I.MapRel A)

The lexicographic linear order on the interpreted universe of an interpretation with an arbitrary source vocabulary: as DescriptiveComplexity.RelFOInterpretation.mapRelLinearOrder, of which this is the generalization the composition needs.

Equations

• I.mapRelLinearOrderSrc instS = LinearOrder.lift' Subtype.val ⋯

noncomputable def DescriptiveComplexity.RelFOInterpretation.ordExtendSrcLEquiv {L₁ Lsrc L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] {d : ℕ} (φ : L₁.sum FirstOrder.Language.order →ᴸ Lsrc) (I : RelFOInterpretation Lsrc L₂ T d) {A : Type} [L₁.Structure A] [LinearOrder A] (instS : Lsrc.Structure A) (hexp : φ.IsExpansionOn A) : (L₂.sum FirstOrder.Language.order).Equiv ((ordExtendSrc φ I).MapRel A) (I.MapRel A)

The order-extended interpretation produces exactly the interpreted structure equipped with the lexicographic order, restricted to the domain.

Equations

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

Composition of FO(LFP) interpretations

noncomputable def DescriptiveComplexity.LFPInterpretation.comp {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] {d₁ d₂ : ℕ} (J : LFPInterpretation L₂ L₃ Tag₂ d₂) (I : LFPInterpretation L₁ L₂ Tag₁ d₁) : LFPInterpretation L₁ L₃ (Tag₂ × (Fin d₂ → Tag₁)) (d₂ * d₁)

The composite of two FO(LFP) interpretations: the two inductions are stratified – the inner one first, then the outer one pulled back through the inner interpretation – and the two interpretations compose with the guarded pullback, read over the stratified block.

Equations

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

noncomputable def DescriptiveComplexity.LFPInterpretation.compLEquiv {L₁ L₂ L₃ : FirstOrder.Language} [L₂.IsRelational] [L₃.IsRelational] {Tag₁ Tag₂ : Type} [Finite Tag₁] {d₁ d₂ : ℕ} (J : LFPInterpretation L₂ L₃ Tag₂ d₂) (I : LFPInterpretation L₁ L₂ Tag₁ d₁) (A : Type) [L₁.Structure A] [Finite A] : L₃.Equiv ((J.comp I).Map A) (J.Map (I.Map A))

The composite interpretation produces the twice-interpreted structure. This is the substitution property of FO(LFP): what the composite computes in one induction and one layer of formulas is what the two interpretations compute in sequence.

Equations

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

The order of the interpreted structure

noncomputable def DescriptiveComplexity.LFPInterpretation.ordExtend {L₁ L₂ : FirstOrder.Language} {T : Type} [LinearOrder T] {d : ℕ} (I : LFPInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) : LFPInterpretation (L₁.sum FirstOrder.Language.order) (L₂.sum FirstOrder.Language.order) T d

Extension of an FO(LFP) interpretation over an ordered base to one whose target carries the order vocabulary, interpreted by the lexicographic order on tagged tuples. The induction is unchanged; the comparison formula is read over the base expanded by its block.

Equations

• I.ordExtend = { ind := I.ind, toRel := DescriptiveComplexity.RelFOInterpretation.ordExtendSrc FirstOrder.Language.LHom.sumInl I.toRel }

@[instance_reducible]

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

The lexicographic linear order on the universe interpreted by an FO(LFP) interpretation.

Equations

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

noncomputable def DescriptiveComplexity.LFPInterpretation.ordExtendLEquiv {L₁ L₂ : FirstOrder.Language} [L₂.IsRelational] {T : Type} [LinearOrder T] {d : ℕ} (I : LFPInterpretation (L₁.sum FirstOrder.Language.order) L₂ T d) (A : Type) [L₁.Structure A] [LinearOrder A] : (L₂.sum FirstOrder.Language.order).Equiv (I.ordExtend.Map A) (I.Map A)

The order-extended interpretation produces exactly the interpreted structure equipped with the lexicographic order.

Equations

• I.ordExtendLEquiv A = DescriptiveComplexity.RelFOInterpretation.ordExtendSrcLEquiv FirstOrder.Language.LHom.sumInl I.toRel (I.expStructure A) ⋯

Transitivity

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

Transitivity of FO(LFP) reductions: if P ≤ˡᶠᵖ Q and Q ≤ˡᶠᵖ R, then P ≤ˡᶠᵖ R. The two inductions are stratified into one, the interpretations compose, and the intermediate structure is ordered lexicographically – the same three ingredients as DescriptiveComplexity.RelOrderedFOReduction.trans, plus the stratification that is this notion's own.

Equations

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

@[instance_reducible]

noncomputable instance DescriptiveComplexity.instTransDecisionProblemLFPReduction {L₁ L₂ L₃ : FirstOrder.Language} [L₁.IsRelational] [L₂.IsRelational] [L₃.IsRelational] : Trans LFPReduction LFPReduction LFPReduction

Trans instance for FO(LFP) reductions, enabling calc chains.

Equations

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