Blum complexity measures

StructureBlum complexity measure#✓fully proved

A Blum measure \(\Phi\) assigns to every program \(c\) and input \(n \in \mathbb{N}\) a partially defined cost \(\Phi_c(n) \in \mathbb{N}\) satisfying Blum's two axioms: \(\Phi_c(n)\) is defined exactly when program \(c\) halts on input \(n\), and the relation \(\Phi_c(n) = m\) between \(c\), \(n\) and \(m\) is decidable.

structure BlumMeasure where
  /-- The cost of running program `c` on input `n`: defined exactly when the program halts. -/
  cost : Nat.Partrec.Code → ℕ →. ℕ
  /-- **Blum's first axiom**: the cost is defined exactly when the program halts. -/
  domain_axiom : ∀ (c : Nat.Partrec.Code) (n : ℕ), (cost c n).Dom ↔ (c.eval n).Dom
  /-- **Blum's second axiom**: the graph of the cost function is decidable. -/
  graph_decidable : ComputablePred (fun w : ℕ ↦
    cost (Denumerable.ofNat Nat.Partrec.Code w.unpair.1)
      w.unpair.2.unpair.1 = Part.some w.unpair.2.unpair.2)

Sources

• Blum, "A machine-independent theory of the complexity of recursive functions", Journal of the ACM 14 (1967), 322–336, Definition 1.

Used by 3

Used byBlum complexity class · Blum classes via an explicit threshold · Blum classes are monotone in the bound

DefinitionBlum complexity class#✓fully proved

Given a Blum measure \(\Phi\) and a function \(t\) from \(\mathbb{N}\) to \(\mathbb{N}\), the Blum class of \(t\) consists of the partial functions \(f\) from \(\mathbb{N}\) to \(\mathbb{N}\) that are computed by some program \(c\) whose cost \(\Phi_c(n)\) is defined and at most \(t(n)\) for all but finitely many inputs \(n\).

The bound is not required at every input: Blum's classes are defined up to finite exceptions, and the finite exceptions are essential to the gap and union theorems (a program may be slow on finitely many inputs without leaving the class).

def BlumClass (Φ : BlumMeasure) (t : ℕ → ℕ) (f : ℕ →. ℕ) : Prop :=
  ∃ c : Nat.Partrec.Code, c.eval = f ∧
    ∀ᶠ n in Filter.atTop, ∃ m, m ≤ t n ∧ Φ.cost c n = Part.some m

Sources

• Blum, "A machine-independent theory of the complexity of recursive functions", Journal of the ACM 14 (1967), 322–336, Definition 2.

Uses 1 · Used by 2

Statement usesBlum complexity measure

Used byBlum classes via an explicit threshold · Blum classes are monotone in the bound

TheoremBlum classes are monotone in the bound#✓fully proved

If t is eventually dominated by t', every function in the t-class is in the t'-class.

theorem BlumClass.mono {Φ : BlumMeasure} {t t' : ℕ → ℕ} {f : ℕ →. ℕ}
    (h : ∀ᶠ n in Filter.atTop, t n ≤ t' n) (hf : BlumClass Φ t f) :
    BlumClass Φ t' f

Sources

• Blum, "A machine-independent theory of the complexity of recursive functions", Journal of the ACM 14 (1967), 322–336, Definition 2.

Uses 2

Statement usesBlum complexity class · Blum complexity measure

TheoremBlum classes via an explicit threshold#✓fully proved

Let \(\Phi\) be a Blum measure, \(t\) a function from \(\mathbb{N}\) to \(\mathbb{N}\) and \(f\) a partial function from \(\mathbb{N}\) to \(\mathbb{N}\). Then \(f\) lies in the Blum class of \(t\) with respect to \(\Phi\) if and only if there are a program \(c\) that computes \(f\) and a threshold \(N\) such that for every input \(n \ge N\) the cost \(\Phi_c(n)\) is defined and at most \(t(n)\).

theorem blumClass_iff (Φ : BlumMeasure) (t : ℕ → ℕ) (f : ℕ →. ℕ) :
    BlumClass Φ t f ↔
      ∃ c : Nat.Partrec.Code, c.eval = f ∧
        ∃ N, ∀ n, N ≤ n → ∃ m, m ≤ t n ∧ Φ.cost c n = Part.some m

Sources

• Blum, "A machine-independent theory of the complexity of recursive functions", Journal of the ACM 14 (1967), 322–336, Definition 2.

Uses 2

Statement usesBlum complexity class · Blum complexity measure

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.