The classes P, NP and coNP

15 fully proved

Bitstring encodings

ClassBitstring encodings#✓fully proved

A canonical bitstring encoding of a type \(\alpha\) consists of an encoding map from \(\alpha\) to finite lists of booleans and a partial decoding map from finite lists of booleans to \(\alpha\), such that decoding the encoding of any \(a \in \alpha\) succeeds and returns \(a\).

class BitstringEncoding α extends Computability.Encoding α Bool

Sources

a class version of Mathlib's Computability.Encoding specialized to the alphabet Bool, inlined from FormalConjectures (absent from Mathlib).

Used by 318

Bitstring Encoding

DefinitionEncoding function of a bitstring encoding#✓fully proved

For a type \(\alpha\) with a canonical bitstring encoding, the bitstring encoding of \(a \in \alpha\) is the finite list of booleans that this encoding assigns to \(a\).

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

Uses 1 · Used by 310

Statement usesBitstring encodings

DefinitionDecoding function of a bitstring encoding#✓fully proved

For a type \(\alpha\) with a canonical bitstring encoding, bitstring decoding is the decoding function of that encoding: it sends each finite list of booleans either to an element of \(\alpha\) or to failure.

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

Uses 1 · Used by 312

Statement usesBitstring encodings

TheoremDecoding inverts bitstring encoding#✓fully proved

Let \(\alpha\) be a type with a canonical bitstring encoding. For every \(a \in \alpha\), decoding the bitstring encoding of \(a\) succeeds and returns \(a\).

@[simp]
theorem bitDecode_bitEncode [BitstringEncoding α] (a : α) :
    bitDecode (bitEncode a) = some a

class BitstringEncoding α extends Computability.Encoding α Bool

MathlibExt/Computability/Complexity.lean:48

def bitDecode [BitstringEncoding α] (l : List Bool) : Option α := toEncoding.decode l

MathlibExt/Computability/Complexity.lean:58

def bitEncode [BitstringEncoding α] (a : α) : List Bool := toEncoding.encode a

MathlibExt/Computability/Complexity.lean:55

Uses 3 · Used by 309

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Encoding function of a bitstring encoding

DefinitionSelf-delimiting form of a bitstring#✓fully proved

The self-delimiting form of a bitstring \((b_1, \dots, b_n)\) is \((\mathrm{true}, b_1, \dots, \mathrm{true}, b_n, \mathrm{false})\): each bit is preceded by \(\mathrm{true}\) and the block is terminated by \(\mathrm{false}\). In particular the empty bitstring becomes \((\mathrm{false})\).

def delimit : List Bool → List Bool
  | [] => [false]
  | b :: l => true :: b :: delimit l

Used by 367

DefinitionParsing one self-delimiting block#✓fully proved

Write booleans as bits, with true as \(1\) and false as \(0\). Reading a list of bits from the front, a \(0\) ends the block, and a \(1\) followed by a bit \(b\) contributes \(b\) to the payload. The result is the payload together with the rest of the list after the terminating \(0\). Parsing fails if the list runs out before a terminating \(0\) is read.

def undelimit : List Bool → Option (List Bool × List Bool)
  | false :: rest => some ([], rest)
  | true :: b :: input => (undelimit input).map fun p => (b :: p.1, p.2)
  | _ => none

Used by 338

DefinitionBounded parsing of self-delimiting blocks#✓fully proved

Given a bound \(n\) and a list of booleans \(s\), the parse returns the empty list of payloads if \(s\) is empty. If \(s\) is nonempty and \(n = 0\) it fails. If \(s\) is nonempty and \(n = m + 1\), it parses one self-delimiting block from the front of \(s\), then parses the remaining list with bound \(m\), and returns the first payload followed by the payloads of the rest. It fails if either step fails. So the parse succeeds exactly when \(s\) is the concatenation of at most \(n\) self-delimiting blocks, and it returns their payloads in order.

def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
  | _, [] => some []
  | 0, _ :: _ => none
  | fuel + 1, input =>
    (undelimit input).bind fun p => (undelimitBlocksAux fuel p.2).map (p.1 :: ·)

def undelimit : List Bool → Option (List Bool × List Bool)
  | false :: rest => some ([], rest)
  | true :: b :: input => (undelimit input).map fun p => (b :: p.1, p.2)
  | _ => none

