Ordered first-order reductions

Textbook FO reductions (Immerman 1999, Descriptive Complexity, ch. 3) operate on ordered finite structures: the input structure comes with a linear order on its universe, which the defining formulas may mention. The order is essential for many reductions: e.g. reducing SAT to 3-colorability threads an OR-gadget chain along the order of each clause's literals, which no order-free first-order interpretation can express.

This file provides the ordered variant of DescriptiveComplexity.FOReduction:

• an (L.sum Language.order).Structure instance on any linearly ordered L-structure, realizing the extra binary symbol leSymb as ≤;
• DescriptiveComplexity.OrderedFOReduction P Q: a first-order interpretation of L' in the ordered expansion L.sum Language.order, mapping yes-instances of P exactly to yes-instances of Q – for every finite linearly ordered input structure. Finiteness matters: gadget constructions traverse the order and need minima, maxima and successors.

Since the problem P does not mention the order and correctness is required for every linear order on the input structure, an OrderedFOReduction is what descriptive complexity calls an order-invariant FO reduction.

@[instance_reducible]

instance DescriptiveComplexity.sumOrderStructure (L : FirstOrder.Language) (A : Type) [L.Structure A] [LE A] : (L.sum FirstOrder.Language.order).Structure A

A linearly ordered L-structure is a structure over the ordered expansion L.sum Language.order, interpreting the order symbol as ≤.

Equations

• DescriptiveComplexity.sumOrderStructure L A = inferInstance

instance DescriptiveComplexity.instOrderedStructureSumOrder_descriptiveComplexity (L : FirstOrder.Language) (A : Type) [L.Structure A] [LE A] : (L.sum FirstOrder.Language.order).OrderedStructure A

@[simp]

theorem DescriptiveComplexity.relMap_sumInl {L : FirstOrder.Language} {A : Type} [L.Structure A] [LE A] {n : ℕ} (r : L.Relations n) (x : Fin n → A) : FirstOrder.Language.Structure.RelMap (Sum.inl r) x ↔ FirstOrder.Language.Structure.RelMap r x

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

An ordered first-order reduction from the problem P (on L-structures) to the problem Q (on L'-structures): a first-order interpretation over the ordered expansion of L that maps yes-instances of P exactly to yes-instances of Q, for every finite linearly ordered input structure.

As P does not depend on the order, correctness for every linear order makes this an order-invariant FO reduction; it is computable in AC⁰ ⊆ PTIME on (encodings of) finite ordered structures, hence in particular a Karp reduction.

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

  The underlying first-order interpretation, over the ordered expansion.

• 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 ordered first-order reduction from the problem P (on L-structures) to the problem Q (on L'-structures): a first-order interpretation over the ordered expansion of L that maps yes-instances of P exactly to yes-instances of Q, for every finite linearly ordered input structure.

As P does not depend on the order, correctness for every linear order makes this an order-invariant FO reduction; it is computable in AC⁰ ⊆ PTIME on (encodings of) finite ordered structures, hence in particular a Karp reduction.

Equations

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