Abstract complexity classes, the polynomial hierarchy, and NP-completeness

Complexity classes are introduced abstractly: a ComplexityClass assigns to decision problems (over arbitrary vocabularies) a membership predicate and a hardness predicate, and is required to be closed under (ordered) first-order reductions – membership downward (P ≤ᶠᵒ Q and Q ∈ 𝒞 give P ∈ 𝒞), hardness upward (P ≤ᶠᵒ Q and P 𝒞-hard give Q 𝒞-hard). Since FO reductions are computable in AC⁰ ⊆ LOGSPACE ⊆ PTIME, every class from LOGSPACE up is closed in this sense, so this is a mild requirement. Note that closure must be part of the definition of a complexity class rather than an axiom quantified over all classes: arbitrary collections of problems need not be closed, and the quantified axiom would be inconsistent.

This file also defines the complement of a decision problem (DecisionProblem.compl, notation Pᶜ), and the observation that a reduction complements: the same interpretation reduces Pᶜ to Qᶜ (DescriptiveComplexity.FOReduction.compl).

The polynomial hierarchy itself – DescriptiveComplexity.SigmaP/DescriptiveComplexity.PiP, with levels k ≥ 1 defined by second-order quantifier alternation and level 0 left as an empty placeholder – lives in DescriptiveComplexity.Hierarchy; the Cook–Levin theorem (Cook 1971; Levin 1973) lives with the problem SAT in DescriptiveComplexity.Problems.Sat, and completeness theorems for other problems in their files under DescriptiveComplexity/Problems/ (e.g. DescriptiveComplexity.threeCol_NP_complete in DescriptiveComplexity.Problems.ThreeColorability).

structure DescriptiveComplexity.ComplexityClass : Type 1

An abstract complexity class: a collection of decision problems (its Membership predicate) together with a Hardness predicate, closed under (ordered) first-order reductions. Both predicates are left completely abstract; the closure requirements are sound for every class containing LOGSPACE, since (ordered) FO reductions are computable in AC⁰.

• Mem {L : FirstOrder.Language} : DecisionProblem L → Prop

  The problems belonging to the class. Use the notation P ∈ 𝒞.

• Hard {L : FirstOrder.Language} : DecisionProblem L → Prop

  The problems every problem of the class reduces to (“𝒞-hard”).

• mem_of_foReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} : ∀ (a : FOReduction P Q), self.Mem Q → self.Mem P

  Membership travels backward along FO reductions.

• hard_of_foReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} : ∀ (a : FOReduction P Q), self.Hard P → self.Hard Q

  Hardness travels forward along FO reductions.

• mem_of_orderedReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} : ∀ (a : OrderedFOReduction P Q), self.Mem Q → self.Mem P

  Membership travels backward along ordered FO reductions.

• hard_of_orderedReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} : ∀ (a : OrderedFOReduction P Q), self.Hard P → self.Hard Q

  Hardness travels forward along ordered FO reductions.

• hard_of_relOrderedReduction {L L' : FirstOrder.Language} [L'.IsRelational] {P : DecisionProblem L} {Q : DecisionProblem L'} : ∀ (a : RelOrderedFOReduction P Q), self.Hard P → self.Hard Q

  Hardness travels forward along relativized ordered FO reductions – the reductions with a definable target universe, needed for spanning problems.

• mem_congr_finite {L : FirstOrder.Language} {P Q : DecisionProblem L} : (∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) → (self.Mem P ↔ self.Mem Q)

  Complexity classes speak about finite instances only: membership does not depend on the behavior of a problem on infinite structures.

• hard_congr_finite {L : FirstOrder.Language} {P Q : DecisionProblem L} : (∀ (A : Type) [inst : L.Structure A] [Finite A], P.Holds A ↔ Q.Holds A) → (self.Hard P ↔ self.Hard Q)

  Hardness, too, only depends on the finite instances of a problem.

def DescriptiveComplexity.«term_∈_» : Lean.TrailingParserDescr

P ∈ 𝒞: the problem P belongs to the complexity class 𝒞. (This overloads the ∈ notation; the Membership class cannot be used here since the element type DecisionProblem L is not determined by ComplexityClass.)

Equations

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

theorem DescriptiveComplexity.ComplexityClass.ext {C₁ C₂ : ComplexityClass} (hMem : ∀ {L : FirstOrder.Language} (P : DecisionProblem L), C₁.Mem P ↔ C₂.Mem P) (hHard : ∀ {L : FirstOrder.Language} (P : DecisionProblem L), C₁.Hard P ↔ C₂.Hard P) : C₁ = C₂

Two complexity classes with the same members and the same hard problems are equal: the remaining fields are proofs.

def DescriptiveComplexity.ComplexityClass.empty : ComplexityClass

The empty complexity class: no members, and every problem vacuously hard (there is nothing that would have to reduce to it). It is a placeholder for levels of a hierarchy that are not (yet) characterized logically.

Equations

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

@[instance_reducible]

instance DescriptiveComplexity.ComplexityClass.instHasSubset : HasSubset ComplexityClass

Inclusion of complexity classes.

Equations

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

def DescriptiveComplexity.ComplexityClass.Complete (C : ComplexityClass) {L : FirstOrder.Language} (P : DecisionProblem L) : Prop

A problem is complete for a class if it belongs to it and is hard for it.

Equations

• C.Complete P = (C.Mem P ∧ C.Hard P)

theorem DescriptiveComplexity.ComplexityClass.Complete.mem (C : ComplexityClass) {L : FirstOrder.Language} {P : DecisionProblem L} (h : C.Complete P) : C.Mem P

theorem DescriptiveComplexity.ComplexityClass.Complete.hard (C : ComplexityClass) {L : FirstOrder.Language} {P : DecisionProblem L} (h : C.Complete P) : C.Hard P

def DescriptiveComplexity.DecisionProblem.compl {L : FirstOrder.Language} (P : DecisionProblem L) : DecisionProblem L

The complement of a decision problem: its yes-instances are the no-instances of P.

Equations

• P.compl = { Holds := fun (A : Type) (inst : L.Structure A) => ¬P.Holds A, iso_invariant := ⋯ }

@[instance_reducible]

instance DescriptiveComplexity.instComplDecisionProblem {L : FirstOrder.Language} : Compl (DecisionProblem L)

Equations

• DescriptiveComplexity.instComplDecisionProblem = { compl := DescriptiveComplexity.DecisionProblem.compl }

@[simp]

theorem DescriptiveComplexity.DecisionProblem.compl_compl {L : FirstOrder.Language} (P : DecisionProblem L) : Pᶜᶜ = P

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

Reductions complement: the very same interpretation reduces Pᶜ to Qᶜ, since the correctness of a reduction is an equivalence. This is what turns a hardness discharge for a Σ-level into one for the dual Π-level; see DescriptiveComplexity.taut_hard_of_piSODefinable.

Equations

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

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

Reductions complement: the very same interpretation reduces Pᶜ to Qᶜ, since the correctness of a reduction is an equivalence. This is what turns a hardness discharge for a Σ-level into one for the dual Π-level; see DescriptiveComplexity.taut_hard_of_piSODefinable.

Equations

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