Time and space complexity classes

DefinitionLanguage of a decision problem#✓fully proved

The language of a decision problem \(L\) is the set of bitstrings \(x\) with \(L(x) = \mathrm{true}\).

def langOf (L : DecisionProblem) : Set (List Bool) := {x | L x = true}
Uses 1 · Used by 9
Statement usesDecision problems
Used byPSPACE is contained in EXP · The class E · The class EXP · The class EXPSPACE · Deterministic logarithmic space · The complexity class NEXP · The complexity class NL · The complexity class NPSPACE · Polynomial space for decision problems

DefinitionPolynomial space for decision problems#✓fully proved

The class PSPACE of decision problems consists of the decision problems \(L\) whose language \(\{x : L(x) = \mathrm{true}\}\) lies in the multi-tape class PSPACE, that is, is decided by a multi-tape Turing machine that halts on every input and uses space \(O(n^d)\) for some natural number \(d\).

def PSPACE : DecisionComplexityClass :=
  {L | langOf L ∈ Cslib.Turing.MultiTapeTM.Classes.PSPACE}
Uses 4 · Used by 13
Statement usesLanguage of a decision problem · Polynomial space on multi-tape machines · Complexity classes · Decision problems
Used byGeography is PSPACE-complete · The model checking, satisfiability and validity problems of the linear modal μ-calculus are PSPACE-complete · TQBF is PSPACE-complete · NP is contained in PSPACE · PSPACE is contained in EXP · The polynomial hierarchy is contained in PSPACE · Savitch's theorem: NPSPACE = PSPACE · Threshold languages of #P functions are in PSPACE · PP is contained in PSPACE · There is a PSPACE language outside L (space-hierarchy separation) · BPP is contained in PSPACE · BQP is contained in PSPACE · IP = PSPACE (Shamir)

DefinitionThe class EXP#✓fully proved

EXP, deterministic exponential time, is the class of decision problems \(L\) for which there is a natural number \(d\) such that the language of \(L\), the set of bitstrings \(x\) with \(L(x)\) true, belongs to \(\mathrm{DTIME}(2^{n^d})\): it is decided by a multi-tape Turing machine over the binary alphabet with finitely many states in time at most \(c_1 2^{n^d} + c_2\) on inputs of length \(n\), for some natural numbers \(c_1\) and \(c_2\).

def EXP : DecisionComplexityClass :=
  {L | ∃ d, langOf L ∈ Cslib.Turing.MultiTapeTM.DTIME (fun n => 2 ^ (n ^ d))}
Uses 4 · Used by 4
Statement usesLanguage of a decision problem · Deterministic time classes on multi-tape machines · Complexity classes · Decision problems
Used bySatisfiability of a modal μ-calculus formula is EXPTIME-complete · Succinct Circuit Value is EXP-complete · PSPACE is contained in EXP · There is an EXP language outside P (time-hierarchy separation)

DefinitionThe class EXPSPACE#✓fully proved

EXPSPACE, deterministic exponential space, is the class of decision problems \(L\) for which there is a natural number \(d\) such that the language of \(L\), the set of bitstrings \(x\) with \(L(x)\) true, belongs to \(\mathrm{DSPACE}(2^{n^d})\): it is decided by a multi-tape Turing machine over the binary alphabet with finitely many states that halts on every input and visits at most \(c_1 2^{n^d} + c_2\) work-tape cells on inputs of length \(n\), for some natural numbers \(c_1\) and \(c_2\).

def EXPSPACE : DecisionComplexityClass :=
  {L | ∃ d, langOf L ∈ Cslib.Turing.MultiTapeTM.DSPACE (fun n => 2 ^ (n ^ d))}
Uses 4 · Used by 2
Statement usesLanguage of a decision problem · Deterministic space classes on multi-tape machines · Complexity classes · Decision problems
Used byRegular expressions with squaring: universality is EXPSPACE-complete · NEXP is contained in EXPSPACE

DefinitionThe class E#✓fully proved

E is the class of decision problems \(L\) for which there is a natural number \(c\) such that the language of \(L\), the set of bitstrings \(x\) with \(L(x)\) true, belongs to \(\mathrm{DTIME}(2^{cn})\): it is decided by a multi-tape Turing machine over the binary alphabet with finitely many states in time at most \(c_1 2^{cn} + c_2\) on inputs of length \(n\), for some natural numbers \(c_1\) and \(c_2\).

def E : DecisionComplexityClass :=
  {L | ∃ c, langOf L ∈ Cslib.Turing.MultiTapeTM.DTIME (fun n => 2 ^ (c * n))}
Uses 4 · Used by 1
Statement usesLanguage of a decision problem · Deterministic time classes on multi-tape machines · Complexity classes · Decision problems
Used byNisan-Wigderson: exponential hardness in E derandomizes BPP

DefinitionDeterministic logarithmic space#✓fully proved

The class \(\mathsf{L}\) consists of the decision problems \(L\) for which there is a constant \(c \in \mathbb{N}\) such that the language of \(L\) lies in \(\mathrm{DSPACE}(s)\) for \(s(n) = c \lfloor \log_2(n + 1) \rfloor + c\), the class of languages decided by a multi-tape Turing machine with binary alphabet and finitely many states, within some time bound, visiting at most \(c_1 s(n) + c_2\) work-tape cells on inputs of length \(n\) for some constants \(c_1\) and \(c_2\).

def LogSpace : DecisionComplexityClass :=
  {L | ∃ c, langOf L ∈
    Cslib.Turing.MultiTapeTM.DSPACE (fun n => c * Nat.log 2 (n + 1) + c)}
Uses 4 · Used by 3
Statement usesLanguage of a decision problem · Deterministic space classes on multi-tape machines · Complexity classes · Decision problems
Used byNC^1 is contained in L · There is a PSPACE language outside L (space-hierarchy separation) · Undirected ST-connectivity is in L (Reingold)

DefinitionLog-space computable functions#✓fully proved

A function \(f\) from bitstrings to bitstrings is log-space computable when there are a constant \(c \in \mathbb{N}\) and a time bound \(t : \mathbb{N} \to \mathbb{N}\) such that some multi-tape Turing machine with binary alphabet and finitely many states, on every bitstring input \(x\), halts with output \(f(x)\) within \(t(|x|)\) steps and visits at most \(c \lfloor \log_2(|x| + 1) \rfloor + c\) work-tape cells in total.

def LogSpaceComputable (f : List Bool → List Bool) : Prop :=
  ∃ c, ∃ t : ℕ → ℕ,
    Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength f
      ⟨id, Function.injective_id⟩ ⟨id, Function.injective_id⟩ t
      (fun n => c * Nat.log 2 (n + 1) + c)
Used by 2
Used byLog-space many-one reductions · Log-space uniform circuit families

DefinitionLog-space many-one reductions#✓fully proved

A decision problem \(L_1\) is log-space many-one reducible to a decision problem \(L_2\) when there is a log-space computable function \(f\) from bitstrings to bitstrings such that, for every bitstring \(x\), \(L_1(x)\) is true if and only if \(L_2(f(x))\) is true.

def LogSpaceRed (L₁ L₂ : DecisionProblem) : Prop :=
  ∃ f, LogSpaceComputable f ∧ ∀ x, L₁ x ↔ L₂ (f x)
Uses 2 · Used by 2
Statement usesLog-space computable functions · Decision problems
Used byThe Circuit Value Problem is P-complete · ST-connectivity is NL-complete

DefinitionNondeterministic decision#✓fully proved

A nondeterministic multi-tape Turing machine \(M\) over the boolean alphabet decides a set \(L\) of bitstrings if, for every bitstring \(x\), \(x \in L\) if and only if some computation path of \(M\) on \(x\) ends in a halted configuration whose output is the one-element list \([\mathrm{true}]\).

def NTMDecides {k : ℕ} {State : Type*} (ntm : Turing.MultiTapeNTM k Bool State)
    (L : Set (List Bool)) : Prop :=
  ∀ x, (x ∈ L ↔ ∃ p : ntm.ComputationPath x, p.last.Halted ∧ p.last.output = [true])
Used by 2
Used byNondeterministic decision in bounded space · Nondeterministic decision in bounded time

DefinitionNondeterministic decision in bounded time#✓fully proved

Let \(M\) be a nondeterministic multi-tape Turing machine over the boolean alphabet, \(t : \mathbb{N} \to \mathbb{N}\) and \(L\) a set of bitstrings. Then \(M\) decides \(L\) in time \(t\) if, for every input \(x\), every computation path of \(M\) on \(x\) with at least \(t(|x|)\) steps ends in a halted configuration, where \(|x|\) is the length of \(x\), and for every bitstring \(x\), \(x \in L\) if and only if some computation path of \(M\) on \(x\) ends in a halted configuration whose output is the one-element list \([\mathrm{true}]\).

def NTMDecidesInTime {k : ℕ} {State : Type*} (ntm : Turing.MultiTapeNTM k Bool State)
    (t : ℕ → ℕ) (L : Set (List Bool)) : Prop :=
  (∀ x, ∀ p : ntm.ComputationPath x, t x.length ≤ p.time → p.last.Halted) ∧
    NTMDecides ntm L
Uses 1 · Used by 1
Statement usesNondeterministic decision
Used byNondeterministic time classes

DefinitionNondeterministic decision in bounded space#✓fully proved

Let \(M\) be a nondeterministic multi-tape Turing machine over the boolean alphabet, \(s : \mathbb{N} \to \mathbb{N}\) and \(L\) a set of bitstrings. Then \(M\) decides \(L\) in space \(s\) if, for every input \(x\), every computation path of \(M\) on \(x\) visits at most \(s(|x|)\) work-tape cells in total, where \(|x|\) is the length of \(x\), and for every bitstring \(x\), \(x \in L\) if and only if some computation path of \(M\) on \(x\) ends in a halted configuration whose output is the one-element list \([\mathrm{true}]\).

def NTMDecidesInSpace {k : ℕ} {State : Type*} (ntm : Turing.MultiTapeNTM k Bool State)
    (s : ℕ → ℕ) (L : Set (List Bool)) : Prop :=
  (∀ x, ∀ p : ntm.ComputationPath x, p.space ≤ s x.length) ∧
    NTMDecides ntm L
Uses 1 · Used by 1
Statement usesNondeterministic decision
Used byNondeterministic space classes

DefinitionNondeterministic time classes#✓fully proved

For \(t : \mathbb{N} \to \mathbb{N}\), \(\mathrm{NTIME}(t)\) is the set of languages \(L\) of bitstrings for which there are natural numbers \(c_1\), \(c_2\), \(k\) and a nondeterministic multi-tape Turing machine \(M\) over the boolean alphabet with finitely many states and \(k\) work tapes that decides \(L\) in time \(c_1 t(n) + c_2\): on every input \(x\), every computation path of \(M\) with at least \(c_1 t(|x|) + c_2\) steps ends in a halted configuration, where \(|x|\) is the length of \(x\), and \(x \in L\) if and only if some computation path of \(M\) on \(x\) ends in a halted configuration whose output is the one-element list \([\mathrm{true}]\).

def NTIME (t : ℕ → ℕ) : Set (Set (List Bool)) :=
  {L | ∃ c₁ c₂, ∃ k, ∃ (State : Type) (_ : Finite State),
    ∃ ntm : Turing.MultiTapeNTM k Bool State,
    NTMDecidesInTime ntm (fun n => c₁ * t n + c₂) L}
Uses 1 · Used by 2
Statement usesNondeterministic decision in bounded time
Used byThe complexity class NEXP · Nondeterministic time hierarchy

DefinitionNondeterministic space classes#✓fully proved

For \(s : \mathbb{N} \to \mathbb{N}\), \(\mathrm{NSPACE}(s)\) is the set of languages \(L\) of bitstrings for which there are natural numbers \(c_1\), \(c_2\), \(k\) and a nondeterministic multi-tape Turing machine \(M\) over the boolean alphabet with finitely many states and \(k\) work tapes that decides \(L\) in space \(c_1 s(n) + c_2\): on every input \(x\), every computation path of \(M\) visits at most \(c_1 s(|x|) + c_2\) work-tape cells in total, where \(|x|\) is the length of \(x\), and \(x \in L\) if and only if some computation path of \(M\) on \(x\) ends in a halted configuration whose output is the one-element list \([\mathrm{true}]\).

def NSPACE (s : ℕ → ℕ) : Set (Set (List Bool)) :=
  {L | ∃ c₁ c₂, ∃ k, ∃ (State : Type) (_ : Finite State),
    ∃ ntm : Turing.MultiTapeNTM k Bool State,
    NTMDecidesInSpace ntm (fun n => c₁ * s n + c₂) L}
Uses 1 · Used by 2
Statement usesNondeterministic decision in bounded space
Used byThe complexity class NL · The complexity class NPSPACE

DefinitionThe complexity class NL#✓fully proved

NL is the set of decision problems \(L\) for which there is a natural number \(c\) such that the language of \(L\) (the set of bitstrings on which \(L\) is true) belongs to \(\mathrm{NSPACE}(s)\) for \(s(n) = c \lfloor \log_2 (n + 1) \rfloor + c\), where \(\mathrm{NSPACE}(s)\) is the class of languages decided by a nondeterministic multi-tape Turing machine with finitely many states in space \(c_1 s(n) + c_2\) for some natural numbers \(c_1, c_2\).

def NL : DecisionComplexityClass :=
  {L | ∃ c, langOf L ∈ NSPACE (fun n => c * Nat.log 2 (n + 1) + c)}
Uses 4 · Used by 4
Statement usesNondeterministic space classes · Language of a decision problem · Complexity classes · Decision problems
Used byST-connectivity is NL-complete · NL is contained in P · Immerman-Szelepcsenyi theorem: NL = coNL · Immerman: FO + transitive closure is NL on ordered structures

DefinitionThe complexity class NPSPACE#✓fully proved

NPSPACE is the set of decision problems \(L\) for which there is a natural number \(d\) such that the language of \(L\) (the set of bitstrings on which \(L\) is true) belongs to \(\mathrm{NSPACE}(s)\) for \(s(n) = n^d\), where \(\mathrm{NSPACE}(s)\) is the class of languages decided by a nondeterministic multi-tape Turing machine with finitely many states in space \(c_1 s(n) + c_2\) for some natural numbers \(c_1, c_2\).

def NPSPACE : DecisionComplexityClass :=
  {L | ∃ d, langOf L ∈ NSPACE (fun n => n ^ d)}
Uses 4 · Used by 1
Statement usesNondeterministic space classes · Language of a decision problem · Complexity classes · Decision problems
Used bySavitch's theorem: NPSPACE = PSPACE

DefinitionThe complexity class NEXP#✓fully proved

NEXP is the set of decision problems \(L\) for which there is a polynomial \(p\) with natural-number coefficients such that the language of \(L\) (the set of bitstrings on which \(L\) is true) belongs to \(\mathrm{NTIME}(t)\) for \(t(n) = 2^{p(n)}\), where \(\mathrm{NTIME}(t)\) is the class of languages decided by a nondeterministic multi-tape Turing machine with finitely many states in time \(c_1 t(n) + c_2\) for some natural numbers \(c_1, c_2\).

def NEXP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, langOf L ∈ NTIME (fun n => 2 ^ (p.eval n))}
Uses 4 · Used by 3
Statement usesNondeterministic time classes · Language of a decision problem · Complexity classes · Decision problems
Used byWilliams: NEXP is not contained in ACC0 · Succinct 3SAT is NEXP-complete · NEXP is contained in EXPSPACE

