The Conditional Time-Bounded Kolmogorov Complexity Problem (MINcKT)

This module defines the conditional time-bounded Kolmogorov complexity decision problem Cslib.Kolmogorov.MINcKT (the conditional analogue of MINKT from Hirahara, Definition 9), its fixed-parameter counterpart Cslib.Kolmogorov.MINcKTAt, and the conditional promise problem Cslib.Kolmogorov.GapMINcKT (the conditional analogue of GapMINKT from Hirahara, Definition 11), and proves that MINcKT lies in NP (and that MINcKTAt t s lies in NP whenever t and s are computable in polynomial time in unary).

The underlying conditional reference machine condUniversalTM and conditional complexity measures condPlain, condTimeBounded, condTimeBoundedAt, and condLevinKt are developed in Complexity.Computability.Kolmogorov.Conditional.

Threshold conventions

As with MINKT and MINKTAt, both threshold conventions are provided and bridged:

• Thresholds in the instance (Cslib.Kolmogorov.MINcKT): An instance i : MINcKT.Instance consists of a target binary string i.string, an auxiliary condition string i.cond, a step bound i.time, and a program size threshold i.size, encoded by MINcKT.enc with i.time and i.size in unary (following Ko and the conditional analogue of Hirahara, Definition 9). The instance belongs to MINcKT when condTimeBoundedAt i.time i.string i.cond ≤ i.size.
• Fixed-function thresholds (Cslib.Kolmogorov.MINcKTAt t s): For time and size threshold functions t s : ℕ → ℕ, MINcKTAt t s : Set (List Bool × List Bool) is the language of string pairs (x, y) with condTimeBounded t x y ≤ s x.length. The bridge mem_MINcKTAt_iff_mem_MINcKT identifies (x, y) ∈ MINcKTAt t s with ⟨x, y, t x.length, s x.length⟩ ∈ MINcKT, and MINcKTAt.polyTimeReducible_MINcKT reduces MINcKTAt t s to MINcKT whenever t and s are computable in polynomial time in unary.

Main definitions

• Cslib.Kolmogorov.MINcKT.Instance, Cslib.Kolmogorov.MINcKT, Cslib.Kolmogorov.MINcKT.enc: instances, yes-instances, and unary-threshold encoding of MINcKT.
• Cslib.Kolmogorov.MINcKT.check: polynomial-time witness verifier for MINcKT.
• Cslib.Kolmogorov.MINcKTAt, Cslib.Kolmogorov.MINcKTAt.toInstance: fixed-threshold language {(x, y) | condTimeBounded t x y ≤ s x.length} and its canonical embedding into MINcKT.Instance.
• Cslib.Kolmogorov.GapMINcKT, Cslib.Kolmogorov.GapMINcKT.yesSet, Cslib.Kolmogorov.GapMINcKT.noSet: the conditional promise problem GapMINcKT[σ, τ] (conditional analogue of Hirahara, Definition 11, parameterized here by gap functions σ, τ : ℕ → ℕ → ℕ → ℕ of |x|, |y|, and the threshold).

Main results

• Cslib.Kolmogorov.MINcKT.Instance.computableInPolyTime_mk, Cslib.Kolmogorov.MINcKT.computableInPolyTime_check: polynomial-time certificates for the MINcKT constructor and witness verifier.
• Cslib.Kolmogorov.MINcKT.mem_NP: MINcKT ∈ NP MINcKT.enc.
• Cslib.Kolmogorov.mem_MINcKTAt_iff_mem_MINcKT, Cslib.Kolmogorov.MINcKTAt.computableInPolyTime_toInstance, Cslib.Kolmogorov.MINcKTAt.polyTimeReducible_MINcKT: equivalence and polynomial-time reduction between MINcKTAt t s and MINcKT.
• Cslib.Kolmogorov.MINcKTAt.mem_NP, Cslib.Kolmogorov.MINcKTAt.mem_NP_polynomial₂: MINcKTAt t s ∈ NP (encPair encBits encBits) for polynomial-time unary threshold functions.
• Cslib.Kolmogorov.GapMINcKT.disjoint_yesSet_noSet, Cslib.Kolmogorov.GapMINcKT.id_eq: disjointness of the GapMINcKT promise sets and specialization to PromiseProblem.ofSet MINcKT when σ and τ are the identity on the threshold parameter.

