Polynomial time in a cost-annotated programming model

DefinitionDeclared polynomial time for timed deciders#✓fully proved

Let \(f\) be a timed function that maps each list \(x\) of Booleans to a Boolean \(f(x)\) together with a declared time \(t_f(x) \in \mathbb{N}\). Then \(f\) decides in declared polynomial time when there is a polynomial \(p\) with natural-number coefficients such that \(t_f(x) \le p(|x|)\) for every list \(x\) of Booleans, where \(|x|\) is the length of \(x\).

This constrains only the trusted time annotation: it implies neither that \(f\) is computable in any machine model nor that \(f\) is related to any particular decision problem.

def DecidesInDeclaredPolyTime (f : List Bool → TimeM Nat Bool) : Prop :=
  ∃ p : Polynomial ℕ, ∀ x, (f x).time ≤ p.eval x.length

Used by 3

Used byDeclared polynomial time is preserved under precomposition with a reduction · Every decision problem has a timed decider in declared polynomial time · A decider with polynomial declared time gives a verifier with polynomial declared time

DefinitionDeclared polynomial time for timed functions on bitstrings#✓fully proved

Let \(f\) be a timed function that maps each list \(x\) of Booleans to an output list \(f(x)\) of Booleans together with a declared time \(t_f(x) \in \mathbb{N}\). Then \(f\) computes in declared polynomial time when there is a polynomial \(p\) with natural-number coefficients such that, for every list \(x\) of Booleans, both \(t_f(x)\) and the length of \(f(x)\) are at most \(p(|x|)\), where \(|x|\) is the length of \(x\).

Declared times are trusted annotations, not checked against any machine model, so this does not make \(f\) polynomial-time computable: for an arbitrary decision problem \(L\), the function returning the one-element list \([L(x)]\) with declared time \(0\) satisfies it. The output-length bound is what lets declared bounds compose.

def ComputesInDeclaredPolyTime (f : List Bool → TimeM Nat (List Bool)) : Prop :=
  ∃ p : Polynomial ℕ, ∀ x, (f x).time ≤ p.eval x.length ∧
    (f x).ret.length ≤ p.eval x.length

Used by 7

Used byFrom declared-time to polynomial-time many-one reductions · A declared-time reduction followed by a decider for the target decides the source · Declared polynomial time is preserved under precomposition with a reduction · Declared-time many-one reduction by a timed function · Declared-time many-one reduction is reflexive · Declared-time many-one reductions compose · Pulling a verifier back along a declared reduction

DefinitionVerifiers with polynomial declared time#✓fully proved

A timed verifier \(V\), which assigns to each pair of bit strings \((x, w)\) (an input and a witness) a timed computation returning a Boolean, runs in declared polynomial time when there is a polynomial \(q\) with natural coefficients such that the declared time of \(V(x, w)\) is at most \(q(|x| + |w|)\) for all \(x\) and \(w\).

As for deciders, this constrains only the declared time, which is a trusted annotation, and establishes no computability in any machine model.

def VerifierInDeclaredPolyTime (V : List Bool × List Bool → TimeM Nat Bool) : Prop :=
  ∃ q : Polynomial ℕ, ∀ xw, (V xw).time ≤ q.eval (xw.1.length + xw.2.length)

Used by 3

Used byA decider with polynomial declared time gives a verifier with polynomial declared time · Pulling a verifier back along a declared reduction · The SAT verifier has polynomial declared time

DefinitionVerifying a decision problem with a witness bound#✓fully proved

A timed verifier \(V\), which assigns to each pair of bit strings \((x, w)\) (an input and a witness) a timed computation returning a Boolean, verifies a decision problem \(L\) with witness bound \(p\), a polynomial with natural coefficients, when for every bit string \(x\), \(L(x)\) holds if and only if there is a witness \(w\) with \(|w| \le p(|x|)\) such that \(V(x, w)\) returns true.

This is the verifier half of the definition of NP, phrased for a named timed verifier.

def Verifies (V : List Bool × List Bool → TimeM Nat Bool)
    (L : DecisionProblem) (p : Polynomial ℕ) : Prop :=
  ∀ x, L x ↔ ∃ w : List Bool, w.length ≤ p.eval x.length ∧
    (V (x, w)).ret = true

Uses 1 · Used by 4

Statement usesDecision problems

Used byA timed verifier with polynomial-time output function puts its language in NP · Pulling a verifier back along a declared reduction · A decider is a verifier with witness bound zero · The SAT verifier verifies SAT

