The Time-Bounded Kolmogorov Complexity Problem (MINKT)

This module defines the time-bounded Kolmogorov complexity decision problem Cslib.Kolmogorov.MINKT and its fixed-parameter counterpart Cslib.Kolmogorov.MINKTAt, proves that MINKT lies in NP (and that MINKTAt t s lies in NP whenever t and s are computable in polynomial time in unary), and defines Hirahara's promise problem Cslib.Kolmogorov.GapMINKT.

Threshold conventions

Both standard formulations of the time-bounded Kolmogorov complexity decision problem are provided and bridged:

• Thresholds in the instance (Cslib.Kolmogorov.MINKT): An instance i : MINKT.Instance consists of a binary string i.string, a time bound i.time, and a size threshold i.size, encoded by MINKT.enc as x followed by 1^time and 1^size in unary (Ko; Hirahara, Definition 9). The instance belongs to MINKT when timeBoundedAt i.time i.string ≤ i.size.
• Fixed-function thresholds (Cslib.Kolmogorov.MINKTAt t s): For time and size threshold functions t s : ℕ → ℕ, MINKTAt t s : Set (List Bool) is the language of strings x with timeBounded t x ≤ s x.length (Liu and Pass, Section 2.2). The bridge mem_MINKTAt_iff_mem_MINKT identifies x ∈ MINKTAt t s with ⟨x, t x.length, s x.length⟩ ∈ MINKT, and MINKTAt.polyTimeReducible_MINKT reduces MINKTAt t s to MINKT whenever t and s are computable in polynomial time in unary.

Main definitions

• Cslib.Kolmogorov.MINKT.Instance, Cslib.Kolmogorov.MINKT, Cslib.Kolmogorov.MINKT.enc: instances, yes-instances, and unary-threshold encoding of MINKT.
• Cslib.Kolmogorov.MINKT.check: polynomial-time witness check for MINKT.
• Cslib.Kolmogorov.MINKTAt, Cslib.Kolmogorov.MINKTAt.toInstance: fixed-threshold language {x | timeBounded t x ≤ s x.length} and its canonical embedding into MINKT.Instance.
• Cslib.Kolmogorov.GapMINKT, Cslib.Kolmogorov.GapMINKT.yesSet, Cslib.Kolmogorov.GapMINKT.noSet: Hirahara's promise problem GapMINKT[σ, τ] and its yes/no sets (Hirahara, Definition 11).

Main results

• Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_string, Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_time, Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_size, Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_mk, Cslib.Kolmogorov.MINKT.computableInPolyTime_check: polynomial-time certificates for MINKT projections, constructor, and witness verifier.
• Cslib.Kolmogorov.MINKT.mem_NP: MINKT ∈ NP MINKT.enc.
• Cslib.Kolmogorov.mem_MINKTAt_iff_mem_MINKT, Cslib.Kolmogorov.MINKTAt.computableInPolyTime_toInstance, Cslib.Kolmogorov.MINKTAt.polyTimeReducible_MINKT: equivalence and polynomial-time reduction between MINKTAt t s and MINKT.
• Cslib.Kolmogorov.MINKTAt.mem_NP, Cslib.Kolmogorov.MINKTAt.mem_NP_polynomial, Cslib.Kolmogorov.MINKTAt.mem_NP_polynomial₂: MINKTAt t s ∈ NP encBits for polynomial-time unary thresholds and for polynomial time bounds t = p.eval.
• Cslib.Kolmogorov.GapMINKT.disjoint_yesSet_noSet, Cslib.Kolmogorov.GapMINKT.no_eq, Cslib.Kolmogorov.GapMINKT.id_eq: consistency and specialization of GapMINKT.

References

• K.-I. Ko, On the Complexity of Learning Minimum Time-Bounded Turing Machines
• S. Hirahara, Non-Black-Box Worst-Case to Average-Case Reductions within NP
• Y. Liu, R. Pass, On One-way Functions and Kolmogorov Complexity

structure Cslib.Kolmogorov.MINKT.Instance : Type

An instance of MINKT: a target binary string string, a step bound time, and a program size threshold size (Ko; Hirahara, Definition 9).

• string : List Bool

  The target binary string x.

• time : ℕ

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

• size : ℕ

  The maximum allowed program length s.

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

@[instance_reducible]

instance Cslib.Kolmogorov.MINKT.instDecidableEqInstance : DecidableEq Instance

def Cslib.Kolmogorov.MINKT : Set MINKT.Instance

The Minimum Time-Bounded Kolmogorov Complexity Problem (MINKT) (Ko; Hirahara, Definition 9): the set of instances (x, t, s) such that some binary program of length at most s outputs x within t steps under universalTM.

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