DefinitionBPP#✓fully proved

The class BPP of bounded-error probabilistic polynomial-time decision problems consists of the decision problems \(L\) for which there are a polynomial \(p\) with natural number coefficients and a polynomial-time computable function \(R\) from pairs of bitstrings to booleans such that, for every bitstring \(x\), writing \(m = p(|x|)\) and \(c_x\) for the number of strings \(r \in \{0,1\}^m\) with \(R(x, r)\) true: if \(L(x)\) is true then \(3 c_x \ge 2 \cdot 2^m\), and if \(L(x)\) is false then \(3 c_x \le 2^m\). That is, for a uniformly random \(r\), \(R(x, r)\) is true with probability at least \(2/3\) on yes-instances and at most \(1/3\) on no-instances.

def BPP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}
Uses 11 · Used by 5
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 byNisan-Wigderson: exponential hardness in E derandomizes BPP · Adleman's theorem: BPP is contained in P/poly · BPP is contained in PSPACE · RP is contained in BPP · Sipser-Gács-Lautemann: BPP is in \(\Sigma_2^p\) and \(\Pi_2^p\)

DefinitionProbabilistic polynomial time with unbounded error#✓fully proved

The class PP consists of the decision problems \(L\) for which there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable function \(R\) on pairs of bitstrings such that, for every bitstring \(x\) and \(r\) uniformly random among the bitstrings of length \(p(|x|)\), the probability that \(R(x, r)\) is true is greater than \(1/2\) if \(L(x)\) is true, and at most \(1/2\) if \(L(x)\) is false.

def PP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        2 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} >
          2 ^ (p.eval x.length)) ∧
      (L x = false →
        2 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≤
          2 ^ (p.eval x.length))}
Uses 11 · Used by 4
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 byMAJSAT is PP-complete · NP is contained in PP · PP is contained in PSPACE · BQP is contained in PP

DefinitionPolynomial time with polynomial advice#✓fully proved

The class P/poly consists of the decision problems \(L\) for which there are a polynomial \(p\) with natural-number coefficients, bitstrings \(a_0, a_1, a_2, \ldots\) with \(|a_n| \le p(n)\) for every \(n\), and a polynomial-time computable function \(R\) on pairs of bitstrings such that for every bitstring \(x\), \(L(x)\) is true if and only if \(R(x, a_{|x|})\) is true.

def PPoly : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ advice : ℕ → List Bool,
    (∀ n, (advice n).length ≤ p.eval n) ∧
    ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ R (x, advice x.length) = true}
Uses 11 · Used by 3
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 byKarp-Lipton theorem: NP in P/poly collapses PH · Usefulness against P/poly · Adleman's theorem: BPP is contained in P/poly