DefinitionDeclared-time many-one reduction by a timed function#✓fully proved

Let \(L_1\) and \(L_2\) be decision problems and let \(f\) be a timed function that maps each list \(x\) of Booleans to a list \(f(x)\) of Booleans together with a declared time. Then \(f\) is a declared-time many-one reduction from \(L_1\) to \(L_2\) when \(f\) computes in declared polynomial time and \(L_1(x) = L_2(f(x))\) for every list \(x\) of Booleans.

Because declared times are trusted annotations, this is not a polynomial-time many-one reduction in the Turing-machine sense: nothing is established about the computability of \(f\).

def DeclaredPolyManyOneRedVia (f : List Bool → TimeM Nat (List Bool))
    (L₁ L₂ : DecisionProblem) : Prop :=
  ComputesInDeclaredPolyTime f ∧ ∀ x, L₁ x = L₂ (f x).ret

Uses 2 · Used by 6

Statement usesDeclared polynomial time for timed functions on bitstrings · Decision problems

Used byFrom declared-time to polynomial-time many-one reductions · A declared-time reduction followed by a decider for the target decides the source · Declared polynomial time is preserved under precomposition with a reduction · Declared-time many-one reduction is reflexive · Declared-time many-one reductions compose · Pulling a verifier back along a declared reduction

TheoremEvery decision problem has a timed decider in declared polynomial time#✓fully proved

For every decision problem \(L\) there is a timed function \(f\) from lists of Booleans to Booleans that decides in declared polynomial time and whose output \(f(x)\) equals \(L(x)\) for every list \(x\) of Booleans.

The witness returns \(L(x)\) with declared time \(0\), treating the evaluation of \(L\) as free. This is why no complexity classes are defined by quantifying over timed functions.

theorem exists_decidesInDeclaredPolyTime (L : DecisionProblem) :
    ∃ f : List Bool → TimeM Nat Bool, DecidesInDeclaredPolyTime f ∧
      ∀ x, (f x).ret = L x

Uses 2

Statement usesDeclared polynomial time for timed deciders · Decision problems

TheoremA decider with polynomial declared time gives a verifier with polynomial declared time#✓fully proved

If a timed decider \(f\) on bit strings has declared time bounded by a polynomial in the input length, then the verifier that sends an input \(x\) and a witness \(w\) to \(f(x)\), ignoring \(w\), has declared time bounded by a polynomial in \(|x| + |w|\).

theorem verifierInDeclaredPolyTime_of_decidesInDeclaredPolyTime
    {f : List Bool → TimeM Nat Bool} (hf : DecidesInDeclaredPolyTime f) :
    VerifierInDeclaredPolyTime (fun xw => f xw.1)

Uses 2

Statement usesDeclared polynomial time for timed deciders · Verifiers with polynomial declared time

TheoremA decider is a verifier with witness bound zero#✓fully proved

Let \(L\) be a decision problem and let \(f\) be a timed decider whose return value on every bit string \(x\) equals \(L(x)\). Then the verifier that sends an input \(x\) and a witness \(w\) to \(f(x)\), ignoring \(w\), verifies \(L\) with the zero polynomial as witness bound, so only the empty witness is allowed.

Together with the fact that this verifier has polynomial declared time whenever \(f\) does, this is the declared-time form of \(\mathrm{P} \subseteq \mathrm{NP}\) for named algorithms.

theorem verifies_of_decides {f : List Bool → TimeM Nat Bool}
    {L : DecisionProblem} (hdec : ∀ x, (f x).ret = L x) :
    Verifies (fun xw => f xw.1) L 0

Uses 2

Statement usesVerifying a decision problem with a witness bound · Decision problems

TheoremDeclared-time many-one reduction is reflexive#✓fully proved

For every decision problem \(L\), the timed identity function, which returns its input with declared time \(0\), is a declared-time many-one reduction from \(L\) to \(L\).

theorem declaredPolyManyOneRedVia_refl (L : DecisionProblem) :
    DeclaredPolyManyOneRedVia (fun x => pure x) L L

Uses 3

Statement usesDeclared-time many-one reduction by a timed function · Decision problems

Proof usesDeclared polynomial time for timed functions on bitstrings

TheoremDeclared-time many-one reductions compose#✓fully proved

Let \(L_1\), \(L_2\) and \(L_3\) be decision problems. If \(f_1\) is a declared-time many-one reduction from \(L_1\) to \(L_2\) and \(f_2\) is a declared-time many-one reduction from \(L_2\) to \(L_3\), then the timed function that on input \(x\) returns \(f_2(f_1(x))\), with declared time the declared time of \(f_1\) on \(x\) plus that of \(f_2\) on \(f_1(x)\), is a declared-time many-one reduction from \(L_1\) to \(L_3\).