Standard encoding of MINKT.Instance: the string x, followed by 1^time and 1^size in unary (Ko; Hirahara, Definition 9).

@[simp]

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

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

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

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

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

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

theorem Cslib.Kolmogorov.MINKT.length_string_le_length_enc (i : Instance) : i.string.length ≤ (enc i).length

The target string length i.string.length is at most the encoded instance length (enc i).length.

theorem Cslib.Kolmogorov.MINKT.mem_iff {i : Instance} : i ∈ MINKT ↔ timeBoundedAt i.time i.string ≤ ↑i.size

An instance i belongs to MINKT iff timeBoundedAt i.time i.string ≤ i.size.

@[simp]

theorem Cslib.Kolmogorov.MINKT.mk_mem_iff {x : List Bool} {t s : ℕ} : { string := x, time := t, size := s } ∈ MINKT ↔ timeBoundedAt t x ≤ ↑s

⟨x, t, s⟩ ∈ MINKT iff timeBoundedAt t x ≤ s.

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

An instance i belongs to MINKT iff some program of length at most i.size outputs i.string within i.time steps.

theorem Cslib.Kolmogorov.MINKT.mem_iff_exists_universalTMRunFor {i : Instance} : i ∈ MINKT ↔ ∃ (p : List Bool), p.length ≤ i.size ∧ DescriptionMethod.universalTMRunFor p i.time = some i.string

An instance i belongs to MINKT iff universalTMRunFor p i.time = some i.string for some program p of length at most i.size.

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

Monotonicity of MINKT in the size threshold s.

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

Monotonicity of MINKT in the time budget t.

Polynomial-time projections, constructors, and NP membership for MINKT

theorem Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_string : Turing.MultiTapeTM.ComputableInPolyTime string enc Turing.MultiTapeTM.encBits

Extracting the target string i.string from a MINKT.Instance is computable in polynomial time.

theorem Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_time : Turing.MultiTapeTM.ComputableInPolyTime time enc Turing.MultiTapeTM.encUnary

Extracting the unary step bound i.time from a MINKT.Instance is computable in polynomial time.

theorem Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_size : Turing.MultiTapeTM.ComputableInPolyTime size enc Turing.MultiTapeTM.encUnary

Extracting the unary size bound i.size from a MINKT.Instance is computable in polynomial time.

theorem Cslib.Kolmogorov.MINKT.Instance.computableInPolyTime_mk : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : List Bool × ℕ × ℕ) => { string := p.1, time := p.2.1, size := p.2.2 }) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary)) enc

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

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

The witness check for MINKT: given an instance i and a candidate program p, checks that p.length ≤ i.size and that universalTMRunFor p i.time outputs some i.string.

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

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

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

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

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

MINKT is in NP (Ko; Hirahara): a witness for (x, 1^t, 1^s) is a binary program p of length at most s ≤ |(x, 1^t, 1^s)|, verified in polynomial time by running the universal simulator for t steps (check).

Fixed-threshold formulation (MINKTAt)

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

Fixed-threshold MINKT (MINKTAt t s, Liu and Pass, Section 2.2): the language of binary strings x with timeBounded t x ≤ s x.length.

theorem Cslib.Kolmogorov.mem_MINKTAt_iff {t s : ℕ → ℕ} {x : List Bool} : x ∈ MINKTAt t s ↔ timeBounded t x ≤ ↑(s x.length)

A string x belongs to MINKTAt t s iff timeBounded t x ≤ s x.length.

@[simp]

theorem Cslib.Kolmogorov.mem_MINKTAt_iff_mem_MINKT {t s : ℕ → ℕ} {x : List Bool} : x ∈ MINKTAt t s ↔ { string := x, time := t x.length, size := s x.length } ∈ MINKT

A string x belongs to the fixed-threshold language MINKTAt t s if and only if the instance ⟨x, t x.length, s x.length⟩ belongs to MINKT.

theorem Cslib.Kolmogorov.mem_MINKTAt_iff_exists_program {t s : ℕ → ℕ} {x : List Bool} : x ∈ MINKTAt t s ↔ ∃ (p : List Bool), p.length ≤ s x.length ∧ x ∈ (DescriptionMethod.universalTM.run p).runFor (t x.length)

A string x belongs to MINKTAt t s iff some program of length at most s x.length outputs x within t x.length steps.

theorem Cslib.Kolmogorov.mem_MINKTAt_iff_timeBoundedNat_le {t s : ℕ → ℕ} {x : List Bool} (h : timeBounded t x ≠ ⊤) : x ∈ MINKTAt t s ↔ timeBoundedNat t x ≤ s x.length