References

• S. Hirahara, Non-Black-Box Worst-Case to Average-Case Reductions within NP
• K.-I. Ko, On the Complexity of Learning Minimum Time-Bounded Turing Machines

The Minimum Conditional Time-Bounded Kolmogorov Complexity Problem (MINcKT)

structure Cslib.Kolmogorov.MINcKT.Instance : Type

An instance of MINcKT: a target binary string string, a condition binary string cond, a step bound time, and a program size threshold size (conditional analogue of Hirahara, Definition 9).

• string : List Bool

  The target binary string x.

• cond : List Bool

  The auxiliary condition binary string y.

• time : ℕ

  The step bound t for the described multi-tape machine.

• size : ℕ

  The maximum allowed program length s.

def Cslib.Kolmogorov.MINcKT.instDecidableEqInstance.decEq (x✝ x✝¹ : Instance) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance Cslib.Kolmogorov.MINcKT.instDecidableEqInstance : DecidableEq Instance

def Cslib.Kolmogorov.MINcKT : Set MINcKT.Instance

The Minimum Conditional Time-Bounded Kolmogorov Complexity Problem (MINcKT) (conditional analogue of Hirahara, Definition 9): the set of instances (x, y, t, s) such that condTimeBoundedAt t x y ≤ s.

def Cslib.Kolmogorov.MINcKT.enc : Instance ↪ List Bool

Standard encoding of MINcKT.Instance: pairs (i.string, i.cond) with the unary thresholds (i.time, i.size).

@[simp]

theorem Cslib.Kolmogorov.MINcKT.enc_apply (i : Instance) : enc i = (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) ((i.string, i.cond), i.time, i.size)

Applying MINcKT.enc encodes ((i.string, i.cond), (i.time, i.size)) via encPair.

theorem Cslib.Kolmogorov.MINcKT.size_le_length_enc (i : Instance) : i.size ≤ (enc i).length

The unary size parameter i.size is at most (enc i).length.

theorem Cslib.Kolmogorov.MINcKT.time_le_length_enc (i : Instance) : i.time ≤ (enc i).length

The unary time parameter i.time is at most (enc i).length.

theorem Cslib.Kolmogorov.MINcKT.mem_iff {i : Instance} : i ∈ MINcKT ↔ condTimeBoundedAt i.time i.string i.cond ≤ ↑i.size

i ∈ MINcKT iff condTimeBoundedAt i.time i.string i.cond ≤ i.size.

@[simp]

theorem Cslib.Kolmogorov.MINcKT.mk_mem_iff {x y : List Bool} {t s : ℕ} : { string := x, cond := y, time := t, size := s } ∈ MINcKT ↔ condTimeBoundedAt t x y ≤ ↑s

⟨x, y, t, s⟩ ∈ MINcKT iff condTimeBoundedAt t x y ≤ s.

theorem Cslib.Kolmogorov.MINcKT.mem_iff_exists_program {i : Instance} : i ∈ MINcKT ↔ ∃ (p : List Bool), p.length ≤ i.size ∧ i.string ∈ ((DescriptionMethod.condUniversalTM i.cond).run p).runFor i.time

i ∈ MINcKT iff some program of length at most i.size outputs i.string given i.cond within i.time steps.

theorem Cslib.Kolmogorov.MINcKT.mem_of_size_le {x y : List Bool} {t s₁ s₂ : ℕ} (h : { string := x, cond := y, time := t, size := s₁ } ∈ MINcKT) (hs : s₁ ≤ s₂) : { string := x, cond := y, time := t, size := s₂ } ∈ MINcKT

Monotonicity of MINcKT in the size threshold s.

theorem Cslib.Kolmogorov.MINcKT.mem_of_time_le {x y : List Bool} {t₁ t₂ s : ℕ} (h : { string := x, cond := y, time := t₁, size := s } ∈ MINcKT) (ht : t₁ ≤ t₂) : { string := x, cond := y, time := t₂, size := s } ∈ MINcKT

