First-order interpretations and FO reductions

Complexity theory is essentially absent from Mathlib because formalizing a machine model of computation (and resource bounds on it) is hard. However, many classical NP-hardness reductions do not need the full power of polynomial-time computation: the reduction is first-order expressible – the output structure can be described by fixed first-order formulas evaluated in the input structure. Such FO reductions are computable in AC⁰ ⊆ LOGSPACE ⊆ PTIME, so exhibiting an FO reduction is (much) stronger than exhibiting a Karp reduction (Karp 1972), while being completely machine-model-free and therefore easy to formalize on top of Mathlib's ModelTheory library.

This file defines:

• DescriptiveComplexity.DecisionProblem L: a “problem” over the vocabulary L, i.e. a property of L-structures;
• DescriptiveComplexity.FOInterpretation L L' Tag dim: a tagged, dim-dimensional first-order interpretation of a relational language L' in a language L, mapping every L-structure A to an L'-structure I.Map A with universe Tag × (Fin dim → A);
• DescriptiveComplexity.FOInterpretation.IsQuantifierFree: interpretations all of whose defining formulas are quantifier-free (an even weaker reduction notion);
• DescriptiveComplexity.FOReduction P Q: an FO reduction from problem P to problem Q, i.e. an interpretation mapping yes-instances of P exactly to yes-instances of Q.

Design notes

The textbook notion of FO reduction maps a structure A to a structure with universe a definable subset of A^k, using a linear order on A to encode constantly many “sorts” of elements. To stay order-free and subset-free we instead tag tuples with elements of a finite type Tag, and use the full universe Tag × A^dim: junk elements are harmless in practice because the defining formulas can exclude them from all relations. Every tagged interpretation can be converted into a textbook k-ary FO reduction on ordered structures (using the order to encode constantly many tags), so the notion formalized here is a genuine form of FO reducibility.

The universe of I.Map A is Tag × (Fin dim → A), which is finite whenever A and Tag are (FOInterpretation.map_finite): FO reductions map finite structures to finite structures, as required for reductions between decision problems on finite structures.

Following the usual convention of finite model theory, reductions are only required to be correct on nonempty structures (and their tag types are required to be nonempty, so that nonempty structures map to nonempty structures). Empty structures are degenerate: no fixed-dimension interpretation can produce a nonempty structure from an empty one, so e.g. no problem that is false on an empty structure could reduce to SAT (whose empty instance is trivially satisfiable), and hardness results would fail for spurious reasons.

structure DescriptiveComplexity.DecisionProblem (L : FirstOrder.Language) : Type 1

A decision problem in the sense of descriptive complexity: an isomorphism-closed property of L-structures, whose yes-instances are the L-structures satisfying it. Isomorphism-invariance is part of the notion – a decision problem cannot distinguish isomorphic presentations of the same structure.

• Holds (A : Type) [L.Structure A] : Prop

  The predicate: P A (through the function coercion) states that the structure A is a yes-instance.

• iso_invariant {A B : Type} [L.Structure A] [L.Structure B] : ∀ (a : L.Equiv A B), self.Holds A ↔ self.Holds B

  Decision problems do not distinguish isomorphic structures.

@[instance_reducible]

instance DescriptiveComplexity.DecisionProblem.instCoeFunForallForallStructureProp {L : FirstOrder.Language} : CoeFun (DecisionProblem L) fun (x : DecisionProblem L) => (A : Type) → [L.Structure A] → Prop

Equations

• DescriptiveComplexity.DecisionProblem.instCoeFunForallForallStructureProp = { coe := DescriptiveComplexity.DecisionProblem.Holds }

theorem DescriptiveComplexity.DecisionProblem.ext {L : FirstOrder.Language} {P Q : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A], P.Holds A ↔ Q.Holds A) : P = Q

theorem DescriptiveComplexity.DecisionProblem.ext_iff {L : FirstOrder.Language} {P Q : DecisionProblem L} : P = Q ↔ ∀ (A : Type) [inst : L.Structure A], P.Holds A ↔ Q.Holds A