If \(p_1\) and \(p_2\) bound the declared times and output lengths of \(f_1\) and \(f_2\), then \(p_1 + p_2 \circ p_1\) bounds those of the composite.

theorem declaredPolyManyOneRedVia_trans
    {f₁ f₂ : List Bool → TimeM Nat (List Bool)} {L₁ L₂ L₃ : DecisionProblem}
    (h₁₂ : DeclaredPolyManyOneRedVia f₁ L₁ L₂) (h₂₃ : DeclaredPolyManyOneRedVia f₂ L₂ L₃) :
    DeclaredPolyManyOneRedVia (fun x => f₁ x >>= f₂) L₁ L₃

Uses 3

Statement usesDeclared-time many-one reduction by a timed function · Decision problems

Proof usesDeclared polynomial time for timed functions on bitstrings

TheoremDeclared polynomial time is preserved under precomposition with a reduction#✓fully proved

Let \(L_1\) and \(L_2\) be decision problems, let \(f\) be a declared-time many-one reduction from \(L_1\) to \(L_2\), and let \(g\) be a timed function from lists of Booleans to Booleans that decides in declared polynomial time. Then the timed function that on input \(x\) returns \(g(f(x))\), with declared time the declared time of \(f\) on \(x\) plus that of \(g\) on \(f(x)\), decides in declared polynomial time.

If \(p_f\) bounds the declared time and output length of \(f\) and \(p_g\) bounds the declared time of \(g\), then \(p_f + p_g \circ p_f\) bounds the declared time of the composite.

theorem decidesInDeclaredPolyTime_comp_reduction
    {f : List Bool → TimeM Nat (List Bool)} {g : List Bool → TimeM Nat Bool}
    {L₁ L₂ : DecisionProblem} (hred : DeclaredPolyManyOneRedVia f L₁ L₂)
    (hg : DecidesInDeclaredPolyTime g) :
    DecidesInDeclaredPolyTime (fun x => f x >>= g)

Uses 4

Statement usesDeclared polynomial time for timed deciders · Declared-time many-one reduction by a timed function · Decision problems

Proof usesDeclared polynomial time for timed functions on bitstrings

TheoremA declared-time reduction followed by a decider for the target decides the source#✓fully proved

Let \(L_1\) and \(L_2\) be decision problems, let \(f\) be a declared-time many-one reduction from \(L_1\) to \(L_2\), and let \(g\) be a timed function from lists of Booleans to Booleans whose output on every list \(y\) is \(L_2(y)\). Then for every list \(x\) of Booleans, the timed function that runs \(f\) on \(x\) and then \(g\) on its output returns \(L_1(x)\).

Together with the preservation of declared polynomial time under such compositions, this is the declared-time form of closure under reductions; no membership in the class P is claimed.

theorem decides_comp_reduction
    {f : List Bool → TimeM Nat (List Bool)} {g : List Bool → TimeM Nat Bool}
    {L₁ L₂ : DecisionProblem} (hred : DeclaredPolyManyOneRedVia f L₁ L₂)
    (hdec : ∀ x, (g x).ret = L₂ x) (x : List Bool) :
    ((fun x => f x >>= g) x).ret = L₁ x

Uses 3

Statement usesDeclared-time many-one reduction by a timed function · Decision problems

Proof usesDeclared polynomial time for timed functions on bitstrings

TheoremPulling a verifier back along a declared reduction#✓fully proved

