The exponential of a complexity class

DescriptiveComplexity.ComplexityClass.exp reads a class over the expanded universe: P ∈ C.exp when there is an exponential expansion X and a problem Q ∈ C such that P holds of A exactly when Q holds of X.Map A. Since the expanded universe of a size-n structure has 2^(n^a) points, a resource bound read there is one exponential higher than the same bound read on A. This is the succinctness upgrade – trivial properties of circuit-described graphs become NP-complete (Galperin–Wigderson 1983), NP-complete properties become NEXPTIME-complete (Papadimitriou–Yannakakis 1986), and the general statement is Veith 1998 – stated as an operator rather than as a theorem about one problem at a time.

The operator is applied to an abstract DescriptiveComplexity.ComplexityClass, and that is the whole point of the design: the complement equalities, the inclusions and the completeness transfers of the exponential classes are then inherited from their polynomial-level counterparts instead of being reproved.

That ExpDefinable C is closed under (ordered) first-order reductions – so that C.exp is a class at all – is DescriptiveComplexity.ExpExpansion.pullOrdered: an interpretation followed by an expansion is an expansion. Nothing about C is used, which is why the closure holds at an arbitrary class.

Cofinal hardness only sees the membership predicate

theorem DescriptiveComplexity.cofinalHard_congr_mem {Mem Mem' : {L₀ : FirstOrder.Language} → [inst : L₀.IsRelational] → DecisionProblem L₀ → Prop} (h : ∀ {L₀ : FirstOrder.Language} [inst : L₀.IsRelational] (Q : DecisionProblem L₀), Mem Q ↔ Mem' Q) {L : FirstOrder.Language} [L.IsRelational] (P : DecisionProblem L) : CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem) P ↔ CofinalHard (fun {L₀ : FirstOrder.Language} [L₀.IsRelational] => Mem') P

Cofinal hardness depends on the membership predicate only up to pointwise equivalence. Needed to compare the hardness halves of two classes built by DescriptiveComplexity.ComplexityClass.ofMem from equivalent membership predicates, as DescriptiveComplexity.ComplexityClass.exp_compl does.

Definability over an expanded universe

def DescriptiveComplexity.ExpDefinable {L : FirstOrder.Language} [L.IsRelational] (C : ComplexityClass) (P : DecisionProblem L) : Prop

Definability over an expanded universe: the problem P is C-definable one exponential up when some exponential expansion X turns it into a problem of C – P holds of A exactly when a fixed Q ∈ C holds of X.Map A.

Equations

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

theorem DescriptiveComplexity.expDefinable_congr {L : FirstOrder.Language} [L.IsRelational] {C : ComplexityClass} {P P' : DecisionProblem L} (h : ∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ P'.Holds A) : ExpDefinable C P ↔ ExpDefinable C P'

Definability over an expanded universe only depends on the finite instances of a problem.

theorem DescriptiveComplexity.ExpDefinable.of_orderedReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : ComplexityClass} {P : DecisionProblem L} {Q : DecisionProblem L'} (f : OrderedFOReduction P Q) (h : ExpDefinable C Q) : ExpDefinable C P

Closure under ordered first-order reductions: the interpretation of the reduction, followed by the expansion witnessing Q, is again an expansion.

theorem DescriptiveComplexity.ExpDefinable.of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [L'.IsRelational] {C : ComplexityClass} {P : DecisionProblem L} {Q : DecisionProblem L'} (f : FOReduction P Q) (h : ExpDefinable C Q) : ExpDefinable C P

Closure under first-order reductions.

The exponential of a class

noncomputable def DescriptiveComplexity.ComplexityClass.exp (C : ComplexityClass) : ComplexityClass

The exponential of a complexity class: the problems that become members of C when read over an exponentially larger, definable universe. Hardness is cofinal hardness for that membership predicate, as for every class of this library.

Equations

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

@[simp]

theorem DescriptiveComplexity.ComplexityClass.mem_exp {L : FirstOrder.Language} [L.IsRelational] (C : ComplexityClass) (P : DecisionProblem L) : C.exp.Mem P ↔ ExpDefinable C P

theorem DescriptiveComplexity.ComplexityClass.exp_mono {C D : ComplexityClass} (h : C ⊆ D) : C.exp ⊆ D.exp

The exponential is monotone.

theorem DescriptiveComplexity.ComplexityClass.exp_compl (C : ComplexityClass) : C.compl.exp = C.exp.compl

The exponential commutes with complementation: complementing before or after the expansion is the same thing, since the expansion is applied to the instance and complementation to the answer.

This is what makes EXPTIME = coEXPTIME and EXPSPACE = coEXPSPACE consequences of the corresponding polynomial-level facts rather than theorems in their own right.