Transport of relations along isomorphisms

Proving the iso_invariant field of a DecisionProblem always starts the same way: the semantic property is phrased in terms of RelMap r ![a] / RelMap r ![a, b], and one must know that these transport along an L-isomorphism. The two lemmas below package this step once and for all (Mathlib's StrongHomClass.map_rel states it with e ∘ ![a, b], which must first be normalized to ![e a, e b]).

theorem DescriptiveComplexity.relMap_equiv₁ {L : FirstOrder.Language} {A B : Type} [L.Structure A] [L.Structure B] (e : L.Equiv A B) (r : L.Relations 1) (a : A) : FirstOrder.Language.Structure.RelMap r ![a] ↔ FirstOrder.Language.Structure.RelMap r ![e a]

A unary relation transports along an L-isomorphism.

theorem DescriptiveComplexity.relMap_equiv₂ {L : FirstOrder.Language} {A B : Type} [L.Structure A] [L.Structure B] (e : L.Equiv A B) (r : L.Relations 2) (a b : A) : FirstOrder.Language.Structure.RelMap r ![a, b] ↔ FirstOrder.Language.Structure.RelMap r ![e a, e b]

A binary relation transports along an L-isomorphism.

theorem DescriptiveComplexity.relMap_equiv₃ {L : FirstOrder.Language} {A B : Type} [L.Structure A] [L.Structure B] (e : L.Equiv A B) (r : L.Relations 3) (a b c : A) : FirstOrder.Language.Structure.RelMap r ![a, b, c] ↔ FirstOrder.Language.Structure.RelMap r ![e a, e b, e c]

A ternary relation transports along an L-isomorphism.

theorem DescriptiveComplexity.realize_rel₃ {L : FirstOrder.Language} {α M : Type} [L.Structure M] {R : L.Relations 3} {t₁ t₂ t₃ : L.Term α} {v : α → M} : (R.formula ![t₁, t₂, t₃]).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂, FirstOrder.Language.Term.realize v t₃]

Realization of an atom of arity 3, the shape Mathlib's Formula.realize_rel₁ and Formula.realize_rel₂ stop short of.

theorem DescriptiveComplexity.realize_rel₄ {L : FirstOrder.Language} {α M : Type} [L.Structure M] {R : L.Relations 4} {t₁ t₂ t₃ t₄ : L.Term α} {v : α → M} : (R.formula ![t₁, t₂, t₃, t₄]).Realize v ↔ FirstOrder.Language.Structure.RelMap R ![FirstOrder.Language.Term.realize v t₁, FirstOrder.Language.Term.realize v t₂, FirstOrder.Language.Term.realize v t₃, FirstOrder.Language.Term.realize v t₄]

Realization of an atom of arity 4.

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

A tagged dim-dimensional first-order interpretation of the relational language L' in the language L. It maps an L-structure A to the L'-structure with universe Tag × A^dim in which an n-ary relation symbol R holds of tagged tuples (t₁, ā₁), …, (tₙ, āₙ) iff the first-order L-formula relFormula R (t₁, …, tₙ) – whose free variable (i, j) stands for the j-th coordinate āᵢ j of the i-th argument – holds in A.

• relFormula {n : ℕ} : L'.Relations n → (Fin n → Tag) → L.Formula (Fin n × Fin dim)

  The defining L-formula of each relation symbol of L', for each tuple of tags; the free variable (i, j) is the j-th coordinate of the i-th argument tuple.