Let \(L_1\) and \(L_2\) be decision problems, let \(f\) be a declared polynomial-time many-one reduction from \(L_1\) to \(L_2\), and let \(V\) be a verifier with polynomial declared time that verifies \(L_2\) with witness bound \(p\). Let \(V'\) be the verifier that on input \(x\) and witness \(w\) first runs \(f\) on \(x\), obtaining \(y\), then runs \(V\) on \((y, w)\) and accepts when \(V\) accepts and \(|w| \le p(|y|)\); its declared time is the declared time of \(f(x)\) plus that of \(V(y, w)\). Then \(V'\) has polynomial declared time, and there is a polynomial \(p'\) with natural coefficients such that \(V'\) verifies \(L_1\) with witness bound \(p'\).

The proof takes \(p' = p \circ r\) and the time bound \(r(n) + q(r(n) + n)\) with \(n = |x| + |w|\), where \(r\) bounds the declared time and output length of \(f\) and \(q\) bounds the declared time of \(V\).

theorem verifies_comp_reduction
    {f : List Bool → TimeM Nat (List Bool)}
    {V : List Bool × List Bool → TimeM Nat Bool}
    {L₁ L₂ : DecisionProblem} {p : Polynomial ℕ}
    (hred : DeclaredPolyManyOneRedVia f L₁ L₂) (hVt : VerifierInDeclaredPolyTime V)
    (hV : Verifies V L₂ p) :
    ∃ p' : Polynomial ℕ,
      VerifierInDeclaredPolyTime (fun xw => f xw.1 >>= fun y =>
        (fun b => b && decide (xw.2.length ≤ p.eval y.length)) <$>
          V (y, xw.2)) ∧
      Verifies (fun xw => f xw.1 >>= fun y =>
        (fun b => b && decide (xw.2.length ≤ p.eval y.length)) <$>
          V (y, xw.2)) L₁ p'

Uses 5

Statement usesDeclared-time many-one reduction by a timed function · Verifiers with polynomial declared time · Verifying a decision problem with a witness bound · Decision problems

Proof usesDeclared polynomial time for timed functions on bitstrings

TheoremA timed decider with polynomial-time output function gives membership in P#✓fully proved

Let \(L\) be a decision problem and let \(f\) assign to each bit string \(x\) a timed computation, that is, a Boolean return value together with a declared time in \(\mathbb{N}\), whose return value equals \(L(x)\) for every \(x\). If the function sending \(x\) to the return value of \(f(x)\) is polynomial-time computable, then \(L\) belongs to the class P.

The polynomial-time hypothesis must be proved for the specific decider: it does not follow from a polynomial bound on the declared times, which are trusted annotations, since every decision problem has a decider of declared time zero.

theorem mem_P_of_decides {f : List Bool → TimeM Nat Bool}
    {L : DecisionProblem} (hdec : ∀ x, (f x).ret = L x)
    (h : MetaMathlibExt.ComplexityTheory.IsPolyTime fun x => (f x).ret) :
    L ∈ MetaMathlibExt.ComplexityTheory.P

Uses 12

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 P

TheoremA timed verifier with polynomial-time output function puts its language in NP#✓fully proved

Let \(L\) be a decision problem, \(p\) a polynomial with natural-number coefficients, and \(V\) a timed function from pairs of lists of Booleans to Booleans that verifies \(L\) with witness bound \(p\). If the function sending \((x, w)\) to the output of \(V\) on \((x, w)\) is polynomial-time computable by a Turing machine for the canonical bitstring encodings, then \(L\) is in NP.

The polynomial-time hypothesis must be proved separately for \(V\); it does not follow from any bound on the declared time of \(V\).

theorem mem_NP_of_verifies {V : List Bool × List Bool → TimeM Nat Bool}
    {L : DecisionProblem} {p : Polynomial ℕ} (hver : Verifies V L p)
    (h : MetaMathlibExt.ComplexityTheory.IsPolyTime fun xw => (V xw).ret) :
    L ∈ MetaMathlibExt.ComplexityTheory.NP

Uses 13 · Used by 1

Statement usesVerifying a decision problem with a witness bound · 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

Used bySAT is in NP if its verifier is polynomial-time

TheoremFrom declared-time to polynomial-time many-one reductions#✓fully proved

Let \(L_1\) and \(L_2\) be decision problems and let \(f\) be a declared-time many-one reduction from \(L_1\) to \(L_2\). If the function sending \(x\) to the output of \(f\) on \(x\) is polynomial-time computable by a Turing machine for the canonical bitstring encodings, then \(L_1\) reduces to \(L_2\) by a polynomial-time many-one reduction.

The polynomial-time hypothesis must be proved separately for \(f\); it does not follow from the declared-time bound.

theorem cookLevinPolyManyOneRed_of_declared
    {f : List Bool → TimeM Nat (List Bool)} {L₁ L₂ : DecisionProblem}
    (hred : DeclaredPolyManyOneRedVia f L₁ L₂)
    (h : MetaMathlibExt.ComplexityTheory.IsPolyTime fun x => (f x).ret) :
    Cslib.CookLevin.PolyManyOneRed L₁ L₂

Uses 13

Statement usesPolynomial-time many-one reduction · Declared-time many-one reduction by a timed function · 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 · Decision problems · Polynomial-time computable functions

Proof usesDeclared polynomial time for timed functions on bitstrings

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.