FO(LFP) reductions: the polynomial-time reductions of a machine-free library

A first-order reduction (DescriptiveComplexity.FOReduction and its ordered and relativized variants) is computable in AC⁰; the textbook notion of reduction for the classes from PTIME up is the polynomial-time one. In a library without machines, a polynomial-time reduction is an interpretation whose defining formulas belong to a logic capturing PTIME: Immerman's FO(LFP) reductions (Immerman 1999, ch. 3). This file defines them, and embeds every first-order reduction notion of the library into them – the statement that a first-order reduction is in particular a polynomial-time one.

The notion

A DescriptiveComplexity.LFPInterpretation is a relativized first-order interpretation (DescriptiveComplexity.RelFOInterpretation) whose formulas may read, beside the symbols of the base structure, the relations computed by a simultaneous inflationary induction over it (DescriptiveComplexity.StepDef, the library's normal form for FO(≤, IFP) = FO(LFP) = PTIME on ordered structures). The induction is computed once, its value expands the base structure (DescriptiveComplexity.LFPInterpretation.expStructure), and the interpretation is read over the expansion. This is the clausal normal form Immerman's reductions take: one fixed point, then first-order formulas.

Two design points.

• The base vocabulary is a parameter. An LFPInterpretation L L' reads an induction over L itself; the ordered reduction notion instantiates L with the ordered expansion L.sum Language.order. Keeping the base free is what lets the closure theorems be proved once, by an induction on quantifier blocks, and specialized to the ordered reading at the end.
• The interpretation is relativized (it carries a domain formula). The library's hardness travels along relativized reductions ≤ʳᶠᵒ[≤], and a relativized reduction cannot be turned into a whole-universe one – junk points cannot be dropped – so a polynomial-time notion that did not carry a domain formula would not contain the library's own hardness. Classically a polynomial-time reduction may output an instance of any size, and the domain formula is what stands for that freedom here.

DescriptiveComplexity.LFPReduction P Q, notation P ≤ˡᶠᵖ Q, is an ordered LFPInterpretation mapping yes-instances exactly to yes-instances, for every linear order on the input – order-invariance, exactly as for DescriptiveComplexity.OrderedFOReduction.

The embeddings

DescriptiveComplexity.RelOrderedFOReduction.toLFP (and the two variants OrderedFOReduction.toLFP, FOReduction.toLFP) read a first-order reduction as an FO(LFP) reduction with no induction at all: every first-order reduction is a polynomial-time reduction. The converse fails, and provably so: DescriptiveComplexity.exists_lfpReduction_not_orderedReduction (DescriptiveComplexity.FixedPointReductionStrict) exhibits a target to which EVEN reduces in FO(LFP) but not in FO(≤).

What is proved elsewhere

• transitivity, DescriptiveComplexity.LFPReduction.trans (DescriptiveComplexity.FixedPointReductionComposition);
• closure of PTIME, NP and coNP under ≤ˡᶠᵖ, and hardness stated with it – implied by the library's own hardness (DescriptiveComplexity.FixedPointReductionClosure).

Lifting a relativized interpretation along a vocabulary map of its source

def DescriptiveComplexity.RelFOInterpretation.liftSource {L₀ L₁ L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (φ : L₀ →ᴸ L₁) (I : RelFOInterpretation L₀ L' Tag dim) : RelFOInterpretation L₁ L' Tag dim

A relativized interpretation read over a larger source vocabulary: every formula is transported along the vocabulary map.

Equations

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

theorem DescriptiveComplexity.RelFOInterpretation.realize_liftSource_domFormula {L₀ L₁ L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (φ : L₀ →ᴸ L₁) (I : RelFOInterpretation L₀ L' Tag dim) {A : Type} {inst₀ : L₀.Structure A} {inst₁ : L₁.Structure A} (hexp : φ.IsExpansionOn A) (t : Tag) (w : Fin dim → A) : ((liftSource φ I).domFormula t).Realize w ↔ (I.domFormula t).Realize w

def DescriptiveComplexity.RelFOInterpretation.liftSourceLEquiv {L₀ L₁ L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (φ : L₀ →ᴸ L₁) (I : RelFOInterpretation L₀ L' Tag dim) {A : Type} {inst₀ : L₀.Structure A} {inst₁ : L₁.Structure A} [L'.IsRelational] (hexp : φ.IsExpansionOn A) : L'.Equiv ((liftSource φ I).MapRel A) (I.MapRel A)

On a structure that is an expansion along the vocabulary map, the lifted interpretation produces the same structure as the original one: the identity on tagged tuples is an isomorphism.

Equations

• DescriptiveComplexity.RelFOInterpretation.liftSourceLEquiv φ I hexp = { toEquiv := (Equiv.refl (Tag × (Fin dim → A))).subtypeEquiv ⋯, map_fun' := ⋯, map_rel' := ⋯ }

The induction with no relation variables

def DescriptiveComplexity.StepDef.trivialDef (L : FirstOrder.Language) : StepDef L

The simultaneous induction with no relation variables at all: its value is the (unique) assignment of the trivial block, and its output is ⊤. The first-order reductions embed into the FO(LFP) ones through it.

Equations

• DescriptiveComplexity.StepDef.trivialDef L = { B := DescriptiveComplexity.SOBlock.trivial, step := fun (i : DescriptiveComplexity.SOBlock.trivial.ι) => nomatch i, out := ⊤ }

Interpretations reading a fixed point

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

An FO(LFP) interpretation: a relativized first-order interpretation whose formulas may read the value of a simultaneous inflationary induction over the base structure. The induction ind is computed first (its output sentence is not read); the interpretation toRel is then read over the base vocabulary expanded by the induction's relation variables.

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

• ind : StepDef L

  The induction whose value the formulas may read.

• toRel : RelFOInterpretation (L.sum self.ind.B.lang) L' Tag dim

  The interpretation, over the base vocabulary expanded by the block of the induction.

@[instance_reducible]

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

The base structure expanded by the value of the induction – the structure the interpretation is read over.

Equations

• I.expStructure A = I.ind.B.structure₁ (I.ind.inflLimit A)

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

The universe of the interpreted structure: the tagged tuples in the domain, the domain formula being read over the expanded structure.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.LFPInterpretation.mapStructure {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : LFPInterpretation 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.LFPInterpretation.map_finite {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : LFPInterpretation L L' Tag dim) (A : Type) [L.Structure A] [Finite Tag] [Finite A] : Finite (I.Map A)

def DescriptiveComplexity.LFPInterpretation.mapLEquiv {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : LFPInterpretation L L' Tag dim) [L'.IsRelational] {M N : Type} [L.Structure M] [L.Structure N] (e : L.Equiv M N) : L'.Equiv (I.Map M) (I.Map N)

FO(LFP) interpretations are functorial on isomorphisms: the value of the induction transports along the isomorphism (DescriptiveComplexity.StepDef.inflLimit_map), and a relativized interpretation is functorial.

Equations

• I.mapLEquiv e = I.toRel.mapRelLEquiv (⋯.mp (I.ind.B.extendEquiv' e (I.ind.inflLimit M)))

def DescriptiveComplexity.LFPInterpretation.pullProblem {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : LFPInterpretation L L' Tag dim) [L.IsRelational] [L'.IsRelational] (Q : DecisionProblem L') : DecisionProblem L

The pullback of a decision problem along an FO(LFP) interpretation: the structures the interpretation sends to yes-instances.

Equations

• I.pullProblem Q = { Holds := fun (A : Type) [L.Structure A] => Q.Holds (I.Map A), iso_invariant := ⋯ }

@[simp]

theorem DescriptiveComplexity.LFPInterpretation.pullProblem_apply {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : LFPInterpretation L L' Tag dim) [L.IsRelational] [L'.IsRelational] (Q : DecisionProblem L') (A : Type) [L.Structure A] : (I.pullProblem Q).Holds A ↔ Q.Holds (I.Map A)

With no induction, an FO(LFP) interpretation is a relativized one

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

A relativized interpretation, read as an FO(LFP) interpretation with the trivial induction.

Equations

• J.toLFP = { ind := DescriptiveComplexity.StepDef.trivialDef L, toRel := DescriptiveComplexity.RelFOInterpretation.liftSource FirstOrder.Language.LHom.sumInl J }

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

The FO(LFP) interpretation with the trivial induction produces exactly the structure of the relativized interpretation it lifts.

Equations

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

FO(LFP) reductions

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

An FO(LFP) reduction from P to Q – a polynomial-time reduction, in the logical form of Immerman 1999: an FO(LFP) interpretation over the ordered expansion of the source vocabulary, mapping yes-instances of P exactly to yes-instances of Q, for every finite linear order on the input. As for DescriptiveComplexity.OrderedFOReduction, the problem P does not see the order, so the reduction is order-invariant.

The interpretation is relativized, and the domain is required to be inhabited, as in DescriptiveComplexity.RelOrderedFOReduction.

• 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 : LFPInterpretation (L.sum FirstOrder.Language.order) L' self.Tag self.dim

  The underlying FO(LFP) 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(LFP) reduction from P to Q – a polynomial-time reduction, in the logical form of Immerman 1999: an FO(LFP) interpretation over the ordered expansion of the source vocabulary, mapping yes-instances of P exactly to yes-instances of Q, for every finite linear order on the input. As for DescriptiveComplexity.OrderedFOReduction, the problem P does not see the order, so the reduction is order-invariant.

The interpretation is relativized, and the domain is required to be inhabited, as in DescriptiveComplexity.RelOrderedFOReduction.

Equations

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

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

The same interpretation reduces Pᶜ to Qᶜ.

Equations

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

def DescriptiveComplexity.LFPReduction.congrSource {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} {P' : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ P'.Holds A) (f : LFPReduction P Q) : LFPReduction P' Q

An FO(LFP) reduction can be transported along an agreement of the source problems on finite structures.

Equations

• DescriptiveComplexity.LFPReduction.congrSource h f = { Tag := f.Tag, tagFinite := ⋯, dim := f.dim, toInterpretation := f.toInterpretation, map_nonempty := ⋯, correct := ⋯ }

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

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

A relativized ordered FO reduction is an FO(LFP) reduction with no induction: the first-order reductions the library's hardness travels along are in particular polynomial-time reductions.

Equations

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

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

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

Equations

• f.toLFP = f.toRel.toLFP

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

An FO reduction is an FO(LFP) reduction.

Equations

• f.toLFP = f.toOrdered.toRel.toLFP