Documentation

Complexity.Computability.Kolmogorov.Depth

Computational depth #

The computational depth of an object x at time t is C_M^t(x) - C_M(x): how much longer the shortest descriptions of x become when they must run within t steps. This is the basic computational depth of Antunes, Fortnow, van Melkebeek and Vinodchandran, Section 3, there defined with prefix-free complexity, here with the plain complexity of any description method. It is computed in ℕ∞ with truncated subtraction, and since C_M(x) ≤ C_M^t(x), depth plus plain complexity is exactly the time-bounded complexity. The depth between two time bounds t₁ ≤ t₂ is C_M^{t₁}(x) - C_M^{t₂}(x), and depths between consecutive time bounds add up.

Main definitions #

Main results #

References #

source
noncomputable def Cslib.Kolmogorov.DescriptionMethod.depth {α : Type u_1} (M : DescriptionMethod α) (t : ℕ) (x : α) :
ℕ∞

The computational depth C_M^t(x) - C_M(x) of x at time t.

Instances For
    source
    noncomputable def Cslib.Kolmogorov.DescriptionMethod.depthBetween {α : Type u_1} (M : DescriptionMethod α) (t₁ t₂ : ℕ) (x : α) :
    ℕ∞

    The depth C_M^{t₁}(x) - C_M^{t₂}(x) of x between the time bounds t₁ and t₂.

    Instances For
      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depth_add_ecomplexity {α : Type u_1} (M : DescriptionMethod α) (t : ℕ) (x : α) :
      M.depth t x + M.ecomplexity x = M.etimeBoundedComplexity t x

      Depth plus plain complexity is exactly the time-bounded complexity.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depth_le_etimeBoundedComplexity {α : Type u_1} (M : DescriptionMethod α) (t : ℕ) (x : α) :
      M.depth t x ≤ M.etimeBoundedComplexity t x
      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depth_antitone {α : Type u_1} (M : DescriptionMethod α) (x : α) :
      Antitone fun (x_1 : ℕ) => M.depth x_1 x

      Monotonicity in the time bound. More time cannot increase the depth.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depth_eq_zero_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} :
      M.depth t x = 0 ↔ M.etimeBoundedComplexity t x = M.ecomplexity x

      The depth vanishes exactly when the time bound attains the plain complexity.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depth_eq_top_iff {α : Type u_1} {M : DescriptionMethod α} {t : ℕ} {x : α} :
      M.depth t x = ⊤ ↔ M.etimeBoundedComplexity t x = ⊤ ∧ M.ecomplexity x ≠ ⊤

      The depth is infinite exactly when x has a description but none within the time bound.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.exists_forall_le_depth_eq_zero {α : Type u_1} (M : DescriptionMethod α) (x : α) :
      ∃ (t : ℕ), ∀ t' ≥ t, M.depth t' x = 0

      Every object has depth zero from some time bound on.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depthBetween_eq_depth {α : Type u_1} {M : DescriptionMethod α} {t₁ t₂ : ℕ} {x : α} (h : M.etimeBoundedComplexity t₂ x = M.ecomplexity x) :
      M.depthBetween t₁ t₂ x = M.depth t₁ x

      The depth between t and a time bound attaining the plain complexity is the depth at t.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depthBetween_add_etimeBoundedComplexity {α : Type u_1} {M : DescriptionMethod α} {t₁ t₂ : ℕ} {x : α} (h : t₁ ≤ t₂) :
      M.depthBetween t₁ t₂ x + M.etimeBoundedComplexity t₂ x = M.etimeBoundedComplexity t₁ x

      Depth between two time bounds plus the complexity at the later one is the complexity at the earlier one.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depthBetween_add {α : Type u_1} {M : DescriptionMethod α} {t₁ t₂ t₃ : ℕ} {x : α} (h₁₂ : t₁ ≤ t₂) (h₂₃ : t₂ ≤ t₃) :
      M.depthBetween t₁ t₂ x + M.depthBetween t₂ t₃ x = M.depthBetween t₁ t₃ x

      Depths between consecutive time bounds add up.

      source
      theorem Cslib.Kolmogorov.DescriptionMethod.depthBetween_add_depth {α : Type u_1} {M : DescriptionMethod α} {t₁ t₂ : ℕ} {x : α} (h : t₁ ≤ t₂) :
      M.depthBetween t₁ t₂ x + M.depth t₂ x = M.depth t₁ x

      The depth at t₁ is the depth between t₁ and t₂ plus the depth at t₂.