def DescriptiveComplexity.FOInterpretation.Map {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (_I : FOInterpretation L L' Tag dim) (A : Type) : Type

The universe of the structure interpreted in A: tagged dim-tuples.

This is a plain def (not an abbrev) so that the L'.Structure instance on it can be found by instance search, while rcases-style destructuring still sees through it.

Equations

• _I.Map A = (Tag × (Fin dim → A))

@[instance_reducible]

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

The L'-structure interpreted in the L-structure A.

Equations

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

theorem DescriptiveComplexity.FOInterpretation.relMap_map {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : FOInterpretation L L' Tag dim) (A : Type) [L.Structure A] [L'.IsRelational] {n : ℕ} (R : L'.Relations n) (xs : Fin n → I.Map A) : FirstOrder.Language.Structure.RelMap R xs ↔ (I.relFormula R fun (i : Fin n) => (xs i).1).Realize fun (p : Fin n × Fin dim) => (xs p.1).2 p.2

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

FO interpretations map finite structures to finite structures.

theorem DescriptiveComplexity.FOInterpretation.map_nonempty {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : FOInterpretation L L' Tag dim) (A : Type) [Nonempty Tag] [Nonempty A] : Nonempty (I.Map A)

FO interpretations with nonempty tags map nonempty structures to nonempty structures.

def DescriptiveComplexity.FOInterpretation.IsQuantifierFree {L L' : FirstOrder.Language} {Tag : Type} {dim : ℕ} (I : FOInterpretation L L' Tag dim) : Prop

An interpretation is quantifier-free if all its defining formulas are. Quantifier-free reductions are the weakest reduction notion in common use in descriptive complexity; SAT remains NP-complete under them.

Equations

• I.IsQuantifierFree = ∀ {n : ℕ} (R : L'.Relations n) (t : Fin n → Tag), FirstOrder.Language.BoundedFormula.IsQF (I.relFormula R t)

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

A first-order reduction from the problem P (on L-structures) to the problem Q (on L'-structures): a first-order interpretation mapping yes-instances of P exactly to yes-instances of Q.

Since FO interpretations are computable in AC⁰ ⊆ PTIME on (encodings of) finite structures, an FOReduction P Q is in particular a Karp reduction from P to Q: any NP-hardness argument for P transfers to Q, without any formalized machine model.

• Tag : Type

  The tags (copies of A^dim) used by the underlying interpretation.

• tagFinite : Finite self.Tag

  Tags are finite, so that finite structures map to finite structures.

• tagNonempty : Nonempty self.Tag

  Tags are nonempty, so that nonempty structures map to nonempty structures.

• dim : ℕ

  The dimension of the underlying interpretation.

• toInterpretation : FOInterpretation L L' self.Tag self.dim

  The underlying first-order interpretation.

• correct (A : Type) [L.Structure A] [Finite A] [Nonempty A] : P.Holds A ↔ Q.Holds (self.toInterpretation.Map A)

  Yes-instances map exactly to yes-instances, on the finite nonempty structures: membership and hardness read a problem only there (DescriptiveComplexity.ComplexityClass), so asking anything of the infinite ones would be an obligation nothing consumes. The ordered and relativized notions restrict the same way.

def DescriptiveComplexity.«term_≤ᶠᵒ_» : Lean.TrailingParserDescr

A first-order reduction from the problem P (on L-structures) to the problem Q (on L'-structures): a first-order interpretation mapping yes-instances of P exactly to yes-instances of Q.

Since FO interpretations are computable in AC⁰ ⊆ PTIME on (encodings of) finite structures, an FOReduction P Q is in particular a Karp reduction from P to Q: any NP-hardness argument for P transfers to Q, without any formalized machine model.

Equations

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

def DescriptiveComplexity.FOInterpretation.mapEquivSelf {L L' : FirstOrder.Language} (I : FOInterpretation L L' Unit 1) (A : Type) : I.Map A ≃ A

For a one-dimensional interpretation with a single tag, the interpreted universe is equivalent, as a plain type, to the original universe.

Equations

• I.mapEquivSelf A = { toFun := fun (x : I.Map A) => x.2 0, invFun := fun (a : A) => ((), fun (x : Fin 1) => a), left_inv := ⋯, right_inv := ⋯ }

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

Interpretations are functorial on isomorphisms: an L-isomorphism of the base structures induces an L'-isomorphism of the interpreted structures.

Equations

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