DefinitionThe counting class \(\#P\)#✓fully proved

A function \(f\) from bitstrings to natural numbers is in \(\#P\) when there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable Boolean function \(R\) on pairs of bitstrings such that for every bitstring \(x\), \(f(x)\) is the number of bitstrings \(w\) of length exactly \(p(|x|)\) for which \(R(x, w)\) is true.

def SharpP : Set (List Bool → ℕ) :=
  {f | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x, f x = Set.ncard
      {w : Fin (p.eval x.length) → Bool | R (x, List.ofFn w) = true}}
Uses 9 · Used by 4
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 · Polynomial-time computable functions
Used byPolynomial time with a #P oracle · \(\#P\)-complete functions · Stockmeyer: approximate counting of #P functions in BPP^NP · Threshold languages of #P functions are in PSPACE

DefinitionEvaluation of an oracle machine with adaptive queries#✓fully proved

Let \(\alpha\) be a type of oracle answers and \(\beta\) a type of outputs, and call a list of pairs of a bitstring and an element of \(\alpha\) a history. Fix a length cap \(c \in \mathbb{N}\), a next-query function \(N\) sending an input bitstring and a history to a bitstring, a decision function \(F\) sending an input bitstring and a history to an element of \(\beta\), an oracle \(O\) from bitstrings to \(\alpha\) and an input bitstring \(x\). For a number \(f \in \mathbb{N}\) of remaining queries and a history \(h\), the evaluation \(E_f(h)\) is defined by recursion on \(f\): \(E_0(h) = F(x, h)\), and for \(E_{f+1}(h)\) let \(q = N(x, h)\); if \(q\) has length at most \(c\), then \(E_{f+1}(h) = E_f(h')\), where \(h'\) is \(h\) with the pair \((q, O(q))\) appended at the end, and otherwise \(E_{f+1}(h) = F(x, h)\).

Dummy queries simulate early halting, so a fixed number of queries is without loss of generality. At use sites the cap is polynomial in the length of \(x\), so polynomial running time of \(N\) and \(F\) on each call gives polynomial total running time in the length of \(x\).

def evalOracle {α β : Type} (cap : ℕ)
    (nextQ : List Bool × List (List Bool × α) → List Bool)
    (final : List Bool × List (List Bool × α) → β)
    (oracle : List Bool → α) (x : List Bool) (fuel : ℕ)
    (hist : List (List Bool × α)) : β :=
  match fuel with
  | 0 => final (x, hist)
  | fuel + 1 =>
    let q := nextQ (x, hist)
    if q.length ≤ cap then
      evalOracle cap nextQ final oracle x fuel
        (hist ++ [(q, oracle q)])
    else final (x, hist)
Used by 5
Used byNP relative to an oracle · Polynomial time with an oracle · Polynomial time with a #P oracle · \(\#P\)-complete functions · Stockmeyer: approximate counting of #P functions in BPP^NP

DefinitionPolynomial time with an oracle#✓fully proved

For a Boolean oracle \(O\) on bitstrings, the class \(\mathsf{P}^O\) consists of the decision problems \(L\) for which there are polynomials \(p\) and \(q\) and polynomial-time functions \(\mathrm{next}\) and \(\mathrm{final}\) such that, for every bitstring \(x\), \(L(x)\) is true exactly when the following oracle machine outputs true on \(x\). Starting from the empty history \(h\), it runs \(p(|x|)\) rounds; in each round it computes the query \(y = \mathrm{next}(x, h)\) from \(x\) and the history \(h\) of queries and answers so far, and if \(|y| \le q(|x|)\) it appends \((y, O(y))\) to \(h\), while otherwise it skips all remaining rounds. Finally it outputs \(\mathrm{final}(x, h)\).

def PWithOracle (O : List Bool → Bool) : DecisionComplexityClass :=
  {L | ∃ p q : Polynomial ℕ,
    ∃ nextQ : List Bool × List (List Bool × Bool) → List Bool,
    ∃ final : List Bool × List (List Bool × Bool) → Bool,
    IsPolyTime nextQ ∧ IsPolyTime final ∧
    ∀ x, L x ↔
      evalOracle (q.eval x.length) nextQ final O x (p.eval x.length) [] = true}
Uses 12 · Used by 2
Statement usesEvaluation of an oracle machine with adaptive queries · Bitstring 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 byAaronson-Wigderson: the algebrization barrier · Baker-Gill-Solovay: oracles separate and collapse P vs NP

DefinitionNP relative to an oracle#✓fully proved

Let \(O\) be a function from bitstrings to booleans. The class \(\mathrm{NP}^O\) is the set of decision problems \(L\) for which there are polynomials \(p\) and \(q\) with natural-number coefficients and polynomial-time computable functions \(\mathrm{nextQ}\) and \(\mathrm{final}\), each taking a bitstring and a list of query/answer pairs, such that for every bitstring \(x\), \(L(x)\) is true if and only if there is a bitstring \(w\) of length at most \(p(|x|)\), where \(|x|\) is the length of \(x\), for which the oracle computation that chooses queries with \(\mathrm{nextQ}\) and decides with \(\mathrm{final}\), run with oracle \(O\), query-length cap \(q(|x|)\) and \(p(|x|)\) adaptive queries on the bitstring encoding of the pair \((x, w)\) from the empty history, returns true.

def NPWithOracle (O : List Bool → Bool) : DecisionComplexityClass :=
  {L | ∃ p q : Polynomial ℕ,
    ∃ nextQ : List Bool × List (List Bool × Bool) → List Bool,
    ∃ final : List Bool × List (List Bool × Bool) → Bool,
    IsPolyTime nextQ ∧ IsPolyTime final ∧
    ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧
      evalOracle (q.eval x.length) nextQ final O (MetaMathlibExt.BitstringEncoding.bitEncode (x, w))
        (p.eval x.length) [] = true}
Uses 12 · Used by 3
Statement usesEvaluation of an oracle machine with adaptive queries · Bitstring 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 byAaronson-Wigderson: the algebrization barrier · Baker-Gill-Solovay: oracles separate and collapse P vs NP · An oracle separates NP from coNP

DefinitionPolynomial time with a #P oracle#✓fully proved

The class \(\mathsf{P}^{\#\mathsf{P}}\) consists of the decision problems \(L\) for which there are a function \(f\) in \(\#\mathsf{P}\), polynomials \(p\) and \(q\), and polynomial-time functions \(\mathrm{next}\) and \(\mathrm{final}\) such that, for every bitstring \(x\), \(L(x)\) is true exactly when the following oracle machine outputs true on \(x\). Starting from the empty history \(h\), it runs \(p(|x|)\) rounds; in each round it computes the query \(y = \mathrm{next}(x, h)\) from \(x\) and the history \(h\) of queries and their natural-number answers so far, and if \(|y| \le q(|x|)\) it appends \((y, f(y))\) to \(h\), while otherwise it skips all remaining rounds. Finally it outputs \(\mathrm{final}(x, h)\).

def PWithSharpP : DecisionComplexityClass :=
  {L | ∃ f ∈ SharpP, ∃ p q : Polynomial ℕ,
    ∃ nextQ : List Bool × List (List Bool × ℕ) → List Bool,
    ∃ final : List Bool × List (List Bool × ℕ) → Bool,
    IsPolyTime nextQ ∧ IsPolyTime final ∧
    ∀ x, L x ↔
      evalOracle (q.eval x.length) nextQ final f x (p.eval x.length) [] = true}
Uses 13 · Used by 1
Statement usesThe counting class \(\#P\) · Evaluation of an oracle machine with adaptive queries · Bitstring 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 byToda's theorem: PH is contained in \(\mathsf{P}^{\#\mathsf{P}}\)

Definition\(\#P\)-complete functions#✓fully proved

A function \(f\) from bitstrings to natural numbers is \(\#P\)-complete when \(f\) is in \(\#P\) and every function \(g\) in \(\#P\) is computed from \(f\) by a polynomial-time oracle machine. That is, there are polynomials \(p\) and \(q\) with natural-number coefficients and polynomial-time computable functions choosing the next query and the final natural-number answer from the input and the history of queries and oracle answers, such that for every bitstring \(x\) the following outputs \(g(x)\): make up to \(p(|x|)\) queries to \(f\) in turn, stop early as soon as the next query is longer than \(q(|x|)\), and then return the final answer computed from \(x\) and the history.

def SharpPComplete (f : List Bool → ℕ) : Prop :=
  f ∈ SharpP ∧ ∀ g ∈ SharpP, ∃ p q : Polynomial ℕ,
    ∃ nextQ : List Bool × List (List Bool × ℕ) → List Bool,
    ∃ final : List Bool × List (List Bool × ℕ) → ℕ,
    IsPolyTime nextQ ∧ IsPolyTime final ∧
    ∀ x, g x = evalOracle (q.eval x.length) nextQ final f x (p.eval x.length) []
Uses 11 · Used by 2
Statement usesThe counting class \(\#P\) · Evaluation of an oracle machine with adaptive queries · Bitstring 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 · Polynomial-time computable functions
Used byThe permanent is #P-complete (Valiant) · Counting SAT is #P-complete

DefinitionAlternating bounded quantifiers#✓fully proved

Let \(b : \mathbb{N} \to \mathbb{N}\) be a length bound, \(k\) a natural number, \(R\) a Boolean function of a bitstring and a list of bitstrings, and \(x\) a bitstring. The statement with \(k\) blocks, beginning with \(\exists\) when the given flag is true and with \(\forall\) when it is false, is

\[Q_1 w_1 \, Q_2 w_2 \cdots Q_k w_k \; R(x, [w_1, \dots, w_k]) = \mathrm{true},\]

where the quantifiers \(Q_1, \dots, Q_k\) alternate between \(\exists\) and \(\forall\) and every \(w_i\) ranges over the bitstrings of length at most \(b(|x|)\). For \(k = 0\) it is \(R(x, []) = \mathrm{true}\).

def AltQuant (bound : ℕ → ℕ) : ℕ → Bool →
    (List Bool × List (List Bool) → Bool) → List Bool → Prop
  | 0, _, R, x => R (x, []) = true
  | k + 1, true, R, x =>
    ∃ w, w.length ≤ bound x.length ∧
      AltQuant bound k false (fun p => R (p.1, w :: p.2)) x
  | k + 1, false, R, x =>
    ∀ w, w.length ≤ bound x.length →
      AltQuant bound k true (fun p => R (p.1, w :: p.2)) x
Used by 2
Used byThe universal levels of the polynomial hierarchy · The class \(\Sigma_k^p\)

DefinitionThe class \(\Sigma_k^p\)#✓fully proved

For a natural number \(k\), a decision problem \(L\) is in \(\Sigma_k^p\) when there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable Boolean function \(R\) of a bitstring and a list of bitstrings such that for every bitstring \(x\), \(L(x)\) is true if and only if \(Q_1 w_1\, Q_2 w_2 \cdots Q_k w_k\) with \(R(x, [w_1, \dots, w_k])\) true, where \(Q_i\) is \(\exists\) for odd \(i\) and \(\forall\) for even \(i\), and each \(w_i\) ranges over bitstrings of length at most \(p(|x|)\). For \(k = 0\) the condition is that \(R(x, [\,])\) is true.

def SigmaK (k : ℕ) : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List (List Bool) → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ AltQuant (fun n => p.eval n) k true R x}
Uses 12 · Used by 4
Statement usesAlternating bounded quantifiers · Bitstring 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 by\(\mathrm{QSAT}_k\) is \(\Sigma_k^p\)-complete, uniformly in \(k\) · Karp-Lipton theorem: NP in P/poly collapses PH · The polynomial hierarchy · Sipser-Gács-Lautemann: BPP is in \(\Sigma_2^p\) and \(\Pi_2^p\)

DefinitionThe universal levels of the polynomial hierarchy#✓fully proved

For a natural number \(k\), the class \(\Pi_k^p\) consists of the decision problems \(L\) for which there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable function \(R\), taking a bitstring and a list of bitstrings to a boolean, such that for every bitstring \(x\), \(L(x)\) is true if and only if

\[ \forall w_1\, \exists w_2\, \forall w_3 \cdots Q_k w_k\; R(x, [w_1, \ldots, w_k]) = \mathrm{true}, \]

where the \(k\) quantifiers alternate starting with \(\forall\) (so \(Q_k\) is \(\forall\) for odd \(k\) and \(\exists\) for even \(k\)) and each \(w_i\) ranges over the bitstrings of length at most \(p(|x|)\). For \(k = 0\) the condition is \(R(x, []) = \mathrm{true}\).

def PiK (k : ℕ) : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List (List Bool) → Bool, IsPolyTime R ∧
    ∀ x, L x ↔ AltQuant (fun n => p.eval n) k false R x}
Uses 12 · Used by 2
Statement usesAlternating bounded quantifiers · Bitstring 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 byAM is contained in \(\Pi_2^p\) (Babai) · Sipser-Gács-Lautemann: BPP is in \(\Sigma_2^p\) and \(\Pi_2^p\)

DefinitionThe polynomial hierarchy#✓fully proved

The class PH is the union, over all natural numbers \(k\), of the classes \(\Sigma_k^p\) of the polynomial hierarchy.

def PH : DecisionComplexityClass := ⋃ k, SigmaK k
Uses 3 · Used by 5
Statement usesThe class \(\Sigma_k^p\) · Complexity classes · Decision problems
Used byKarp-Lipton theorem: NP in P/poly collapses PH · If P = NP then the polynomial hierarchy collapses to P · The polynomial hierarchy is contained in PSPACE · Toda's theorem: PH is contained in \(\mathsf{P}^{\#\mathsf{P}}\) · MA is contained in PH

DefinitionThe class \(\mathsf{AM}\) (Arthur–Merlin)#✓fully proved

A decision problem \(L\) on bitstrings is in \(\mathsf{AM}\) when there are polynomials \(p\) and \(q\) with natural-number coefficients and a polynomial-time computable Boolean function \(R(x, r, w)\) of three bitstrings such that, for every bitstring \(x\), writing \(A_x\) for the set of strings \(r \in \{0,1\}^{p(|x|)}\) for which some bitstring \(w\) of length at most \(q(|x|)\) makes \(R(x, r, w)\) true: if \(L(x)\) is true then \(3|A_x| \ge 2 \cdot 2^{p(|x|)}\), and if \(L(x)\) is false then \(3|A_x| \le 2^{p(|x|)}\).

Here \(r\) is Arthur's random string and \(w\) is Merlin's reply, so for uniformly random \(r\) the acceptance probability is at least \(2/3\) on yes-instances and at most \(1/3\) on no-instances.

def AM : DecisionComplexityClass :=
  {L | ∃ p q : Polynomial ℕ,
    ∃ R : List Bool × List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool |
          ∃ w : List Bool, w.length ≤ q.eval x.length ∧
            R (x, List.ofFn r, w) = true} ≥ 2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        3 * Set.ncard {r : Fin (p.eval x.length) → Bool |
          ∃ w : List Bool, w.length ≤ q.eval x.length ∧
            R (x, List.ofFn r, w) = true} ≤ 2 ^ (p.eval x.length))}
Uses 11 · Used by 4
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 byThe class coAM · AM is contained in \(\Pi_2^p\) (Babai) · MA is contained in AM · Graph non-isomorphism is in AM

DefinitionThe class coAM#✓fully proved

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

def coAM : DecisionComplexityClass := {L | Lᶜ ∈ AM}
Uses 3 · Used by 1
Statement usesThe class \(\mathsf{AM}\) (Arthur–Merlin) · Complexity classes · Decision problems
Used byGraph isomorphism is in NP and coAM

DefinitionInteractive-proof game#✓fully proved

The game takes a length cap \(c\), a verifier message function \(V_{\mathrm{msg}}\), a verifier decision function \(V_{\mathrm{dec}}\), a prover \(P\) mapping transcripts (lists of bitstrings) to bitstrings, an input \(x\), a coin string \(\rho\), a number \(k\) of rounds and a transcript \(t\), and returns a Boolean outcome. If \(k = 0\), the outcome is \(V_{\mathrm{dec}}(x, \rho, t)\). Otherwise the verifier sends \(m = V_{\mathrm{msg}}(x, \rho, t)\), and the prover replies \(a = P(t')\), where \(t'\) is \(t\) extended by \(m\). If both \(m\) and \(a\) have length at most \(c\), the outcome is that of the game with \(k - 1\) rounds and transcript \(t\) extended by \(m\) and then \(a\); otherwise the outcome is false.

The transcript records only verifier messages and prover replies, so the prover never sees the verifier's coins. At use sites the cap is polynomial in \(|x|\), so polynomial time for each verifier step gives polynomial total time in the original input.

def IPGame (cap : ℕ)
    (Vmsg : List Bool × List Bool × List (List Bool) → List Bool)
    (Vdec : List Bool × List Bool × List (List Bool) → Bool)
    (P : List (List Bool) → List Bool) (x coins : List Bool) (rounds : ℕ)
    (transcript : List (List Bool)) : Bool :=
  match rounds with
  | 0 => Vdec (x, coins, transcript)
  | rounds + 1 =>
    let m := Vmsg (x, coins, transcript)
    let reply := P (transcript ++ [m])
    if m.length ≤ cap ∧ reply.length ≤ cap then
      IPGame cap Vmsg Vdec P x coins rounds (transcript ++ [m, reply])
    else false
Used by 1
Used byThe class IP

DefinitionThe class IP#✓fully proved

A decision problem \(L\) is in \(\mathsf{IP}\) when there are polynomials \(s\), \(r\) and \(q\) with natural-number coefficients and polynomial-time functions \(V_{\mathrm{msg}}\) (the verifier's message function) and \(V_{\mathrm{dec}}\) (its decision function) with the following property. For a bitstring \(x\), a prover \(P\) (an arbitrary function from transcripts to bitstrings) and a coin string \(c\), let \(G(P, c)\) be the outcome of the interactive-proof game with message length cap \(q(|x|)\), verifier \(V_{\mathrm{msg}}\) and \(V_{\mathrm{dec}}\), prover \(P\), input \(x\), coins \(c\), \(r(|x|)\) rounds and the empty initial transcript. Then for every bitstring \(x\): if \(L(x)\) is true, some prover \(P\) makes \(G(P, c)\) true for at least \(2/3\) of the coin strings \(c \in \{0,1\}^{s(|x|)}\); and if \(L(x)\) is false, every prover \(P\) makes \(G(P, c)\) true for at most \(1/3\) of them.

Cslib.Complexity.Classes.IP · 18 lines 
def IP : DecisionComplexityClass :=
  {L | ∃ s r q : Polynomial ℕ,
    ∃ Vmsg : List Bool × List Bool × List (List Bool) → List Bool,
    ∃ Vdec : List Bool × List Bool × List (List Bool) → Bool,
    IsPolyTime Vmsg ∧ IsPolyTime Vdec ∧
    ∀ x,
      (L x = true →
        ∃ P : List (List Bool) → List Bool,
          3 * Set.ncard {coins : Fin (s.eval x.length) → Bool |
            IPGame (q.eval x.length) Vmsg Vdec P x (List.ofFn coins)
              (r.eval x.length) [] = true} ≥
            2 * 2 ^ (s.eval x.length)) ∧
      (L x = false →
        ∀ P : List (List Bool) → List Bool,
          3 * Set.ncard {coins : Fin (s.eval x.length) → Bool |
            IPGame (q.eval x.length) Vmsg Vdec P x (List.ofFn coins)
              (r.eval x.length) [] = true} ≤
            2 ^ (s.eval x.length))}
Uses 12 · Used by 2
Statement usesInteractive-proof game · Bitstring 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 byGoldwasser-Sipser: private coins add no power to interactive proofs · IP = PSPACE (Shamir)

DefinitionProbabilistically checkable proofs#✓fully proved

For functions \(r, q : \mathbb{N} \to \mathbb{N}\), the class \(\mathrm{PCP}(r, q)\) consists of the decision problems \(L\) for which there are polynomial-time computable functions \(Q\) and \(D\) such that \(Q(x, \rho)\) is a list of at most \(q(|x|)\) natural numbers for all bitstrings \(x\) and \(\rho\), and such that for every bitstring \(x\) the following holds. For a proof \(\pi : \mathbb{N} \to \{\mathrm{true}, \mathrm{false}\}\), let \(\pi(Q(x, \rho))\) be the list of values of \(\pi\) at the entries of \(Q(x, \rho)\), and let \(P_\pi(x)\) be the probability, over a uniformly random bitstring \(\rho\) of length \(r(|x|)\), that \(D(x, \rho, \pi(Q(x, \rho)))\) is true. If \(L(x)\) is true, then \(P_\pi(x) \ge 2/3\) for some proof \(\pi\); if \(L(x)\) is false, then \(P_\pi(x) \le 1/3\) for every proof \(\pi\).

The verifier is non-adaptive: the queried positions depend only on \(x\) and \(\rho\).

Cslib.Complexity.Classes.PCP · 18 lines 
def PCP (rbound qbound : ℕ → ℕ) : DecisionComplexityClass :=
  {L | ∃ queries : List Bool × List Bool → List ℕ,
    ∃ decide : List Bool × List Bool × List Bool → Bool,
    IsPolyTime queries ∧ IsPolyTime decide ∧
    (∀ x rand, (queries (x, rand)).length ≤ qbound x.length) ∧
    ∀ x,
      (L x = true →
        ∃ proof : ℕ → Bool,
          3 * Set.ncard {rand : Fin (rbound x.length) → Bool |
            decide (x, List.ofFn rand,
              (queries (x, List.ofFn rand)).map proof) = true} ≥
              2 * 2 ^ (rbound x.length)) ∧
      (L x = false →
        ∀ proof : ℕ → Bool,
          3 * Set.ncard {rand : Fin (rbound x.length) → Bool |
            decide (x, List.ofFn rand,
              (queries (x, List.ofFn rand)).map proof) = true} ≤
              2 ^ (rbound x.length))}
Uses 11 · Used by 1
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 byThe PCP theorem: NP = PCP(O(log n), O(1))

InductiveGates of a flat Boolean circuit#✓fully proved

A gate of a flat Boolean circuit on \(n\) inputs is one of: an input variable \(x_i\) for some \(i < n\); a Boolean constant; a negation gate with one predecessor index \(a \in \mathbb{N}\); a conjunction gate or a disjunction gate with a list of predecessor indices; or a mod gate with a modulus \(m \in \mathbb{N}\) and a list of predecessor indices.

Predecessors are referred to by their positions in the circuit; that gate \(j\) refers only to gates before \(j\) is a separate well-formedness condition on circuits.

inductive ACGate (n : ℕ) where
  | var : Fin n → ACGate n
  | const : Bool → ACGate n
  | notGate : ℕ → ACGate n
  | andGate : List ℕ → ACGate n
  | orGate : List ℕ → ACGate n
  | modGate : ℕ → List ℕ → ACGate n
Used by 34
Used byRazborov: monotone circuits for clique need superpolynomial size · Shannon: most Boolean functions need exponential circuits · Wire count of a flat circuit · Evaluation of an encoded Boolean circuit · Well-formed encoded circuits · Gate values of an encoded circuit · Well-formed succinct 3SAT descriptors · Gate values of an encoded circuit (Succinct Circuit Value) · Well-formed description circuits (Succinct Circuit Value) · Gate values of an encoded circuit · Decoding a gate from its (kind, references) pair · Encoding a gate as a (kind, references) pair · The class \(\mathsf{AC}^0\) · The class \(\mathsf{AC}^0(m)\) · Depth of a flat Boolean circuit · Gate depths of a flat Boolean circuit · Evaluation of a flat Boolean circuit · Depth of a gate · Predecessors of a gate · Value of a gate · Serial gate evaluation agrees with typed gate evaluation · Circuits of fan-in at most two · Circuits without mod gates · Monotone circuits · Circuits whose modular gates have a fixed modulus · The class NC^k · The NC hierarchy is increasing · Log-space uniform circuit families · Well-formed flat circuits · Evaluation of an encoded circuit · Gate values of a serialized circuit · Evaluation of an encoded flat circuit · Nisan-Wigderson: exponential hardness in E derandomizes BPP · Gate values of an encoded circuit

DefinitionPredecessors of a gate#✓fully proved

For a gate \(g\) of a flat Boolean circuit on \(n\) inputs, this is the list of gate indices that \(g\) reads: the empty list for an input variable or a constant, the one-element list \([a]\) for the negation of gate \(a\), and the argument list \(l\) for an and, or or mod gate with argument list \(l\) (the modulus of a mod gate is not included).

def gateInputs {n : ℕ} : ACGate n → List ℕ
  | .var _ => []
  | .const _ => []
  | .notGate a => [a]
  | .andGate l => l
  | .orGate l => l
  | .modGate _ l => l
Uses 1 · Used by 2
Statement usesGates of a flat Boolean circuit
Used byWire count of a flat circuit · Well-formed flat circuits

DefinitionWell-formed flat circuits#✓fully proved

A flat Boolean circuit on \(n\) inputs, given as a list of gates \((g_0, \dots, g_{m-1})\), is well-formed when every gate references only strictly earlier gates: for every \(j < m\), every gate index \(a\) among the inputs of \(g_j\) satisfies \(a < j\).

def WellFormedCircuit {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ j (h : j < C.length), ∀ a ∈ gateInputs (C[j]'h), a < j
Uses 2 · Used by 10
Statement usesGates of a flat Boolean circuit · Predecessors of a gate
Used byRazborov: monotone circuits for clique need superpolynomial size · Shannon: most Boolean functions need exponential circuits · Well-formed encoded circuits · Well-formed succinct 3SAT descriptors · Well-formed description circuits (Succinct Circuit Value) · The class \(\mathsf{AC}^0\) · The class \(\mathsf{AC}^0(m)\) · The class NC^k · The NC hierarchy is increasing · Nisan-Wigderson: exponential hardness in E derandomizes BPP

DefinitionValue of a gate#✓fully proved

Let \(v\) be a list of Boolean values of earlier gates, where an index outside \(v\) reads as false, and let \(\sigma\) assign a Boolean value to each of the \(n\) inputs. Given \(v\) and \(\sigma\), the value of the input variable \(x_i\) is \(\sigma(i)\); the value of the constant \(b\) is \(b\); the value of the negation of gate \(a\) is the negation of \(v_a\); the value of an and gate (or gate) with argument list \(l\) is the conjunction (disjunction) of the values \(v_a\) for \(a\) in \(l\); and the value of a mod gate with modulus \(m\) and argument list \(l\) is false if \(m = 0\), and otherwise true exactly when the number of entries \(a\) of \(l\) with \(v_a\) true, counted with repetition, is divisible by \(m\).

def gateValue {n : ℕ} (vs : List Bool) (assign : Fin n → Bool) : ACGate n → Bool
  | .var i => assign i
  | .const b => b
  | .notGate a => !(vs.getD a false)
  | .andGate l => l.all (fun a => vs.getD a false)
  | .orGate l => l.any (fun a => vs.getD a false)
  | .modGate m l =>
    if m = 0 then false
    else (l.filter (fun a => vs.getD a false)).length % m = 0
Uses 1 · Used by 2
Statement usesGates of a flat Boolean circuit
Used byEvaluation of a flat Boolean circuit · Serial gate evaluation agrees with typed gate evaluation

DefinitionEvaluation of a flat Boolean circuit#✓fully proved

For a circuit on \(n\) inputs given as a list of gates \(g_0, \dots, g_{m-1}\) and an assignment \(\alpha\) of booleans to the inputs, the list of gate values is \((v_0, \dots, v_{m-1})\), where \(v_j\) is computed from \(v_0, \dots, v_{j-1}\), a reference to a gate \(a \ge j\) reading as false: an input gate \(i\) has value \(\alpha(i)\), a constant gate has its constant, a negation gate on \(a\) has value \(\lnot v_a\), an and gate (or gate) has the conjunction (disjunction) of the values it references, and a mod gate with modulus \(k\) is true if and only if \(k \ne 0\) and the number of its references with value true, counted with multiplicity, is divisible by \(k\).

def circuitEval {n : ℕ} (C : List (ACGate n)) (assign : Fin n → Bool) : List Bool :=
  C.foldl (fun vs g => vs ++ [gateValue vs assign g]) []
Uses 2 · Used by 15
Statement usesGates of a flat Boolean circuit · Value of a gate
Used byRazborov: monotone circuits for clique need superpolynomial size · Shannon: most Boolean functions need exponential circuits · Evaluation of an encoded Boolean circuit · Gate values of an encoded circuit · Gate values of an encoded circuit (Succinct Circuit Value) · Gate values of an encoded circuit · The class \(\mathsf{AC}^0\) · The class \(\mathsf{AC}^0(m)\) · The class NC^k · The NC hierarchy is increasing · Evaluation of an encoded circuit · Gate values of a serialized circuit · Evaluation of an encoded flat circuit · Nisan-Wigderson: exponential hardness in E derandomizes BPP · Gate values of an encoded circuit

DefinitionEncoding a gate as a (kind, references) pair#✓fully proved

A gate of a flat Boolean circuit on \(n\) inputs is encoded as a pair of a natural number (its kind) and a list of natural numbers (its references), the shared encoding used by decoding-based problems such as Circuit Value and succinct circuits: the input variable \(x_i\) is encoded as \((0, [i])\); the constant true as \((1, [1])\) and the constant false as \((1, [0])\); the negation of gate \(a\) as \((2, [a])\); the conjunction of the gates listed in \(r\) as \((3, r)\); and the disjunction of the gates listed in \(r\) as \((4, r)\). Mod gates have no encoding of their own: every mod gate is encoded as \((5, [])\).

The serial evaluator reads kind \(5\) as false.

def acGateToPair {n : ℕ} : ACGate n → ℕ × List ℕ
  | .var i => (0, [i.val])
  | .const b => (1, [if b then 1 else 0])
  | .notGate a => (2, [a])
  | .andGate l => (3, l)
  | .orGate l => (4, l)
  | .modGate _ _ => (5, [])
Uses 1 · Used by 1
Statement usesGates of a flat Boolean circuit
Used byLog-space uniform circuit families

DefinitionDecoding a gate from its (kind, references) pair#✓fully proved

A pair \((k, r)\) of a natural number \(k\) and a list \(r\) of natural numbers decodes to a gate of a flat Boolean circuit on \(n\) inputs as follows: \((0, [i])\) decodes to the input variable \(x_i\) when \(i < n\) and to the constant false when \(i \ge n\); \((1, [b])\) decodes to the constant that is true if and only if \(b = 1\); \((2, [a])\) decodes to the negation of gate \(a\); \((3, r)\) decodes to the conjunction of the gates listed in \(r\); and \((4, r)\) decodes to the disjunction of the gates listed in \(r\). Every other pair, including every pair of kind \(5\) (the encoding of a mod gate), decodes to the constant false.

These defaults match the serial evaluator, which reads an unknown kind, and an input variable with no corresponding input, as false.

def acGateOfPair {n : ℕ} : ℕ × List ℕ → ACGate n
  | (0, [i]) => if h : i < n then .var ⟨i, h⟩ else .const false
  | (1, [b]) => .const (b = 1)
  | (2, [a]) => .notGate a
  | (3, l) => .andGate l
  | (4, l) => .orGate l
  | _ => .const false
Uses 1 · Used by 12
Statement usesGates of a flat Boolean circuit
Used byEvaluation of an encoded Boolean circuit · Well-formed encoded circuits · Gate values of an encoded circuit · Well-formed succinct 3SAT descriptors · Gate values of an encoded circuit (Succinct Circuit Value) · Well-formed description circuits (Succinct Circuit Value) · Gate values of an encoded circuit · Serial gate evaluation agrees with typed gate evaluation · Evaluation of an encoded circuit · Gate values of a serialized circuit · Evaluation of an encoded flat circuit · Gate values of an encoded circuit

DefinitionEvaluating a serialized gate#✓fully proved

Let \(v\) be a list of Boolean values of earlier gates, let \(a\) assign a Boolean to each of the \(n\) inputs \(0, \dots, n - 1\), and let \((k, \ell)\) be a serialized gate. Write \(v_c\) for entry \(c\) of \(v\), read as false when \(c\) is out of range. The value of the gate is: \(a(i)\) if \((k, \ell) = (0, [i])\) with \(i < n\), and false if \((k, \ell) = (0, [i])\) with \(i \ge n\); true exactly when \(b = 1\) if \((k, \ell) = (1, [b])\); the negation of \(v_c\) if \((k, \ell) = (2, [c])\); the conjunction of the \(v_c\) for \(c\) in \(\ell\) if \(k = 3\); their disjunction if \(k = 4\); and false in every other case.

def serialGateEval {n : ℕ} (vs : List Bool) (assign : Fin n → Bool)
    (g : ℕ × List ℕ) : Bool :=
  match g with
  | (0, [i]) => if h : i < n then assign ⟨i, h⟩ else false
  | (1, [b]) => b = 1
  | (2, [a]) => !(vs.getD a false)
  | (3, l) => l.all (fun a => vs.getD a false)
  | (4, l) => l.any (fun a => vs.getD a false)
  | _ => false
Used by 1
Used bySerial gate evaluation agrees with typed gate evaluation

TheoremSerial gate evaluation agrees with typed gate evaluation#✓fully proved

For every list \(v\) of Boolean values of earlier gates, every assignment of Boolean values to the \(n\) inputs and every pair \(g = (k, r)\) of a natural number \(k\) (the gate kind) and a list \(r\) of natural numbers (its references), evaluating \(g\) with the serial \((\mathrm{kind}, \mathrm{refs})\) gate evaluator gives the same value as evaluating the gate decoded from \(g\) with the gate-value function.

theorem gateValue_ofPair {n : ℕ} (vs : List Bool) (assign : Fin n → Bool)
    (g : ℕ × List ℕ) :
    serialGateEval vs assign g = gateValue vs assign (acGateOfPair g)
Uses 4
Statement usesDecoding a gate from its (kind, references) pair · Value of a gate · Evaluating a serialized gate
Proof usesGates of a flat Boolean circuit

DefinitionDepth of a gate#✓fully proved

Let \(d\) be the list of depths of the earlier gates of a flat Boolean circuit on \(n\) inputs, and for a gate index \(a\) let \(d_a\) be the entry of \(d\) at (zero-based) position \(a\), or \(0\) when \(a\) is not a position of \(d\). The depth of an input-variable gate or a constant gate is \(0\); the depth of a negation, AND, OR or modular gate is one more than the maximum of \(d_a\) over the gates \(a\) it references, where the maximum over no gates is \(0\).

def gateDepthOf (ds : List ℕ) {n : ℕ} : ACGate n → ℕ
  | .var _ => 0
  | .const _ => 0
  | .notGate a => ds.getD a 0 + 1
  | .andGate l => List.foldr max 0 (l.map (fun a => ds.getD a 0)) + 1
  | .orGate l => List.foldr max 0 (l.map (fun a => ds.getD a 0)) + 1
  | .modGate _ l => List.foldr max 0 (l.map (fun a => ds.getD a 0)) + 1
Uses 1 · Used by 1
Statement usesGates of a flat Boolean circuit
Used byGate depths of a flat Boolean circuit

DefinitionGate depths of a flat Boolean circuit#✓fully proved

For a circuit given as a list of gates \(g_0, \dots, g_{m-1}\), the list of gate depths is \((d_0, \dots, d_{m-1})\), where \(d_j = 0\) if \(g_j\) is an input or constant gate, and otherwise \(d_j\) is one more than the maximum of the depths \(d_a\) of the gates \(a\) that \(g_j\) references (the maximum over no references is \(0\)), a reference \(a \ge j\) counting as depth \(0\).

def circuitDepths {n : ℕ} (C : List (ACGate n)) : List ℕ :=
  C.foldl (fun ds g => ds ++ [gateDepthOf ds g]) []
Uses 2 · Used by 1
Statement usesGates of a flat Boolean circuit · Depth of a gate
Used byDepth of a flat Boolean circuit

DefinitionDepth of a flat Boolean circuit#✓fully proved

The depth of a circuit, given as a list of gates, is the maximum of the depths of its gates, and \(0\) for the empty circuit. Input and constant gates have depth \(0\); a negation, and, or or mod gate has depth one more than the maximum depth of the gates it references (the maximum over no references is \(0\)), where a reference to a gate that does not come earlier in the list counts as depth \(0\).

def circuitDepth {n : ℕ} (C : List (ACGate n)) : ℕ :=
  List.foldr max 0 (circuitDepths C)
Uses 2 · Used by 4
Statement usesGates of a flat Boolean circuit · Gate depths of a flat Boolean circuit
Used byThe class \(\mathsf{AC}^0\) · The class \(\mathsf{AC}^0(m)\) · The class NC^k · The NC hierarchy is increasing

DefinitionCircuits without mod gates#✓fully proved

A flat Boolean circuit \(C\) on \(n\) inputs is mod-free when none of its gates is a mod gate.

def IsModFree {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ g ∈ C, match g with
    | .modGate _ _ => False
    | _ => True
Uses 1 · Used by 5
Statement usesGates of a flat Boolean circuit
Used byShannon: most Boolean functions need exponential circuits · The class \(\mathsf{AC}^0\) · The class NC^k · The NC hierarchy is increasing · Nisan-Wigderson: exponential hardness in E derandomizes BPP

DefinitionCircuits whose modular gates have a fixed modulus#✓fully proved

For a natural number \(m\), a flat Boolean circuit on \(n\) inputs satisfies the modulus-\(m\) condition when every \(\mathrm{mod}\) gate in it has modulus exactly \(m\); gates of the other kinds are unrestricted.

def ModOnly {n : ℕ} (m : ℕ) (C : List (ACGate n)) : Prop :=
  ∀ g ∈ C, match g with
    | .modGate m' _ => m' = m
    | _ => True
Uses 1 · Used by 1
Statement usesGates of a flat Boolean circuit
Used byThe class \(\mathsf{AC}^0(m)\)

DefinitionMonotone circuits#✓fully proved

A flat circuit \(C\) on \(n\) input variables, given as a list of gates, is monotone when every gate of \(C\) is an input variable, an AND gate or an OR gate. Constant, NOT and mod gates are not allowed.

def IsMonotoneCircuit {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ g ∈ C, match g with
    | .var _ => True
    | .andGate _ => True
    | .orGate _ => True
    | _ => False
Uses 1 · Used by 1
Statement usesGates of a flat Boolean circuit
Used byRazborov: monotone circuits for clique need superpolynomial size

DefinitionThe class \(\mathsf{AC}^0\)#✓fully proved

A decision problem \(L\) on bitstrings is in \(\mathsf{AC}^0\) when there are a depth bound \(d\), a polynomial \(p\) with natural-number coefficients and, for every \(n\), a flat Boolean circuit \(C_n\) on \(n\) inputs such that for every \(n\): every gate of \(C_n\) refers only to earlier gates; \(C_n\) has no mod gates; \(C_n\) has at most \(p(n)\) gates and depth at most \(d\); and for every bitstring \(x\) of length \(n\), \(L(x)\) is true if and only if \(C_n\) has a last gate and the value of that gate on input \(x\) is true.

The and and or gates have unbounded fan-in, and the family \((C_n)\) need not be uniform.

def AC0 : DecisionComplexityClass :=
  {L | ∃ d, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
    ∀ n, WellFormedCircuit (C n) ∧ IsModFree (C n) ∧ (C n).length ≤ p.eval n ∧
      circuitDepth (C n) ≤ d ∧
      ∀ x : List Bool, x.length = n →
        (L x = true ↔
          (circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}
Uses 7 · Used by 2
Statement usesGates of a flat Boolean circuit · Circuits without mod gates · Well-formed flat circuits · Depth of a flat Boolean circuit · Evaluation of a flat Boolean circuit · Complexity classes · Decision problems
Used byMajority is not in AC0 · Parity is not in AC0

DefinitionThe class \(\mathsf{AC}^0(m)\)#✓fully proved

For a natural number \(m\), a decision problem \(L\) on bitstrings is in \(\mathsf{AC}^0[m]\) when there are a depth bound \(d\), a polynomial \(p\) with natural-number coefficients and, for every \(n\), a flat Boolean circuit \(C_n\) on \(n\) inputs such that for every \(n\): every gate of \(C_n\) refers only to earlier gates; every mod gate of \(C_n\) has modulus \(m\); \(C_n\) has at most \(p(n)\) gates and depth at most \(d\); and for every bitstring \(x\) of length \(n\), \(L(x)\) is true if and only if \(C_n\) has a last gate and the value of that gate on input \(x\) is true.

The and and or gates have unbounded fan-in, the family \((C_n)\) need not be uniform, and a circuit with no mod gates also qualifies.

def AC0Mod (m : ℕ) : DecisionComplexityClass :=
  {L | ∃ d, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
    ∀ n, WellFormedCircuit (C n) ∧ ModOnly m (C n) ∧ (C n).length ≤ p.eval n ∧
      circuitDepth (C n) ≤ d ∧
      ∀ x : List Bool, x.length = n →
        (L x = true ↔
          (circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}
Uses 7 · Used by 2
Statement usesGates of a flat Boolean circuit · Circuits whose modular gates have a fixed modulus · Well-formed flat circuits · Depth of a flat Boolean circuit · Evaluation of a flat Boolean circuit · Complexity classes · Decision problems
Used bySmolensky: parity is not in AC0(mod 3) · The class \(\mathsf{ACC}^0\)

DefinitionThe class \(\mathsf{ACC}^0\)#✓fully proved

\(\mathsf{ACC}^0\) is the union of the classes \(\mathsf{AC}^0[m]\) over all natural numbers \(m\): a decision problem is in \(\mathsf{ACC}^0\) when it is in \(\mathsf{AC}^0[m]\) for some \(m\). A circuit family witnessing membership uses one fixed modulus \(m\) throughout.

def ACC0 : DecisionComplexityClass := ⋃ m, AC0Mod m
Uses 3 · Used by 1
Statement usesThe class \(\mathsf{AC}^0(m)\) · Complexity classes · Decision problems
Used byWilliams: NEXP is not contained in ACC0

DefinitionThe parity language#✓fully proved

The parity decision problem accepts a bitstring exactly when an odd number of its entries are true.

def parityDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x : List Bool => decide ((x.filter fun b => b).length % 2 = 1)
Uses 1 · Used by 2
Statement usesDecision problems
Used byParity is not in AC0 · Smolensky: parity is not in AC0(mod 3)

DefinitionThe majority language#✓fully proved

The majority language is the decision problem that accepts a bitstring \(x\) exactly when \(x\) has more true bits than false bits, that is, when \(2k > |x|\), where \(k\) is the number of true bits of \(x\) and \(|x|\) is its length.

def majorityDec : MetaMathlibExt.ComplexityTheory.DecisionProblem :=
  fun x : List Bool => decide (2 * (x.filter fun b => b).length > x.length)
Uses 1 · Used by 1
Statement usesDecision problems
Used byMajority is not in AC0

DefinitionThe class RP#✓fully proved

A decision problem \(L\) is in \(\mathsf{RP}\) when there are a polynomial \(p\) with natural-number coefficients and a polynomial-time computable Boolean function \(R\) on pairs of bitstrings such that for every bitstring \(x\): if \(L(x)\) is true, then \(R(x, r)\) is true for at least half of the \(2^{p(|x|)}\) bitstrings \(r\) of length \(p(|x|)\); and if \(L(x)\) is false, then \(R(x, r)\) is false for every bitstring \(r\) of length \(p(|x|)\).

def RP : DecisionComplexityClass :=
  {L | ∃ p : Polynomial ℕ, ∃ R : List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        2 * Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} ≥
          2 ^ (p.eval x.length)) ∧
      (L x = false →
        Set.ncard {r : Fin (p.eval x.length) → Bool | R (x, List.ofFn r) = true} = 0)}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2; M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 10.8.
Uses 11 · Used by 8
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 byThe class coRP · Membership in coRP · ZPP · ZPP is the intersection of RP and coRP · ZPP is contained in coRP · ZPP is contained in RP · RP is contained in BPP · RP is contained in NP

DefinitionThe class coRP#✓fully proved

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

def coRP : DecisionComplexityClass := {L | Lᶜ ∈ RP}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2; M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 10.8.
Uses 3 · Used by 5
Statement usesThe class RP · Complexity classes · Decision problems
Used byMembership in coRP · ZPP · ZPP is the intersection of RP and coRP · ZPP is contained in coRP · ZPP is contained in RP

TheoremMembership in coRP#✓fully proved

A decision problem \(L\) belongs to \(\mathsf{coRP}\) if and only if its complement, the decision problem that accepts exactly the bitstrings \(L\) rejects, belongs to \(\mathsf{RP}\).

theorem mem_coRP {L : DecisionProblem} : L ∈ coRP ↔ Lᶜ ∈ RP
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2.
Uses 4
Statement usesThe class RP · The class coRP · Complexity classes · Decision problems

DefinitionZPP#✓fully proved

The class \(\mathsf{ZPP}\) (zero-error probabilistic polynomial time) is defined as the set of decision problems that lie in both \(\mathsf{RP}\) and \(\mathsf{coRP}\), that is, \(\mathsf{ZPP} = \mathsf{RP} \cap \mathsf{coRP}\).

def ZPP : DecisionComplexityClass := RP ∩ coRP
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2 (where ZPP is defined as this intersection); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 10.8.
Uses 4 · Used by 3
Statement usesThe class RP · The class coRP · Complexity classes · Decision problems
Used byZPP is the intersection of RP and coRP · ZPP is contained in coRP · ZPP is contained in RP

TheoremZPP is the intersection of RP and coRP#✓fully proved

The class \(\mathsf{ZPP}\) equals \(\mathsf{RP} \cap \mathsf{coRP}\); here this holds by definition.

theorem zpp_eq : ZPP = RP ∩ coRP
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2.
Uses 5
Statement usesThe class RP · ZPP · The class coRP · Complexity classes · Decision problems

TheoremZPP is contained in RP#✓fully proved

Every decision problem in \(\mathsf{ZPP}\) lies in \(\mathsf{RP}\), that is, \(\mathsf{ZPP} \subseteq \mathsf{RP}\).

theorem zpp_subset_rp : ZPP ⊆ RP
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2.
Uses 5
Statement usesThe class RP · ZPP · Complexity classes · Decision problems
Proof usesThe class coRP

TheoremZPP is contained in coRP#✓fully proved

Every decision problem in \(\mathsf{ZPP}\) lies in \(\mathsf{coRP}\), that is, \(\mathsf{ZPP} \subseteq \mathsf{coRP}\).

theorem zpp_subset_corp : ZPP ⊆ coRP
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 7.2.
Uses 5
Statement usesZPP · The class coRP · Complexity classes · Decision problems
Proof usesThe class RP

DefinitionThe class MA (Merlin–Arthur)#✓fully proved

A decision problem \(L\) is in \(\mathsf{MA}\) when there are polynomials \(p\) and \(q\) with natural-number coefficients and a polynomial-time computable predicate \(R\) on triples \((x, w, r)\) of bitstrings such that, for every bitstring \(x\), with \(N_x(w)\) the number of strings \(r\) of length \(p(|x|)\) for which \(R(x, w, r)\) is true: if \(L(x)\) is true, then some \(w\) with \(|w| \le q(|x|)\) satisfies \(3 N_x(w) \ge 2 \cdot 2^{p(|x|)}\); and if \(L(x)\) is false, then every \(w\) with \(|w| \le q(|x|)\) satisfies \(3 N_x(w) \le 2^{p(|x|)}\).

So Merlin sends a witness \(w\) first and Arthur then flips \(p(|x|)\) coins \(r\): Arthur accepts with probability at least \(2/3\) for some \(w\) on yes-instances, and with probability at most \(1/3\) for every \(w\) on no-instances. In the class AM the random string comes before the witness.

def MA : DecisionComplexityClass :=
  {L | ∃ p q : Polynomial ℕ,
    ∃ R : List Bool × List Bool × List Bool → Bool, IsPolyTime R ∧
    ∀ x,
      (L x = true →
        ∃ w : List Bool, w.length ≤ q.eval x.length ∧
          3 * Set.ncard {r : Fin (p.eval x.length) → Bool |
            R (x, w, List.ofFn r) = true} ≥ 2 * 2 ^ (p.eval x.length)) ∧
      (L x = false →
        ∀ w : List Bool, w.length ≤ q.eval x.length →
          3 * Set.ncard {r : Fin (p.eval x.length) → Bool |
            R (x, w, List.ofFn r) = true} ≤ 2 ^ (p.eval x.length))}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 8.1; L. Babai, "Trading group theory for randomness", Proceedings of the Seventeenth Annual ACM Symposium on Theory of Computing (STOC 1985), 421-429.
Uses 11 · Used by 4
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 byThe class coMA · Membership in coMA · MA is contained in AM · MA is contained in PH

DefinitionThe class coMA#✓fully proved

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

def coMA : DecisionComplexityClass := {L | Lᶜ ∈ MA}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 8.1.
Uses 3 · Used by 1
Statement usesThe class MA (Merlin–Arthur) · Complexity classes · Decision problems
Used byMembership in coMA

TheoremMembership in coMA#✓fully proved

A decision problem \(L\) belongs to \(\mathsf{coMA}\) if and only if its complement, the decision problem that accepts exactly the bitstrings \(L\) rejects, belongs to \(\mathsf{MA}\).

theorem mem_coMA {L : DecisionProblem} : L ∈ coMA ↔ Lᶜ ∈ MA
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 8.1.
Uses 4
Statement usesThe class MA (Merlin–Arthur) · The class coMA · Complexity classes · Decision problems

AbbreviationSerial circuits#✓fully proved

A serial circuit is a list of pairs \((k, \ell)\), where \(k\) is a natural number (the gate kind) and \(\ell\) is a list of natural numbers (the gate's references).

A flat circuit is serialized gate by gate into this form: kind \(0\) is an input variable, kind \(1\) a constant, kind \(2\) a negation, kind \(3\) a conjunction and kind \(4\) a disjunction, while a modular-counting gate, which has no serial form here, becomes \((5, [\,])\).

abbrev SerialCircuit := List (ℕ × List ℕ)
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 6 (circuit encodings).

DefinitionLog-space uniform circuit families#✓fully proved

A family \((C_n)_{n \in \mathbb{N}}\) of flat Boolean circuits, \(C_n\) having \(n\) inputs, is log-space uniform when there is a log-space computable function \(D\) on bitstrings such that, for every \(n\), decoding \(D(1^n)\) (where \(1^n\) is the string of \(n\) ones) as a list of (gate kind, references) pairs succeeds and returns the serial encoding of \(C_n\), that is, the list of the serial encodings of its gates in order. Since \(1^n\) has length \(n\), the description is computed in space \(O(\log n)\).

def UniformCircuitFamily (C : (n : ℕ) → List (ACGate n)) : Prop :=
  ∃ desc : List Bool → List Bool, LogSpaceComputable desc ∧
    ∀ n, MetaMathlibExt.BitstringEncoding.bitDecode
      (desc (List.replicate n true)) = some ((C n).map acGateToPair)
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21 (log-space uniformity); M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 9.20.
Uses 11 · Used by 2
Statement usesGates of a flat Boolean circuit · Log-space computable functions · Encoding a gate as a (kind, references) pair · Bitstring 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
Used byThe class NC^k · The NC hierarchy is increasing

DefinitionCircuits of fan-in at most two#✓fully proved

A flat Boolean circuit \(C\) on \(n\) inputs has fan-in at most two when every and gate, or gate and mod gate of \(C\) has an argument list of length at most \(2\).

Bounded fan-in is what \(\mathsf{NC}\) requires: without it, the \(\mathsf{NC}^k\) circuit classes would be the unbounded-fan-in classes \(\mathsf{AC}^k\).

def IsFanInLeTwo {n : ℕ} (C : List (ACGate n)) : Prop :=
  ∀ g ∈ C, match g with
    | .andGate l => l.length ≤ 2
    | .orGate l => l.length ≤ 2
    | .modGate _ l => l.length ≤ 2
    | _ => True
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21; M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 9.20.
Uses 1 · Used by 2
Statement usesGates of a flat Boolean circuit
Used byThe class NC^k · The NC hierarchy is increasing

DefinitionThe class NC^k#✓fully proved

For a natural number \(k\), a decision problem \(L\) is in \(\mathsf{NC}^k\) when there are a constant \(c\), a polynomial \(p\) with natural number coefficients and a log-space uniform family of flat Boolean circuits \((C_n)_{n \in \mathbb{N}}\), where \(C_n\) has \(n\) inputs, such that for every \(n\) the circuit \(C_n\) is well formed, has no \(\mathrm{mod}\) gates, has at most two inputs at every and gate and every or gate, has at most \(p(n)\) gates, has depth at most \(c \cdot (\lfloor \log_2 (n + 1) \rfloor + 1)^k\), and, for every bitstring \(x\) of length \(n\), \(L\) accepts \(x\) exactly when \(C_n\) has a last gate and that gate evaluates to true on input \(x\).

So \(\mathsf{NC}^k\) consists of the problems decided by log-space uniform circuit families of polynomial size, fan-in at most \(2\) and depth \(O(\log^k n)\), and \(\mathsf{NC}^0\) is constant depth. Bounded fan-in is essential: with unbounded fan-in this would be \(\mathsf{AC}^k\).

def NCK (k : ℕ) : DecisionComplexityClass :=
  {L | ∃ c, ∃ p : Polynomial ℕ, ∃ C : (n : ℕ) → List (ACGate n),
    UniformCircuitFamily C ∧
    ∀ n, WellFormedCircuit (C n) ∧ IsModFree (C n) ∧ IsFanInLeTwo (C n) ∧
      (C n).length ≤ p.eval n ∧
      circuitDepth (C n) ≤ c * (Nat.log 2 (n + 1) + 1) ^ k ∧
      ∀ x : List Bool, x.length = n →
        (L x = true ↔
          (circuitEval (C n) (fun i => x.getD (i : ℕ) false)).getLast? = some true)}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21; M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 9.20.
Uses 9 · Used by 5
Statement usesGates of a flat Boolean circuit · Circuits of fan-in at most two · Circuits without mod gates · Log-space uniform circuit families · Well-formed flat circuits · Depth of a flat Boolean circuit · Evaluation of a flat Boolean circuit · Complexity classes · Decision problems
Used byNC^1 is contained in L · Membership in NC · The class NC · NC is the union of its levels · The NC hierarchy is increasing

DefinitionThe class NC#✓fully proved

\(\mathsf{NC}\) is the complexity class of decision problems that belong to \(\mathsf{NC}^k\) for some natural number \(k\), that is, \(\mathsf{NC} = \bigcup_{k} \mathsf{NC}^k\).

def NC : DecisionComplexityClass := ⋃ k, NCK k
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21; M. Sipser, Introduction to the Theory of Computation, 3rd ed., 2013, Definition 9.20.
Uses 3 · Used by 3
Statement usesThe class NC^k · Complexity classes · Decision problems
Used byNC is contained in P · Membership in NC · NC is the union of its levels

TheoremNC is the union of its levels#✓fully proved

The class \(\mathsf{NC}\) equals the union \(\bigcup_{k \in \mathbb{N}} \mathsf{NC}^k\) of the classes \(\mathsf{NC}^k\) over all natural numbers \(k\); this holds by definition.

theorem nc_eq : NC = ⋃ k, NCK k
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21.
Uses 4
Statement usesThe class NC · The class NC^k · Complexity classes · Decision problems

TheoremMembership in NC#✓fully proved

A decision problem \(L\) belongs to \(\mathsf{NC}\) if and only if \(L\) belongs to \(\mathsf{NC}^k\) for some natural number \(k\).

theorem mem_nc {L : DecisionProblem} : L ∈ NC ↔ ∃ k, L ∈ NCK k
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21.
Uses 4
Statement usesThe class NC · The class NC^k · Complexity classes · Decision problems

TheoremThe NC hierarchy is increasing#✓fully proved

For every natural number \(k\), every decision problem in \(\mathsf{NC}^k\) is in \(\mathsf{NC}^{k+1}\), that is, \(\mathsf{NC}^k \subseteq \mathsf{NC}^{k+1}\).

The depth bound of \(\mathsf{NC}^k\), a constant times \((\lfloor \log_2 (n + 1) \rfloor + 1)^k\), is monotone in \(k\) because its base is at least \(1\).

theorem nck_mono {k : ℕ} : NCK k ⊆ NCK (k + 1)
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 6.21.
Uses 10
Statement usesThe class NC^k · Complexity classes · Decision problems
Proof usesGates of a flat Boolean circuit · Circuits of fan-in at most two · Circuits without mod gates · Log-space uniform circuit families · Well-formed flat circuits · Depth of a flat Boolean circuit · Evaluation of a flat Boolean circuit

AbbreviationEncoded rational number#✓fully proved

A rational number is encoded as a triple \((s, a, b)\) of a boolean \(s\) and natural numbers \(a\) and \(b\), read as the sign, the numerator and the denominator.

abbrev RatEnc := Bool × ℕ × ℕ
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4 (rational gate entries).
Used by 13
Used byApplying a 2-local gate to a state · BQP · Matrix encoded by a list of entries · Encoded 2-local quantum gate · Well-formed quantum gate · Complex number of a pair of rational encodings · Rational number of an encoding · Embedding of a 2-local term into \(n\) qubits · No-instances of the 2-local Hamiltonian problem · Yes-instances of the 2-local Hamiltonian problem · Encoded 2-local Hamiltonian term · Valid 2-local Hamiltonian term · QMA for promise problems

DefinitionRational number of an encoding#✓fully proved

A triple \((s, p, q)\), with \(s\) a boolean and \(p, q\) natural numbers, encodes the rational number \(-p/q\) when \(s\) is true and \(p/q\) when \(s\) is false; when \(q = 0\) the value is \(0\), since division by zero gives \(0\).

def toRat (e : RatEnc) : ℚ :=
  (if e.1 then -1 else 1) * (e.2.1 : ℚ) / (e.2.2 : ℚ)
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 1 · Used by 3
Statement usesEncoded rational number
Used byComplex number of a pair of rational encodings · No-instances of the 2-local Hamiltonian problem · Yes-instances of the 2-local Hamiltonian problem

DefinitionComplex number of a pair of rational encodings#✓fully proved

A pair \((e_1, e_2)\) of rational encodings encodes the complex number \(q_1 + q_2 i\), where \(q_1\) and \(q_2\) are the rational numbers encoded by \(e_1\) and \(e_2\).

def toComplex (e : RatEnc × RatEnc) : ℂ :=
  ⟨((toRat e.1 : ℚ) : ℝ), ((toRat e.2 : ℚ) : ℝ)⟩
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 2 · Used by 1
Statement usesEncoded rational number · Rational number of an encoding
Used byMatrix encoded by a list of entries

DefinitionBinary digit of a natural number#✓fully proved

For natural numbers \(k\) and \(i\), this is the digit of \(i\) at position \(k\) in binary, counting from the least significant digit at position \(0\), that is, \(\lfloor i / 2^k \rfloor \bmod 2\), taken as an element of \(\{0, 1\}\).

def qBit (k i : ℕ) : Fin 2 :=
  ⟨(i / 2 ^ k) % 2, Nat.mod_lt _ (by norm_num)⟩
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Used by 4
Used byAcceptance probability of a quantum state · Applying a 2-local gate to a state · Setting two bits of an index · Embedding of a 2-local term into \(n\) qubits

DefinitionIndex of a pair of bits#✓fully proved

A pair \((a, b)\) of bits \(a, b \in \{0, 1\}\) has index \(2a + b\), its position in the enumeration \((0, 0), (0, 1), (1, 0), (1, 1)\) of the four pairs.

def qIdx2 (p : Fin 2 × Fin 2) : ℕ := p.1.val * 2 + p.2.val
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Used by 1
Used byMatrix encoded by a list of entries

DefinitionMatrix encoded by a list of entries#✓fully proved

Number the pairs \((a, b)\) with \(a, b \in \{0, 1\}\) by \(2a + b\), and index the rows and columns of a \(4 \times 4\) complex matrix by these pairs. Given a list \(e\) of pairs of encoded rational numbers, the matrix of \(e\) has in row \(p\) and column \(q\) the complex number whose real part is the first and whose imaginary part is the second rational of the entry of \(e\) at position \(4p + q\) (counting from \(0\), with \(p\) and \(q\) replaced by their numbers), and \(0\) when \(e\) has no entry at that position. A list of \(16\) pairs thus lists the entries in row-major order.

def matrixOfEntries (entries : List (RatEnc × RatEnc)) :
    Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ :=
  fun p q =>
    toComplex (entries.getD (qIdx2 p * 4 + qIdx2 q) ((false, 0, 1), (false, 0, 1)))
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 3 · Used by 4
Statement usesEncoded rational number · Index of a pair of bits · Complex number of a pair of rational encodings
Used byApplying a 2-local gate to a state · Well-formed quantum gate · Embedding of a 2-local term into \(n\) qubits · Valid 2-local Hamiltonian term

DefinitionSetting two bits of an index#✓fully proved

For natural numbers \(N\), \(s\), \(i\), \(j\) and a pair \(b = (b_1, b_2)\) of bits, this is the index in \(\{0, \dots, 2^N - 1\}\) given by \((s - s_i 2^i - s_j 2^j + b_1 2^i + b_2 2^j) \bmod 2^N\), where \(s_k\) is bit \(k\) of \(s\) and each subtraction of natural numbers is truncated at \(0\). When \(i \ne j\) this is \(s\) with bit \(i\) set to \(b_1\) and bit \(j\) set to \(b_2\), reduced modulo \(2^N\).

def setBits (N s i j : ℕ) (b : Fin 2 × Fin 2) : Fin (2 ^ N) :=
  ⟨(s - (qBit i s).val * 2 ^ i - (qBit j s).val * 2 ^ j +
    b.1.val * 2 ^ i + b.2.val * 2 ^ j) % 2 ^ N, Nat.mod_lt _ (by positivity)⟩
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 1 · Used by 1
Statement usesBinary digit of a natural number
Used byApplying a 2-local gate to a state

AbbreviationEncoded 2-local quantum gate#✓fully proved

A 2-local quantum gate is encoded as a triple \((i, j, e)\) of natural numbers \(i\) and \(j\), the qubits it acts on, and a list \(e\) of pairs of encoded rational numbers, the real and imaginary parts of the entries of its \(4 \times 4\) matrix in row-major order.

The encoding itself does not require \(e\) to have \(16\) entries or the matrix to be unitary; unitarity and the qubit bounds are part of well-formedness.

abbrev QGate := ℕ × ℕ × List (RatEnc × RatEnc)
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 1 · Used by 5
Statement usesEncoded rational number
Used byApplying a quantum circuit to a state · Applying a 2-local gate to a state · BQP · Well-formed quantum gate · QMA for promise problems

DefinitionWell-formed quantum gate#✓fully proved

A 2-local gate acting on qubits \(i\) and \(j\) with entry list \(e\) is well-formed on \(N\) qubits when \(i < j < N\) and the \(4 \times 4\) complex matrix \(U\) encoded by \(e\) is unitary, that is, \(U^* U = I\).

def QGateWellFormed (N : ℕ) (gate : QGate) : Prop :=
  gate.1 < gate.2.1 ∧ gate.2.1 < N ∧
    (star (matrixOfEntries gate.2.2)) * (matrixOfEntries gate.2.2) = 1
Sources
  • A. Y. Kitaev, A. H. Shen, and M. N. Vyalyi, Classical and Quantum Computation, American Mathematical Society, 2002, Section 14.4.
Uses 3 · Used by 2
Statement usesEncoded 2-local quantum gate · Encoded rational number · Matrix encoded by a list of entries
Used byBQP · QMA for promise problems

DefinitionApplying a 2-local gate to a state#✓fully proved

Let \(N\) be a number of qubits, and let a gate consist of two qubit positions \(i\) and \(j\) together with a list of entries encoding a \(4 \times 4\) complex matrix \(U\) whose rows and columns are indexed by pairs of bits. For a state vector \(\psi\) on \(N\) qubits, that is, a function from \(\{0, \dots, 2^N - 1\}\) to \(\mathbb{C}\), applying the gate gives the state whose value at a basis index \(s\) is \(\sum_{b \in \{0,1\}^2} U_{(s_i, s_j), b} \, \psi(s[b])\). Here \(s_k = \lfloor s / 2^k \rfloor \bmod 2\) is bit \(k\) of \(s\), and for \(b = (b_1, b_2)\) the index \(s[b]\) is \((s - s_i 2^i - s_j 2^j + b_1 2^i + b_2 2^j) \bmod 2^N\), with truncated subtraction of natural numbers; when \(i \ne j\) and \(i, j < N\), this is \(s\) with bits \(i\) and \(j\) replaced by \(b_1\) and \(b_2\).

def applyGate (N : ℕ) (gate : QGate) (ψ : Fin (2 ^ N) → ℂ) : Fin (2 ^ N) → ℂ :=
  fun s => ∑ b : Fin 2 × Fin 2,
    (matrixOfEntries gate.2.2) (qBit gate.1 s.val, qBit gate.2.1 s.val) b *
      ψ (setBits N s.val gate.1 gate.2.1 b)
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 4 (unitary evolution).
Uses 5 · Used by 1
Statement usesEncoded 2-local quantum gate · Encoded rational number · Matrix encoded by a list of entries · Binary digit of a natural number · Setting two bits of an index
Used byApplying a quantum circuit to a state

DefinitionApplying a quantum circuit to a state#✓fully proved

For a state vector \(\psi \in \mathbb{C}^{2^N}\) on \(N\) qubits and a list of 2-local gates \(g_1, \dots, g_k\), the result of applying the circuit to \(\psi\) is obtained by applying the gate \(g_1\) to \(\psi\), then \(g_2\) to the result, and so on up to \(g_k\). For the empty list it is \(\psi\) itself.

def applyCircuit (N : ℕ) (gates : List QGate) (ψ : Fin (2 ^ N) → ℂ) :
    Fin (2 ^ N) → ℂ :=
  gates.foldl (fun ψ g => applyGate N g ψ) ψ
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 4 (quantum circuits).
Uses 2 · Used by 2
Statement usesEncoded 2-local quantum gate · Applying a 2-local gate to a state
Used byBQP · QMA for promise problems

DefinitionNumber with a given binary expansion#✓fully proved

A list \(b_0, b_1, \ldots, b_{n-1}\) of booleans, read as bits with true as \(1\) and false as \(0\), denotes the natural number \(\sum_{i < n} b_i 2^i\); the first entry is the least significant bit.

def qNumOf : List Bool → ℕ
  | [] => 0
  | b :: rest => (if b then 1 else 0) + 2 * qNumOf rest
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 1 (computational basis).
Used by 1
Used byComputational basis state of a bitstring

DefinitionComputational basis state of a bitstring#✓fully proved

For a bitstring \(x = (x_0, \dots, x_{n-1})\), reading true as \(1\) and false as \(0\), the computational basis state of \(x\) is the vector \(\psi : \{0, \dots, 2^n - 1\} \to \mathbb{C}\) with \(\psi(s) = 1\) if \(s = \sum_{k < n} x_k 2^k\) (the number whose binary expansion is \(x\), least significant bit first) and \(\psi(s) = 0\) otherwise.

def basisState (x : List Bool) : Fin (2 ^ x.length) → ℂ :=
  fun s => if s.val = qNumOf x then 1 else 0
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 1 (computational basis).
Uses 1 · Used by 2
Statement usesNumber with a given binary expansion
Used byInitial state of a BQP computation · Initial state of a QMA verifier

DefinitionTensor product of state vectors#✓fully proved

For vectors \(\varphi \in \mathbb{C}^{2^a}\) and \(\psi \in \mathbb{C}^{2^b}\), indexed by \(\{0, \dots, 2^a - 1\}\) and \(\{0, \dots, 2^b - 1\}\), their tensor product is the vector in \(\mathbb{C}^{2^{a+b}}\) whose entry at \(s\) is \(\varphi_{s \bmod 2^a}\, \psi_{\lfloor s / 2^a \rfloor}\). Thus \(\varphi\) occupies the low-order \(a\) bits of the index and \(\psi\) the high-order \(b\) bits.

def tensorProd {a b : ℕ} (φ : Fin (2 ^ a) → ℂ) (ψ : Fin (2 ^ b) → ℂ) :
    Fin (2 ^ (a + b)) → ℂ :=
  fun s => φ ⟨s.val % 2 ^ a, Nat.mod_lt _ (by positivity)⟩ *
    ψ ⟨s.val / 2 ^ a, by
      have h : s.val < 2 ^ b * 2 ^ a := by
        calc s.val < 2 ^ (a + b) := s.isLt
          _ = 2 ^ a * 2 ^ b := by rw [pow_add]
          _ = 2 ^ b * 2 ^ a := by rw [Nat.mul_comm]
      exact (Nat.div_lt_iff_lt_mul (by positivity)).mpr h⟩
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 2 (tensor products).
Used by 2
Used byInitial state of a BQP computation · Initial state of a QMA verifier

DefinitionAll-zero state#✓fully proved

The all-zero state on \(a\) qubits is the vector in \(\mathbb{C}^{2^a}\), indexed by \(s \in \{0, \dots, 2^a - 1\}\), whose entry at \(s = 0\) is \(1\) and whose other entries are \(0\); that is, the computational basis state \(|0 \cdots 0\rangle\).

def zeroState (a : ℕ) : Fin (2 ^ a) → ℂ :=
  fun s => if s.val = 0 then 1 else 0
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 1 (computational basis).
Used by 2
Used byInitial state of a BQP computation · Initial state of a QMA verifier

DefinitionSquared norm of a state vector#✓fully proved

For a vector \(\psi \in \mathbb{C}^{2^m}\), indexed by \(\{0, \dots, 2^m - 1\}\), its squared norm is the real number \(\sum_{s} \overline{\psi_s}\, \psi_s = \sum_{s} |\psi_s|^2\).

def sqNorm {m : ℕ} (ψ : Fin (2 ^ m) → ℂ) : ℝ :=
  ∑ s : Fin (2 ^ m), (starRingEnd ℂ (ψ s) * ψ s).re
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 2 (Born rule).
Used by 1
Used byQMA for promise problems

DefinitionAcceptance probability of a quantum state#✓fully proved

For a state vector \(\psi\) on \(N\) qubits, given by its amplitudes \(\psi(s) \in \mathbb{C}\) at the basis states \(s \in \{0, \dots, 2^N - 1\}\), the acceptance probability is the sum of \(|\psi(s)|^2\) over the basis states \(s\) whose qubit \(0\) (the output qubit, the least significant bit of \(s\)) equals \(1\). By the Born rule, for a unit vector \(\psi\) this is the probability that measuring the output qubit gives \(1\).

def acceptProb {N : ℕ} (ψ : Fin (2 ^ N) → ℂ) : ℝ :=
  ∑ s : Fin (2 ^ N), if qBit 0 s.val = 1 then (starRingEnd ℂ (ψ s) * ψ s).re else 0
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 2 (Born rule, measurement).
Uses 1 · Used by 2
Statement usesBinary digit of a natural number
Used byBQP · QMA for promise problems

DefinitionInitial state of a BQP computation#✓fully proved

For a bitstring \(x = (x_0, \dots, x_{n-1})\), with true read as \(1\) and false as \(0\), and a number \(a\) of ancilla qubits, the initial state is the tensor product of the computational basis state of \(x\) and the all-zero state on \(a\) qubits: the vector on \(\{0, \dots, 2^{n+a} - 1\}\) whose value at \(s\) is the value of the basis state of \(x\) at \(s \bmod 2^n\) times the value of the all-zero state at \(\lfloor s / 2^n \rfloor\). So \(x\) occupies the \(n\) low-order bits of the index, and the state equals \(1\) at the index \(\sum_{k < n} x_k 2^k\) and \(0\) elsewhere.

def bqpInitState (x : List Bool) (a : ℕ) : Fin (2 ^ (x.length + a)) → ℂ :=
  tensorProd (basisState x) (zeroState a)
Sources
  • M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 4 (quantum circuits); S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 10.1.
Uses 3 · Used by 1
Statement usesComputational basis state of a bitstring · Tensor product of state vectors · All-zero state
Used byBQP

DefinitionBQP#✓fully proved

The class BQP of bounded-error quantum polynomial-time decision problems consists of the decision problems \(L\) for which there are polynomials \(a\) and \(q\) with natural number coefficients and a polynomial-time computable map sending each bitstring \(x\) to a list of 2-local quantum gates such that, for every bitstring \(x\), with \(n = |x|\) and \(N = n + a(n)\): the list has at most \(q(n)\) gates; each gate acts on qubits \(i < j < N\) and its \(4 \times 4\) matrix, whose entries have rational real and imaginary parts, is unitary; and after the gates are applied in order to the state with \(x\) in the computational basis on the \(n\) low-order qubits and \(a(n)\) ancilla qubits in state \(0\), the probability that qubit \(0\) measures \(1\) is at least \(2/3\) if \(L(x)\) is true and at most \(1/3\) if \(L(x)\) is false.

def BQP : DecisionComplexityClass :=
  {L | ∃ a s : Polynomial ℕ, ∃ gates : List Bool → List QGate,
    IsPolyTime gates ∧
    (∀ x, (gates x).length ≤ s.eval x.length) ∧
    (∀ x, ∀ g ∈ gates x, QGateWellFormed (x.length + a.eval x.length) g) ∧
    ∀ x,
      (L x = true →
        2 / 3 ≤ acceptProb
          (applyCircuit (x.length + a.eval x.length) (gates x)
            (bqpInitState x (a.eval x.length)))) ∧
      (L x = false → acceptProb
          (applyCircuit (x.length + a.eval x.length) (gates x)
            (bqpInitState x (a.eval x.length))) ≤ 1 / 3)}
Sources
  • S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Definition 10.1; M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge University Press, 2000, Chapter 4; E. Bernstein and U. Vazirani, "Quantum complexity theory", SIAM Journal on Computing 26 (1997), 1411-1473.
Uses 17 · Used by 2
Statement usesEncoded 2-local quantum gate · Well-formed quantum gate · Encoded rational number · Acceptance probability of a quantum state · Applying a quantum circuit to a state · Initial state of a BQP computation · Bitstring 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 byBQP is contained in PP · BQP is contained in PSPACE

StructureOptimization problems#✓fully proved

An optimization problem consists of a function \(v\) assigning a rational value \(v(x, s)\) to every instance \(x\) and every candidate solution \(s\), both bitstrings; a feasibility predicate saying whether \(s\) is a feasible solution for \(x\); and a polynomial \(p\) with natural-number coefficients such that every feasible solution \(s\) for \(x\) has length at most \(p(|x|)\). It is required that \(v(x, s) \ge 0\) for all \(x\) and \(s\), that \(v(x, s) = 0\) whenever \(s\) is not feasible for \(x\), and that every instance has a feasible solution.

The problem is read as a maximization problem. The structure carries no computational content: polynomial-time feasibility and a polynomial-time encoding of the objective form a separate predicate (NPO), which the approximation classes APX, PTAS and FPTAS require.

Cslib.Complexity.Classes.OptProblem · 15 lines 
structure OptProblem where
  /-- The objective value of solution `s` for instance `x`. -/
  val : List Bool → List Bool → ℚ
  /-- The feasibility predicate: whether `s` is a feasible solution for `x`. -/
  feas : List Bool → List Bool → Bool
  /-- A polynomial bound on feasible solution lengths. -/
  bound : Polynomial ℕ
  /-- Feasible solutions respect the length bound. -/
  feas_len : ∀ x s, feas x s = true → s.length ≤ bound.eval x.length
  /-- Objective values are nonnegative. -/
  val_nonneg : ∀ x s, 0 ≤ val x s
  /-- The value on infeasible solutions is `0`. -/
  val_infeas : ∀ x s, feas x s = false → val x s = 0
  /-- Every instance has a feasible solution. -/
  feas_nonempty : ∀ x, ∃ s, feas x s = true
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Used by 11
Used byApproximation ratio at a precision · The class APX · The class FPTAS · FPTAS is contained in PTAS · Constant-factor approximable problems · Fully polynomial-time approximation schemes · NPO optimization problems · Polynomial-time approximation schemes · The class PTAS · PTAS is contained in APX · MAX-CUT as an optimization problem

DefinitionApproximation ratio at a precision#✓fully proved

Let \(P\) be a maximization problem with objective value \(\mathrm{val}(x, s)\) for instance \(x\) and solution \(s\), let \(A\) be an algorithm taking a pair of bitstrings, let \(k\) be a natural number and let \(\rho\) be a rational number. Then \(A\) achieves ratio \(\rho\) on \(P\) at precision \(k\) when, for every instance \(x\) and every feasible solution \(s\) of \(x\), the output \(y = A(x, 1^k)\) of \(A\) on \(x\) and the unary string \(1^k\) of \(k\) ones is a feasible solution of \(x\) with \(\rho \cdot \mathrm{val}(x, s) \le \mathrm{val}(x, y)\).

Since every instance has a feasible solution, the output is then always feasible and worth at least \(\rho\) times the value of every feasible solution. The approximation classes share this call convention: a fully polynomial-time approximation scheme is one algorithm achieving ratio \(1 - 1/k\) at every precision \(k \ge 1\), a polynomial-time approximation scheme has such an algorithm for each \(k \ge 1\) separately, and APX asks for some ratio \(\rho\) with \(0 < \rho \le 1\) at precision \(2\).

def ApproxAt (P : OptProblem) (A : List Bool × List Bool → List Bool) (k : ℕ)
    (ρ : ℚ) : Prop :=
  ∀ x s, P.feas x s = true →
    ρ * P.val x s ≤ P.val x (A (x, List.replicate k true)) ∧
    P.feas x (A (x, List.replicate k true)) = true
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Uses 1 · Used by 5
Statement usesOptimization problems
Used byFPTAS is contained in PTAS · Constant-factor approximable problems · Fully polynomial-time approximation schemes · Polynomial-time approximation schemes · PTAS is contained in APX

DefinitionNPO optimization problems#✓fully proved

Let \(P\) be an optimization problem whose instances \(x\) and solutions \(s\) are bitstrings, with rational value \(\mathrm{val}(x, s)\) and feasibility predicate \(\mathrm{feas}(x, s)\). Then \(P\) is an NPO problem when the map \((x, s) \mapsto \mathrm{feas}(x, s)\) is polynomial-time computable, and there is a polynomial-time computable map \(\mathrm{enc}\) sending each pair \((x, s)\) to a triple \((b, a, d)\) of a boolean and two natural numbers such that, for all \(x\) and \(s\): \(d \neq 0\); if \(s\) is feasible for \(x\), then \(\mathrm{val}(x, s) = \sigma a / d\), where \(\sigma = -1\) if \(b\) is true and \(\sigma = 1\) otherwise; and if \(s\) is not feasible for \(x\), then \(\mathrm{val}(x, s) = 0\).

The approximation classes APX, PTAS and FPTAS all require this condition. Without it, a problem could hide an undecidable feasibility relation while assigning value \(0\) everywhere, and the constant empty-solution algorithm would vacuously satisfy the approximation guarantees.

def IsNPO (P : OptProblem) : Prop :=
  IsPolyTime (fun p : List Bool × List Bool => P.feas p.1 p.2) ∧
  ∃ enc : List Bool × List Bool → (Bool × ℕ × ℕ), IsPolyTime enc ∧
    (∀ x s, P.val x s =
      if P.feas x s then
        (if (enc (x, s)).1 then -1 else 1) * ((enc (x, s)).2.1 : ℚ) / (enc (x, s)).2.2
      else 0) ∧
    (∀ x s, (enc (x, s)).2.2 ≠ 0)
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Uses 10 · Used by 5
Statement usesOptimization problems · Bitstring 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 · Polynomial-time computable functions
Used byFPTAS is contained in PTAS · Constant-factor approximable problems · Fully polynomial-time approximation schemes · Polynomial-time approximation schemes · PTAS is contained in APX

DefinitionConstant-factor approximable problems#✓fully proved

A maximization problem \(P\) is in \(\mathsf{APX}\) when \(P\) is an NPO problem and there are a rational number \(\rho\) with \(0 < \rho \le 1\) and a polynomial-time algorithm \(A\) such that, for every instance \(x\) and every feasible solution \(s\) for \(x\), the output \(A(x, 1^2)\) of \(A\) on \(x\) with the unary precision tape of length \(2\) is a feasible solution for \(x\) whose value is at least \(\rho\) times the value of \(s\).

The ratio \(\rho\) is the fraction of the optimum achieved, the reciprocal of the convention \(\rho \ge 1\) in which the value is at least the optimum divided by \(\rho\). The NPO requirement is part of the class: without it, a problem that is not NPO and has value \(0\) everywhere would qualify vacuously.

def IsAPX (P : OptProblem) : Prop :=
  IsNPO P ∧ ∃ ρ : ℚ, 0 < ρ ∧ ρ ≤ 1 ∧ ∃ A : List Bool × List Bool → List Bool,
    IsPolyTime A ∧ ApproxAt P A 2 ρ
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Uses 12 · Used by 1
Statement usesApproximation ratio at a precision · NPO optimization problems · Optimization problems · Bitstring 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 · Polynomial-time computable functions
Used byThe class APX

DefinitionThe class APX#✓fully proved

APX is the set of maximization problems \(P\) that are NP optimization problems (feasibility is decidable in polynomial time, and a polynomial-time computable map sends every instance-solution pair to a signed fraction with nonzero denominator that equals the objective value whenever the solution is feasible) and for which there are a rational number \(\rho\) with \(0 < \rho \le 1\) and a polynomial-time algorithm \(A\) achieving ratio \(\rho\) on \(P\) at precision \(2\): for every instance \(x\) and every feasible solution \(s\) of \(x\), the output \(y\) of \(A\) on \(x\) and the unary precision string \(11\) is a feasible solution of \(x\) whose value is at least \(\rho\) times the value of \(s\).

def APX : Set OptProblem := {P | IsAPX P}
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.
Uses 2 · Used by 1
Statement usesConstant-factor approximable problems · Optimization problems
Used byPTAS is contained in APX

DefinitionPolynomial-time approximation schemes#✓fully proved

An optimization problem \(P\), with value \(\mathrm{val}(x, s)\) of a solution \(s\) for an instance \(x\), admits a polynomial-time approximation scheme when \(P\) is an NPO problem and for every integer \(k \ge 1\) there is a polynomial-time computable algorithm \(A\) on pairs of bitstrings with the following property: for every instance \(x\) and every feasible solution \(s\) for \(x\), the output \(A(x, 1^k)\) on \(x\) and the string \(1^k\) of \(k\) true bits is a feasible solution for \(x\) with \((1 - 1/k)\,\mathrm{val}(x, s) \le \mathrm{val}(x, A(x, 1^k))\). That is, \(A\) achieves approximation ratio \(1 - 1/k\), an error of \(\varepsilon = 1/k\); the algorithm may depend on \(k\).

def IsPTAS (P : OptProblem) : Prop :=
  IsNPO P ∧ ∀ k : ℕ, 1 ≤ k → ∃ A : List Bool × List Bool → List Bool,
    IsPolyTime A ∧ ApproxAt P A k (1 - 1 / (k : ℚ))
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Uses 12 · Used by 2
Statement usesApproximation ratio at a precision · NPO optimization problems · Optimization problems · Bitstring 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 · Polynomial-time computable functions
Used byThe class PTAS · MAX-CUT has no PTAS unless P = NP

DefinitionThe class PTAS#✓fully proved

PTAS is the set of optimization problems \(P\) that are NPO problems (feasibility is decidable in polynomial time and the objective value is given by a polynomial-time computable rational encoding) and that have a polynomial-time approximation scheme: for every natural number \(k \ge 1\) there is a polynomial-time algorithm \(A\) such that, for every instance \(x\) and every feasible solution \(s\) of \(x\), the output of \(A\) on \(x\) and the string of \(k\) ones is a feasible solution of \(x\) whose value is at least \((1 - 1/k)\) times the value of \(s\).

def PTAS : Set OptProblem := {P | IsPTAS P}
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.
Uses 2 · Used by 2
Statement usesPolynomial-time approximation schemes · Optimization problems
Used byFPTAS is contained in PTAS · PTAS is contained in APX

DefinitionFully polynomial-time approximation schemes#✓fully proved

A maximization problem \(P\) has an FPTAS when \(P\) is an NPO problem and there is one polynomial-time algorithm \(A\) such that, for every integer \(k \ge 1\), every instance \(x\) and every feasible solution \(s\) for \(x\), the output \(A(x, 1^k)\) of \(A\) on \(x\) with the unary precision tape of length \(k\) is a feasible solution for \(x\) whose value is at least \(1 - 1/k\) times the value of \(s\).

Since the precision tape is unary, polynomial time in the total input length is polynomial time in \(|x|\) and \(1/\varepsilon\), where \(\varepsilon = 1/k\).

def IsFPTAS (P : OptProblem) : Prop :=
  IsNPO P ∧ ∃ A : List Bool × List Bool → List Bool, IsPolyTime A ∧
    ∀ k : ℕ, 1 ≤ k → ApproxAt P A k (1 - 1 / (k : ℚ))
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440; S. Arora and B. Barak, Computational Complexity: A Modern Approach, 2009, Chapter 11.
Uses 12 · Used by 1
Statement usesApproximation ratio at a precision · NPO optimization problems · Optimization problems · Bitstring 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 · Polynomial-time computable functions
Used byThe class FPTAS

DefinitionThe class FPTAS#✓fully proved

FPTAS is the class of optimization problems that have a fully polynomial-time approximation scheme.

def FPTAS : Set OptProblem := {P | IsFPTAS P}
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.
Uses 2 · Used by 1
Statement usesFully polynomial-time approximation schemes · Optimization problems
Used byFPTAS is contained in PTAS

TheoremFPTAS is contained in PTAS#✓fully proved

Every optimization problem in the class FPTAS of problems with a fully polynomial-time approximation scheme belongs to the class PTAS of problems with a polynomial-time approximation scheme.

The single fully polynomial-time algorithm serves as the algorithm for every precision \(k\).

theorem fptas_subset_ptas : FPTAS ⊆ PTAS
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.
Uses 14
Statement usesThe class FPTAS · Optimization problems · The class PTAS
Proof usesApproximation ratio at a precision · NPO optimization problems · Bitstring 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 · Polynomial-time computable functions

TheoremPTAS is contained in APX#✓fully proved

Every optimization problem in the class PTAS belongs to the class APX.

The algorithm that the approximation scheme provides for error \(1/2\) achieves the constant ratio \(1/2\).

theorem ptas_subset_apx : PTAS ⊆ APX
Sources
  • C. H. Papadimitriou and M. Yannakakis, "Optimization, approximation, and complexity classes", Journal of Computer and System Sciences 43 (1991), 425-440.
Uses 14
Statement usesThe class APX · Optimization problems · The class PTAS
Proof usesApproximation ratio at a precision · NPO optimization problems · Bitstring 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 · Polynomial-time computable functions

DefinitionNegligible functions#✓fully proved

A function \(e : \mathbb{N} \to \mathbb{Q}\) is negligible if for every natural number \(c\) there is a natural number \(N\) such that \(e(n) \le 1 / n^c\) for all natural numbers \(n \ge N\).

def Negligible (e : ℕ → ℚ) : Prop :=
  ∀ c : ℕ, ∃ N : ℕ, ∀ n : ℕ, N ≤ n → e n ≤ 1 / (n : ℚ) ^ c
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2.
Used by 5
Used byOne-way function families · One-way permutation families · One-way permutations are one-way functions · Goldreich-Levin: hardcore predicate from one-way permutations · One-way functions exist

DefinitionInversion success probability#✓fully proved

Let \(f\) be a family of functions, \(f_n\) mapping \(n\)-bit strings to bitstrings, and let \(A\) be an inverter mapping a triple \((n, y, r)\) of a length \(n\), an output \(y\) and a coin string \(r\) to a bitstring. For natural numbers \(n\) and \(m\), the inversion success probability of \(A\) against \(f\) at length \(n\) with \(m\) coins is the fraction of the \(2^{n+m}\) pairs \((x, r)\) of an \(n\)-bit string \(x\) and an \(m\)-bit string \(r\) such that \(f_n(x') = f_n(x)\), where \(x'\) is the \(n\)-bit string whose \(i\)-th bit is the \(i\)-th bit of \(A(n, f_n(x), r)\), or false when that output has no \(i\)-th bit.

The inverter receives the length \(n\) explicitly: when output lengths vary, it could not otherwise recover \(n\) from \(f_n(x)\) alone.

noncomputable def invertSucc (f : (n : ℕ) → (Fin n → Bool) → List Bool)
    (inv : ℕ × List Bool × List Bool → List Bool) (n m : ℕ) : ℚ :=
  (Set.ncard {p : (Fin n → Bool) × (Fin m → Bool) |
    f n (fun i => (inv (n, f n p.1, List.ofFn p.2)).getD i.val false) = f n p.1} : ℚ) /
    (2 : ℚ) ^ (n + m)
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2.
Used by 2
Used byOne-way function families · One-way permutations are one-way functions

DefinitionOne-way function families#✓fully proved

Let \(f\) assign to each \(n \in \mathbb{N}\) and each \(n\)-bit string \(x\) a bitstring \(f_n(x)\). The family \(f\) is one-way when three conditions hold. First, its output lengths are polynomially bounded: some polynomial \(p\) satisfies \(|f_n(x)| \le p(n)\) for all \(n\) and \(x\). Second, it is uniformly computable: some polynomial-time computable function maps the bitstring encoding of the pair \((n, x)\) to \(f_n(x)\) for all \(n\) and \(x\). Third, it is hard to invert: for every polynomial \(q\) with natural-number coefficients and every polynomial-time computable inverter \(A\) on triples \((n, y, r)\) of a natural number and two bitstrings, the inversion success probability of \(A\) against \(f\) at length \(n\) with \(q(n)\) coins is negligible in \(n\), that is, for every \(c \in \mathbb{N}\) it is at most \(1 / n^c\) for all large enough \(n\). Here the inversion success probability is the fraction of pairs \((x, r)\) of an \(n\)-bit string \(x\) and a \(q(n)\)-bit string \(r\) for which the \(n\)-bit string \(x'\) formed by the first \(n\) bits of \(A(n, f_n(x), r)\), with missing bits false, satisfies \(f_n(x') = f_n(x)\).

Deterministic inverters are the special case that ignores the coins. The uniform evaluator is essential: per-length polynomial-size circuits would admit arbitrary noncomputable families.

def IsOneWayFunction (f : (n : ℕ) → (Fin n → Bool) → List Bool) : Prop :=
  (∃ pOut : Polynomial ℕ, ∀ n, ∀ x : Fin n → Bool, (f n x).length ≤ pOut.eval n) ∧
  (∃ evalf : List Bool → List Bool, IsPolyTime evalf ∧
    ∀ n, ∀ x : Fin n → Bool,
      evalf (MetaMathlibExt.BitstringEncoding.bitEncode (n, List.ofFn x)) = f n x) ∧
  ∀ (q : Polynomial ℕ) (inv : ℕ × List Bool × List Bool → List Bool),
    IsPolyTime inv → Negligible (fun n => invertSucc f inv n (q.eval n))
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2; R. Impagliazzo, "A personal view of average-case complexity", Proceedings of the Tenth Annual Structure in Complexities Theory Conference (1995), 134-147.
Uses 11 · Used by 2
Statement usesNegligible functions · Inversion success probability · Bitstring 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 · Polynomial-time computable functions
Used byOne-way permutations are one-way functions · One-way functions imply P ≠ NP

DefinitionInversion success probability against a permutation family#✓fully proved

Let \(\pi\) be a family of maps \(\pi_n\) from \(n\)-bit strings to \(n\)-bit strings, let \(A\) be a function sending a natural number and two bitstrings to a bitstring, and let \(n\) and \(m\) be natural numbers. For a bitstring \(w\), write \(\mathrm{trunc}_n(w)\) for the \(n\)-bit string whose bit at each position \(i < n\) is the entry of \(w\) at position \(i\), or false if \(w\) has at most \(i\) entries. The success probability of \(A\) against \(\pi\) at length \(n\) with \(m\) coins is the rational number \(N / 2^{n+m}\), where \(N\) is the number of pairs \((x, c)\) of an \(n\)-bit string \(x\) and an \(m\)-bit string \(c\) with \(\pi_n(\mathrm{trunc}_n(A(n, \pi_n(x), c))) = \pi_n(x)\), where \(\pi_n(x)\) is passed to \(A\) as a bitstring.

Here \(A\) is a probabilistic inverter that receives the security parameter \(n\), the image \(\pi_n(x)\) and the coins \(c\).

noncomputable def permInvertSucc (π : (n : ℕ) → (Fin n → Bool) → (Fin n → Bool))
    (inv : ℕ × List Bool × List Bool → List Bool) (n m : ℕ) : ℚ :=
  (Set.ncard {p : (Fin n → Bool) × (Fin m → Bool) |
    π n (fun i => (inv (n, List.ofFn (π n p.1), List.ofFn p.2)).getD i.val false) =
      π n p.1} : ℚ) / (2 : ℚ) ^ (n + m)
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2.
Used by 2
Used byOne-way permutation families · One-way permutations are one-way functions

DefinitionOne-way permutation families#✓fully proved

Let \(\pi\) assign to each \(n \in \mathbb{N}\) a map \(\pi_n\) from \(n\)-bit strings to \(n\)-bit strings. The family \(\pi\) is a one-way permutation when three conditions hold. First, each \(\pi_n\) is injective, hence a permutation of the \(n\)-bit strings. Second, it is uniformly computable: some polynomial-time computable function maps the bitstring encoding of the pair \((n, x)\) to \(\pi_n(x)\) for all \(n\) and all \(n\)-bit strings \(x\). Third, it is hard to invert: for every polynomial \(q\) with natural-number coefficients and every polynomial-time computable inverter \(A\) on triples \((n, y, r)\) of a natural number and two bitstrings, the inversion success probability of \(A\) against \(\pi\) at length \(n\) with \(q(n)\) coins is negligible in \(n\), that is, for every \(c \in \mathbb{N}\) it is at most \(1 / n^c\) for all large enough \(n\). Here the inversion success probability is the fraction of pairs \((x, r)\) of an \(n\)-bit string \(x\) and a \(q(n)\)-bit string \(r\) for which the \(n\)-bit string \(x'\) formed by the first \(n\) bits of \(A(n, \pi_n(x), r)\), with missing bits false, satisfies \(\pi_n(x') = \pi_n(x)\).

def IsOneWayPermutation (π : (n : ℕ) → (Fin n → Bool) → (Fin n → Bool)) : Prop :=
  (∀ n, Function.Injective (π n)) ∧
  (∃ evalπ : List Bool → List Bool, IsPolyTime evalπ ∧
    ∀ n, ∀ x : Fin n → Bool,
      evalπ (MetaMathlibExt.BitstringEncoding.bitEncode (n, List.ofFn x)) =
        List.ofFn (π n x)) ∧
  ∀ (q : Polynomial ℕ) (inv : ℕ × List Bool × List Bool → List Bool),
    IsPolyTime inv → Negligible (fun n => permInvertSucc π inv n (q.eval n))
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2.
Uses 11 · Used by 1
Statement usesNegligible functions · Inversion success probability against a permutation family · Bitstring 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 · Polynomial-time computable functions
Used byOne-way permutations are one-way functions

TheoremOne-way permutations are one-way functions#✓fully proved

Let \(\pi\) be a one-way permutation family, so that each \(\pi_n\) maps \(n\)-bit strings to \(n\)-bit strings. Then the family that sends an \(n\)-bit string \(x\) to the bitstring \(\pi_n(x)\) is a one-way function family.

Length preservation gives the polynomial output bound, the evaluator of \(\pi\) serves unchanged, and the inversion success probabilities coincide because an \(n\)-bit string is determined by the list of its bits.

theorem one_way_permutation_implies_one_way_function
    {π : (n : ℕ) → (Fin n → Bool) → (Fin n → Bool)}
    (hπ : IsOneWayPermutation π) :
    IsOneWayFunction (fun n x => List.ofFn (π n x))
Sources
  • O. Goldreich, Foundations of Cryptography, Vol. 1, Cambridge University Press, 2001, Section 2.2.
Uses 14
Statement usesOne-way function families · One-way permutation families
Proof usesNegligible functions · Inversion success probability · Inversion success probability against a permutation family · Bitstring 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 · Polynomial-time computable functions

TheoremPolynomial-time machines have polynomially bounded output#✓fully proved

A polynomial-time machine has polynomially bounded encoded output.

theorem output_length_le {α β A B : Type} {ea : α → List A}
    {eb : β → List B} {f : α → β}
    (h : TM2ComputableInPolyTime ea eb f) (a : α) :
    (eb (f a)).length ≤ (midPoly h).eval (ea a).length
Uses 5 · Used by 2
Statement usesIntermediate length bound of the composite machine
Proof usesStacks of the initial configuration are no longer than the input · Push bound of a finite multi-stack Turing machine · Number of push instructions in a TM2 statement · A halted run stays halted
Used byOutput of a polynomial-time map is polynomial in raw input length · Mapping the first component of a pair is polynomial-time

TheoremPolynomial-time maps run on unframed bit lists#✓fully proved

Canonical polynomial-time maps can also be run on unframed bit lists.

theorem raw_computable {f : List Bool → List Bool} (hf : IsPolyTime f) :
    Nonempty (TM2ComputableInPolyTime
      (fun x : List Bool => x) (fun x : List Bool => x) f)
Uses 12 · Used by 2
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 · Polynomial-time computable functions
Proof usesPolynomial-time decoder of the canonical bit-list encoding · Polynomial-time encoder to the canonical bit-list encoding · Polynomial-time TM2-computable functions are closed under composition
Used byOutput of a polynomial-time map is polynomial in raw input length · Mapping the first component of a pair is polynomial-time

TheoremMapping the first component of a pair is polynomial-time#✓fully proved

Mapping the first component of an encoded pair is polynomial-time; the second component is preserved, not recomputed or guessed.

theorem IsPolyTime.map_fst {f : List Bool → List Bool}
    (hf : IsPolyTime f) :
    IsPolyTime (fun p : List Bool × List Bool => (f p.1, p.2))
Uses 38 · Used by 1
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 · Polynomial-time computable functions
Proof usesPolynomial-time conversion to the verifier's pair encoding · Canonical bit-list decoder · Work alphabet of the dense-SAT verifier · Pair encoding \(w \# y\) · Polynomial-time machines have polynomially bounded output · Polynomial-time maps run on unframed bit lists · Stack indices of the composite machine · Stack alphabets of the composite machine · Labels of the composite machine · States of the composite machine · Intermediate alphabet of the composite machine · First copy loop of the composite machine · Second copy loop of the composite machine · Evaluation of a natural-number polynomial is monotone · Simulation transports runs · Composite label of an \(M_1\) label · Lifting a statement of the first machine · Intermediate length bound of the composite machine · Assembling the stacks of the composite machine · Pop label of the first copy loop · Pop label of the second copy loop · The program of the composite machine · Scratch stack of the composite machine · Stack embedding · Translating a statement along a stack embedding · Exact run transport to supplied host final stacks · Exact-length runs of a TM2 machine · A single step executes the statement at the current label · Polynomial-time TM2-computable functions are closed under composition
Used byPreimage of SAT under a polynomial-time map is in NP

TheoremOutput of a polynomial-time map is polynomial in raw input length#✓fully proved

Encoded output length is polynomial in the unframed input length.

theorem IsPolyTime.length_bound {f : List Bool → List Bool}
    (hf : IsPolyTime f) :
    ∃ q : Polynomial ℕ, ∀ x, (f x).length ≤ q.eval x.length
Uses 12 · Used by 1
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 · Polynomial-time computable functions
Proof usesPolynomial-time machines have polynomially bounded output · Polynomial-time maps run on unframed bit lists · Intermediate length bound of the composite machine
Used byPreimage of SAT under a polynomial-time map is in NP

TheoremPreimage of SAT under a polynomial-time map is in NP#✓fully proved

Pulling SAT back along a polynomial map preserves NP membership. SAT verifier soundness holds even for certificates above its length bound.

theorem satDec_comp_mem_NP {f : List Bool → List Bool}
    (hf : IsPolyTime f) : satDec ∘ f ∈ NP
Uses 33 · Used by 1
Statement usesSAT as a decision problem · Bitstring 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 · The complexity class NP
Proof usesSAT accepts the code of a formula exactly when it is satisfiable · The SAT verifier is polynomial-time · Formula check against a witness · Correctness of the witness formula check · Decoding a complete length-prefixed CNF formula · The CNF decoder inverts the length-prefixed CNF code · Length-prefixed binary code of a CNF formula · Witness lookup · The SAT verifier · The SAT verifier rejects undecodable inputs · The SAT verifier on a decodable input · The SAT verifier verifies SAT · Occurrence list of a CNF formula · CNF formula · Satisfaction of a CNF formula · Satisfiability of a CNF formula · Satisfiability means having a satisfying assignment · Polynomial-time functions are closed under composition · Output of a polynomial-time map is polynomial in raw input length · Mapping the first component of a pair is polynomial-time
Used byNP is closed under polynomial-time preimages

TheoremNP is closed under polynomial-time preimages#✓fully proved

Canonical NP is closed under polynomial-time preimages. Cook–Levin supplies a verifier sound for arbitrarily long certificates, so enlarging the transformed witness bound introduces no false positives.

theorem comp_mem_NP {L : DecisionProblem} {f : List Bool → List Bool}
    (hL : L ∈ NP) (hf : IsPolyTime f) : L ∘ f ∈ NP
Uses 17 · Used by 2
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 · The complexity class NP
Proof usesCook–Levin theorem · Polynomial-time many-one reduction · SAT as a decision problem · Polynomial-time functions are closed under composition · Preimage of SAT under a polynomial-time map is in NP
Used bycoNP is closed under polynomial-time preimages · NP membership pulls back along polynomial many-one reductions

TheoremNP membership pulls back along polynomial many-one reductions#✓fully proved

NP membership transfers backwards along a polynomial many-one reduction.

theorem mem_NP_of_polyManyOneRed {L K : DecisionProblem}
    (hK : K ∈ NP) (hr : PolyManyOneRed L K) : L ∈ NP
Uses 14 · Used by 1
Statement usesPolynomial-time many-one reduction · Complexity classes · Decision problems · The complexity class NP
Proof 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 · Polynomial-time computable functions · NP is closed under polynomial-time preimages
Used byBinary-coded PARTITION is in NP

TheoremcoNP is closed under polynomial-time preimages#✓fully proved

Canonical coNP is closed under polynomial-time preimages.

theorem comp_mem_coNP {L : DecisionProblem} {f : List Bool → List Bool}
    (hL : L ∈ coNP) (hf : IsPolyTime f) : L ∘ f ∈ coNP
Uses 13
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 · The class coNP
Proof usesNP is closed under polynomial-time preimages

TheoremPolynomial many-one reductions also reduce complements#✓fully proved

The same reduction function reduces the complements.

theorem PolyManyOneRed.compl
    {L K : MetaMathlibExt.ComplexityTheory.DecisionProblem}
    (h : PolyManyOneRed L K) : PolyManyOneRed Lᶜ Kᶜ
Uses 11
Statement usesPolynomial-time many-one reduction · Decision problems
Proof 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 · Polynomial-time computable functions
117 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.