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 polynomial time – lives in DescriptiveComplexity.Hierarchy; the Cook–Levin theorem ([Cook 1971][cook1971complexity]; [Levin 1973][levin1973universal]) 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⁰.

Hardness is a field of its own rather than a function of Mem: the naive “every member reduces to P” cannot even be stated here, since a reduction has a relational target while Hard ranges over arbitrary vocabularies. The classes of this library take it to be cofinal hardness for their own members and are built by DescriptiveComplexity.ComplexityClass.ofMem, which supplies both that reading of Hard and the three closure proofs it needs; keeping the field abstract leaves room for the two that read hardness differently (DescriptiveComplexity.ComplexityClass.empty, DescriptiveComplexity.PH).

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

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

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

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

• mem_of_foReduction {L L' : FirstOrder.Language} [L.IsRelational] [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] [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] [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] [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] [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} [L.IsRelational] {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} [L.IsRelational] {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} [inst : L.IsRelational] (P : DecisionProblem L), C₁.Mem P ↔ C₂.Mem P) (hHard : ∀ {L : FirstOrder.Language} [inst : L.IsRelational] (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 stands for a level of a hierarchy that has no logical characterization.

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} [L.IsRelational] (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} [L.IsRelational] {P : DecisionProblem L} (h : C.Complete P) : C.Mem P

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

def DescriptiveComplexity.DecisionProblem.compl {L : FirstOrder.Language} [L.IsRelational] (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} [L.IsRelational] : Compl (DecisionProblem L)

Equations

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

@[simp]

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

def DescriptiveComplexity.FOReduction.compl {L L' : FirstOrder.Language} [L.IsRelational] [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] [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 := ⋯ }

Home · Documentation · Publications · Contributors · Source · Cite