MathlibExt/Computability/Complexity.lean:74

Uses 1 · Used by 304

Statement usesParsing one self-delimiting block

DefinitionParsing a list of booleans into self-delimiting blocks#✓fully proved

Given a list of booleans \(s\), this repeatedly parses one self-delimiting block from the front of \(s\) until \(s\) is used up, allowing at most as many blocks as the length of \(s\), and returns the list of payloads in order. It fails if some block fails to parse. The bound never binds, since every block uses at least one bit. So the parse succeeds exactly when \(s\) is a concatenation of self-delimiting blocks.

def undelimitBlocks (input : List Bool) : Option (List (List Bool)) :=
  undelimitBlocksAux input.length input

def undelimitBlocksAux : ℕ → List Bool → Option (List (List Bool))
  | _, [] => some []
  | 0, _ :: _ => none
  | fuel + 1, input =>
    (undelimit input).bind fun p => (undelimitBlocksAux fuel p.2).map (p.1 :: ·)

MathlibExt/Computability/Complexity.lean:95

Uses 1 · Used by 301

Statement usesBounded parsing of self-delimiting blocks

Complexity Theory

AbbreviationDecision problems#✓fully proved

A decision problem is a function from finite lists of booleans (bitstrings) to booleans.

abbrev DecisionProblem := List Bool → Bool

Sources

inlined from FormalConjectures (absent from Mathlib).

Used by 439

AbbreviationComplexity classes#✓fully proved

A complexity class is a set of decision problems.

abbrev DecisionComplexityClass := Set DecisionProblem

Sources

inlined from FormalConjectures (absent from Mathlib).

Uses 1 · Used by 275

Statement usesDecision problems

DefinitionPolynomial-time computability under given encodings#✓fully proved

Let \(e_\alpha\) encode \(\alpha\) as words over an alphabet \(\Gamma_\alpha\) and \(e_\beta\) encode \(\beta\) as words over \(\Gamma_\beta\). A function \(f : \alpha \to \beta\) is polynomial-time computable with respect to \(e_\alpha\) and \(e_\beta\) when there are a multi-stack Turing machine with finitely many stacks, function labels and internal states and a finite input stack alphabet, identifications of its input and output stack alphabets with \(\Gamma_\alpha\) and \(\Gamma_\beta\), and a polynomial \(p\) with natural-number coefficients, such that for every \(a \in \alpha\) the machine, started at its main function in its initial state with \(e_\alpha(a)\) on its input stack and every other stack empty, halts within \(p(n)\) steps, where \(n\) is the length of \(e_\alpha(a)\), with \(e_\beta(f(a))\) on its output stack, every other stack empty and its internal state equal to its initial state.

def IsPolyTimeWithEncoding {α β Γα Γβ : Type} (ea : Encoding α Γα)
    (eb : Encoding β Γβ) (f : α → β) :=
  Nonempty (Turing.TM2ComputableInPolyTime ea.encode eb.encode f)

Sources

inlined from FormalConjectures (absent from Mathlib).

Used by 2

Used byPolynomial-time computable functions · Composition of polynomial-time functions under encodings

DefinitionPolynomial-time computable functions#✓fully proved

Let \(\alpha\) and \(\beta\) be types with canonical bitstring encodings. A function \(f : \alpha \to \beta\) is polynomial-time computable when it is polynomial-time computable with respect to the canonical bitstring encodings of \(\alpha\) and \(\beta\).

def IsPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
    (f : α → β) : Prop :=
  IsPolyTimeWithEncoding (BitstringEncoding.toEncoding (α := α))
    (BitstringEncoding.toEncoding (α := β)) f

class BitstringEncoding α extends Computability.Encoding α Bool

MathlibExt/Computability/Complexity.lean:48

def IsPolyTimeWithEncoding {α β Γα Γβ : Type} (ea : Encoding α Γα)
    (eb : Encoding β Γβ) (f : α → β) :=
  Nonempty (Turing.TM2ComputableInPolyTime ea.encode eb.encode f)

MathlibExt/Computability/Complexity.lean:179

Sources

inlined from FormalConjectures (absent from Mathlib).

Uses 2 · Used by 103

Statement usesBitstring encodings · Polynomial-time computability under given encodings