Whenever timeBounded t x ≠ ⊤ (in particular, whenever t x.length ≥ x.length + 1), membership in MINKTAt t s is equivalent to the ℕ-valued inequality timeBoundedNat t x ≤ s x.length.

def Cslib.Kolmogorov.MINKTAt.toInstance (t s : ℕ → ℕ) (x : List Bool) : MINKT.Instance

Embeds a string x into MINKT.Instance using the threshold functions t and s at |x|.

@[simp]

theorem Cslib.Kolmogorov.MINKTAt.toInstance_mem_MINKT_iff {t s : ℕ → ℕ} {x : List Bool} : toInstance t s x ∈ MINKT ↔ x ∈ MINKTAt t s

toInstance t s x ∈ MINKT iff x ∈ MINKTAt t s.

theorem Cslib.Kolmogorov.MINKTAt.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.encBits MINKT.enc

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

theorem Cslib.Kolmogorov.MINKTAt.polyTimeReducible_MINKT {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.encBits MINKT.enc (MINKTAt t s) MINKT

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

theorem Cslib.Kolmogorov.MINKTAt.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) : MINKTAt t s ∈ Complexity.NP Turing.MultiTapeTM.encBits

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

theorem Cslib.Kolmogorov.MINKTAt.mem_NP_polynomial (p : Polynomial ℕ) {s : ℕ → ℕ} (hs : Turing.MultiTapeTM.ComputableInPolyTime s Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encUnary) : MINKTAt (fun (x : ℕ) => Polynomial.eval x p) s ∈ Complexity.NP Turing.MultiTapeTM.encBits

For any polynomial time bound t = p.eval and unary polynomial-time size threshold s (as in MINKt[s] of Liu and Pass, Section 2.2), MINKTAt p.eval s ∈ NP encBits.

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

When both the time bound p.eval and size threshold q.eval are polynomials, MINKTAt p.eval q.eval ∈ NP encBits.

Hirahara's promise problem GapMINKT

def Cslib.Kolmogorov.GapMINKT.yesSet : Set MINKT.Instance

The yes-instances of GapMINKT: instances (x, t, s) with $K^t(x) \le s$ (Hirahara, Definition 11).

def Cslib.Kolmogorov.GapMINKT.noSet (σ τ : ℕ → ℕ → ℕ) : Set MINKT.Instance

The raw no-instances of GapMINKT[σ, τ]: instances (x, t, s) with $K^{\tau(|x|, t)}(x) > \sigma(|x|, s)$ (Hirahara, Definition 11).

theorem Cslib.Kolmogorov.GapMINKT.mem_yesSet_iff {i : MINKT.Instance} : i ∈ yesSet ↔ i ∈ MINKT

i ∈ GapMINKT.yesSet iff i ∈ MINKT.

theorem Cslib.Kolmogorov.GapMINKT.mem_noSet_iff {σ τ : ℕ → ℕ → ℕ} {i : MINKT.Instance} : i ∈ noSet σ τ ↔ ↑(σ i.string.length i.size) < timeBoundedAt (τ i.string.length i.time) i.string

i ∈ GapMINKT.noSet σ τ iff σ |i.string| i.size < timeBoundedAt (τ |i.string| i.time) i.string.

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

When $\sigma(n, s) \ge s$ and $\tau(n, t) \ge t$ (as required in Hirahara, Definition 11), GapMINKT.yesSet and GapMINKT.noSet σ τ are disjoint.

theorem Cslib.Kolmogorov.GapMINKT.noSet_id_eq_compl : (noSet (fun (x s : ℕ) => s) fun (x t : ℕ) => t) = MINKTᶜ

With trivial gap functions σ n s = s and τ n t = t, GapMINKT.noSet is the complement of MINKT.

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

Hirahara's GapMINKT promise problem (Hirahara, Definition 11): the promise problem whose yes-instances are MINKT, and whose no-instances are GapMINKT.noSet σ τ, when s ≤ σ n s and t ≤ τ n t. Following Hirahara, the gap hypotheses hσ and hτ are bundled to ensure disjointness of yes- and no-instances by construction.

@[simp]

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

The yes-set of GapMINKT σ τ hσ hτ is MINKT.

@[simp]

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

The no-instances of GapMINKT σ τ hσ hτ are GapMINKT.noSet σ τ.

@[simp]

theorem Cslib.Kolmogorov.GapMINKT.id_eq : GapMINKT (fun (x s : ℕ) => s) (fun (x t : ℕ) => t) ⋯ ⋯ = Complexity.PromiseProblem.ofSet MINKT

With no gap (σ n s = s and τ n t = t), GapMINKT is the decision problem MINKT viewed as a promise problem (PromiseProblem.ofSet MINKT).