Monotonicity of MINcKT in the step budget t.

theorem Cslib.Kolmogorov.MINcKT.Instance.computableInPolyTime_mk : Turing.MultiTapeTM.ComputableInPolyTime (fun (q : (List Bool × List Bool) × ℕ × ℕ) => { string := q.1.1, cond := q.1.2, time := q.2.1, size := q.2.2 }) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) enc

Constructing a MINcKT.Instance from ((x, y), (t, s)) is computable in polynomial time.

def Cslib.Kolmogorov.MINcKT.check (ip : Instance × List Bool) : Bool

The witness check for MINcKT: given an instance i and a candidate program p, checks that p.length ≤ i.size and that condUniversalTMRunFor p i.cond i.time = some i.string.

theorem Cslib.Kolmogorov.MINcKT.check_eq_true_iff {i : Instance} {p : List Bool} : check (i, p) = true ↔ p.length ≤ i.size ∧ i.string ∈ ((DescriptionMethod.condUniversalTM i.cond).run p).runFor i.time

check (i, p) = true iff p.length ≤ i.size and p outputs i.string given i.cond within i.time steps.

theorem Cslib.Kolmogorov.MINcKT.computableInPolyTime_check : Turing.MultiTapeTM.ComputableInPolyTime check (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

Checking a candidate program for MINcKT is computable in polynomial time.

theorem Cslib.Kolmogorov.MINcKT.mem_NP : MINcKT ∈ Complexity.NP enc

MINcKT is in NP (conditional analogue of Hirahara, Definition 9): a witness for (x, y, 1^t, 1^s) is a binary program p of length at most s ≤ |(x, y, 1^t, 1^s)|, verified in polynomial time by MINcKT.check.

Fixed-threshold formulation (MINcKTAt)

def Cslib.Kolmogorov.MINcKTAt (t s : ℕ → ℕ) : Set (List Bool × List Bool)

Fixed-threshold MINcKT (MINcKTAt t s): the language of string pairs (x, y) (encoded by encPair encBits encBits) such that condTimeBounded t x y ≤ s x.length.

@[simp]

theorem Cslib.Kolmogorov.mem_MINcKTAt_iff_mem_MINcKT {t s : ℕ → ℕ} {x y : List Bool} : (x, y) ∈ MINcKTAt t s ↔ { string := x, cond := y, time := t x.length, size := s x.length } ∈ MINcKT

(x, y) ∈ MINcKTAt t s iff ⟨x, y, t x.length, s x.length⟩ ∈ MINcKT.

def Cslib.Kolmogorov.MINcKTAt.toInstance (t s : ℕ → ℕ) (xy : List Bool × List Bool) : MINcKT.Instance

Embeds a pair (x, y) into MINcKT.Instance using threshold functions t and s at |x|.

@[simp]

theorem Cslib.Kolmogorov.MINcKTAt.toInstance_mem_MINcKT_iff {t s : ℕ → ℕ} {xy : List Bool × List Bool} : toInstance t s xy ∈ MINcKT ↔ xy ∈ MINcKTAt t s

toInstance t s xy ∈ MINcKT iff xy ∈ MINcKTAt t s.

theorem Cslib.Kolmogorov.MINcKTAt.computableInPolyTime_toInstance {t s : ℕ → ℕ} (ht : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Turing.MultiTapeTM.ComputableInPolyTime (toInstance t s) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) MINcKT.enc

If t and s are computable in polynomial time in unary, then toInstance t s is computable in polynomial time.

theorem Cslib.Kolmogorov.MINcKTAt.polyTimeReducible_MINcKT {t s : ℕ → ℕ} (ht : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : Complexity.PolyTimeReducible (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) MINcKT.enc (MINcKTAt t s) MINcKT

Whenever t and s are computable in polynomial time in unary, MINcKTAt t s is polynomial-time many-one reducible to MINcKT.

theorem Cslib.Kolmogorov.MINcKTAt.mem_NP {t s : ℕ → ℕ} (ht : Turing.MultiTapeTM.ComputableInPolyTime t Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : MINcKTAt t s ∈ Complexity.NP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

Fixed-threshold MINcKTAt t s is in NP whenever t and s are computable in polynomial time in unary.

theorem Cslib.Kolmogorov.MINcKTAt.mem_NP_polynomial₂ (p q : Polynomial ℕ) : (MINcKTAt (fun (x : ℕ) => Polynomial.eval x p) fun (x : ℕ) => Polynomial.eval x q) ∈ Complexity.NP (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits)

When both p.eval and q.eval are polynomials, MINcKTAt p.eval q.eval ∈ NP.

Conditional promise problem GapMINcKT

def Cslib.Kolmogorov.GapMINcKT.yesSet : Set MINcKT.Instance

The yes-instances of GapMINcKT: instances (x, y, t, s) with $K^t(x \mid y) \le s$ (conditional analogue of Hirahara, Definition 11).

def Cslib.Kolmogorov.GapMINcKT.noSet (σ τ : ℕ → ℕ → ℕ → ℕ) : Set MINcKT.Instance

The no-instances of GapMINcKT[σ, τ]: instances (x, y, t, s) with $K^{\tau(|x|, |y|, t)}(x \mid y) > \sigma(|x|, |y|, s)$ (conditional analogue of Hirahara, Definition 11, parameterized here by gap functions σ, τ : ℕ → ℕ → ℕ → ℕ of |x|, |y|, and the threshold).

theorem Cslib.Kolmogorov.GapMINcKT.disjoint_yesSet_noSet {σ τ : ℕ → ℕ → ℕ → ℕ} (hσ : ∀ (n m s : ℕ), s ≤ σ n m s) (hτ : ∀ (n m t : ℕ), t ≤ τ n m t) : Disjoint yesSet (noSet σ τ)

When s ≤ σ n m s and t ≤ τ n m t, GapMINcKT.yesSet and GapMINcKT.noSet σ τ are disjoint.

theorem Cslib.Kolmogorov.GapMINcKT.noSet_id_eq_compl : (noSet (fun (x x_1 s : ℕ) => s) fun (x x_1 t : ℕ) => t) = MINcKTᶜ

With trivial gap functions σ n m s = s and τ n m t = t, GapMINcKT.noSet is MINcKTᶜ.

def Cslib.Kolmogorov.GapMINcKT (σ τ : ℕ → ℕ → ℕ → ℕ) (hσ : ∀ (n m s : ℕ), s ≤ σ n m s) (hτ : ∀ (n m t : ℕ), t ≤ τ n m t) : Complexity.PromiseProblem MINcKT.Instance

Conditional promise problem GapMINcKT (conditional analogue of Hirahara, Definition 11, parameterized by gap functions σ, τ : ℕ → ℕ → ℕ → ℕ): separates MINcKT from GapMINcKT.noSet σ τ when s ≤ σ n m s and t ≤ τ n m t.

@[simp]

theorem Cslib.Kolmogorov.GapMINcKT.yes_eq {σ τ : ℕ → ℕ → ℕ → ℕ} (hσ : ∀ (n m s : ℕ), s ≤ σ n m s) (hτ : ∀ (n m t : ℕ), t ≤ τ n m t) : (GapMINcKT σ τ hσ hτ).yes = MINcKT

The yes-set of GapMINcKT σ τ hσ hτ is MINcKT.

@[simp]

theorem Cslib.Kolmogorov.GapMINcKT.no_eq {σ τ : ℕ → ℕ → ℕ → ℕ} (hσ : ∀ (n m s : ℕ), s ≤ σ n m s) (hτ : ∀ (n m t : ℕ), t ≤ τ n m t) : (GapMINcKT σ τ hσ hτ).no = noSet σ τ

The no-set of GapMINcKT σ τ hσ hτ is GapMINcKT.noSet σ τ.

@[simp]

theorem Cslib.Kolmogorov.GapMINcKT.id_eq : GapMINcKT (fun (x x_1 s : ℕ) => s) (fun (x x_1 t : ℕ) => t) ⋯ ⋯ = Complexity.PromiseProblem.ofSet MINcKT

With no gap (σ n m s = s and τ n m t = t), GapMINcKT is PromiseProblem.ofSet MINcKT.