DefinitionThe complexity class P#✓fully proved

P is the set of decision problems (functions from lists of booleans to booleans) that are computable in polynomial time by a deterministic multi-stack Turing machine, with respect to the canonical bitstring encodings of inputs and outputs.

def P : DecisionComplexityClass :=
  { L | IsPolyTime L }

abbrev DecisionComplexityClass := Set DecisionProblem

MathlibExt/Computability/Complexity.lean:174

def IsPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
    (f : α → β) : Prop :=
  IsPolyTimeWithEncoding (BitstringEncoding.toEncoding (α := α))
    (BitstringEncoding.toEncoding (α := β)) f

MathlibExt/Computability/Complexity.lean:186

Uses 11 · Used by 32

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Complexity classes · Decision problems · Polynomial-time computable functions

Used byPolynomial-time word problem for Aut(Fₙ) (Kourovka 16.109) · NC is contained in P · The Circuit Value Problem is P-complete · NL is contained in P · Ladner's theorem: NP-intermediate languages exist · Mahaney's theorem: sparse NP-complete sets imply P = NP · If P = NP then the polynomial hierarchy collapses to P · A timed decider with polynomial-time output function gives membership in P · Problems in P are decided in polynomial time by single-tape machines · Immerman-Vardi: FO + least fixed point is P on ordered structures · The quadratic diagonal language is in P · Diagonalization across models · Polynomial time is not contained in code time \(n^2 + 1\) · There is an EXP language outside P (time-hierarchy separation) · Hastad: optimal inapproximability of MAX-3SAT · MAX-CUT has no PTAS unless P = NP · 2-SAT is in P · PRIMES is in P · PATH ∈ P · The EGRES question on hypergraph \(k\)-cut for fixed \(k\) · Integer linear programming in fixed dimension is in P (Lenstra) · Linear programming is in P (Khachiyan) · General matching is in P (Edmonds' blossom algorithm) · Max flow is in P (Edmonds-Karp) · Ruciński's question on perfect matchings in dense hypergraphs · Algorithmica · Heuristica · Impagliazzo's five worlds · Pessiland · Nisan-Wigderson: exponential hardness in E derandomizes BPP · One-way functions imply P ≠ NP · P is closed under polynomial-time preimages

DefinitionThe complexity class NP#✓fully proved

NP is the set of decision problems \(L\) (functions from lists of booleans to booleans) for which there exist a polynomial \(p\) with natural-number coefficients and a polynomial-time computable function \(R\) from pairs of lists of booleans to booleans such that, for every list of booleans \(x\), \(L(x)\) is true if and only if there is a list of booleans \(w\) whose length is at most \(p\) evaluated at the length of \(x\) and for which \(R(x, w)\) is true.

Polynomial time is measured with respect to the canonical bitstring encodings.

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

abbrev DecisionComplexityClass := Set DecisionProblem

MathlibExt/Computability/Complexity.lean:174

def IsPolyTime {α β : Type} [BitstringEncoding α] [BitstringEncoding β]
    (f : α → β) : Prop :=
  IsPolyTimeWithEncoding (BitstringEncoding.toEncoding (α := α))
    (BitstringEncoding.toEncoding (α := β)) f

MathlibExt/Computability/Complexity.lean:186

Uses 11 · Used by 159

Statement usesBitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Complexity classes · Decision problems · Polynomial-time computable functions

DefinitionThe class coNP#✓fully proved

The class coNP. coNP is the set of decision problems \(L\) whose complement, the decision problem that accepts exactly the bitstrings that \(L\) rejects, belongs to NP.

def coNP : DecisionComplexityClass :=
  { L | Lᶜ ∈ NP }

abbrev DecisionComplexityClass := Set DecisionProblem

MathlibExt/Computability/Complexity.lean:174

def NP : DecisionComplexityClass :=
  { L | ∃ (p : Polynomial ℕ), ∃ R : (List Bool × List Bool) → Bool,
      IsPolyTime R ∧
      ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧ R (x, w) }

MathlibExt/Computability/Complexity.lean:200

Sources

inlined from FormalConjectures (absent from Mathlib).

Uses 3 · Used by 2

Statement usesComplexity classes · Decision problems · The complexity class NP

Used byUNSAT is coNP-complete · coNP is closed under polynomial-time preimages

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.